From 5c75b2b701cf9c3f797deeaa58741c4946f8c9e4 Mon Sep 17 00:00:00 2001 From: Samy Avrillon Date: Fri, 26 Jul 2024 11:30:26 +0200 Subject: [PATCH] Completed proof of reflection --- Report/M2Report.tex | 63 +++++++++++++++++++++++++++++++++++-------- Report/graphs/D4.json | 2 +- Report/graphs/E1.json | 2 +- Report/graphs/E2.json | 2 +- Report/graphs/E3.json | 1 + Report/graphs/E4.json | 1 + 6 files changed, 57 insertions(+), 14 deletions(-) create mode 100644 Report/graphs/E3.json create mode 100644 Report/graphs/E4.json diff --git a/Report/M2Report.tex b/Report/M2Report.tex index a5c5e3d..7276f25 100644 --- a/Report/M2Report.tex +++ b/Report/M2Report.tex @@ -456,11 +456,11 @@ \subsubsection{Proof of H1} \todo{Relire + réeexpliquer pourquoi ça prouve} - + \label{sec:coproductConstr} We will define the sums of the form $X \oplus_i L_0^i Y$ in $\BB_i$. \[ - X \oplus_i L_0^i Y := \left(R_{i-1}^i \oplus_{i-1} L_0^{i-1} Y, (R_0^{i-1} \inj_1^{i-1})_\UU \circ \Cstr_i^X \circ (\inj_1^{i-1} \circ \dash)^{-1}\right) + X \oplus_i L_0^i Y := \left(R_{i-1}^i X \oplus_{i-1} L_0^{i-1} Y, (R_0^{i-1} \inj_1^{i-1})_\UU \circ \Cstr_i^X \circ (H_iF_{i-1}\inj_1^{i-1})^{-1}\right) \] Here, $(\inj_1^{i-1} \circ \dash)^{-1}$ is the inverse of the isomorphism of hypothesis H3', and @@ -490,12 +490,12 @@ The second injector is defined as follows: \[ - inj_2^i := (\varepsilon_i \oplus_i \id_{L_0^i Y}) \circ L_{i-1}^i \inj_2^{i-1} + \inj_2^i := (\varepsilon_i \oplus_i \id_{L_0^i Y}) \circ L_{i-1}^i \inj_2^{i-1} \] Where $\varepsilon_i$ is the counit of the adjunction $R_{i-1}^i \vdash L_{i-1}^i$, going from $L_{i-1}^i R_{i-1}^i X$ to $X$. - This goes from $L_0^i Y = L_{i-1}^i L_0^{i-1} Y$ to $L_{i-1}^i(R_{i-1}^i X \oplus_{i-1} L_0^{i-1} Y)$, which is equivalent to $L_{i-1}^i R_{i-1}^i X \oplus_i L_0^i Y)$ as $L_{i-1}^i$ is a left-adjoint functor and therefore it preserves colimits; then goes to $X \oplus_i L_0^i Y$. + This goes from $L_0^i Y = L_{i-1}^i L_0^{i-1} Y$ to $L_{i-1}^i(R_{i-1}^i X \oplus_{i-1} L_0^{i-1} Y)$, which is equivalent to $L_{i-1}^i R_{i-1}^i X \oplus_i L_0^i Y$ as $L_{i-1}^i$ is a left-adjoint functor and therefore it preserves colimits; then goes to $X \oplus_i L_0^i Y$. We will now show that this definition is actually a definition of the coproduct in $\BB_i$. To that extent, we take two objects $X$ and $Z$ in $\BB_i$, $Y$ in $\TSet$ and two morphisms of $\BB_i$ $\varphi_1 : X \to Z$ and $\varphi_2 : L_0^i Y \to Z$. @@ -514,6 +514,16 @@ \subsubsection{Proof of H3} + We need to prove that, for any objects $(X,\Cstr)$ in $\BB_i$ and $Y$ in $\TSet$, that the morphism + $F_i(\inj_1^i) : F_i(X,\Cstr) \to F_i((X,\Cstr) \oplus L_0^i Y)$ is an isomorphism. + + We know from \autoref{sec:coproductConstr} that $\inj_1^i := \inj_1^{i-1}$ as a morphism of $\BB_{i}$ is a morphism $\BB_{i-1}$ that verifies some equalities. + + We also know from the last induction step that $F_{i-1}\inj_1^{i-1}$ is an isomorphism. + \[ + (X,\Cstr) \oplus L_0^iY \simeq (X \oplus L_0^{i-1}Y, (R_0^{i-1}\inj_1^{i-1})_\UU \circ \Cstr \circ (H_iF_{i-1}\inj_1^{i-1})^{-1}) + \] + \section{Misc} @@ -779,15 +789,14 @@ \section{$F_i \vdash G_i$ reflection} \label{apx:FG-refl} - \todo{La preuve :/} We want to find, for each object $(X,(B,g))$ of $\CC_i = (X : \CC_{i-1}) \times (\Set/H_i(X))$, an isomorphism $(X,(B,g)) \to F_iG_i(X,(B,g))$. $g$ is a morphism from $B$ to $H_i(X)$ \[\begin{array}{rcl} - F_iG_i(X,\Rtsc) - &=& F_iW_i(G_{i-1}X,\Rtsc)\\ - &=& F_i(G_{i-1}X \oplus L_0^{i-1}H_\bullet(G_{i-1}X,\Rtsc),\widetilde{\inj_2})\\ - &=&(F_{i-1} \times \id)\left(G_{i-1}X \oplus L_0^{i-1}\Hbar_\bullet(G_{i-1}X,\Rtsc),(A,h)\right)\\ - &=&\left(F_{i-1}(G_{i-1}X \oplus L_0^{i-1}\Hbar_\bullet(G_{i-1}X,\Rtsc)),(A,h)\right) + F_iG_i(X,(B,g)) + &=& F_iW_i(G_{i-1}X,(B,g))\\ + &=& F_i(G_{i-1}X \oplus L_0^{i-1}H_\bullet(G_{i-1}X,(B,g)),\widetilde{\inj_2})\\ + &=&(F_{i-1} \times \id)\left(G_{i-1}X \oplus L_0^{i-1}\Hbar_\bullet(G_{i-1}X,(B,g)),(A,h)\right)\\ + &=&\left(F_{i-1}(G_{i-1}X \oplus L_0^{i-1}\Hbar_\bullet(G_{i-1}X,(B,g))),(A,h)\right) \end{array}\] Where $(A,h)$ is the pullback defined as @@ -798,7 +807,7 @@ % END OF GENERATED LATEX \end{center} - We can extend this pullback using the two isomorphisms given by the induction hypothesis and hypothesis H3. + We can extend this pullback using the two isomorphisms given by the induction hypothesis and hypothesis H3. This pullback is over the injection morphism $\inj_2$ of the coproduct, so the new pullback object is the second component of the $\bullet \oplus B$ i.e. $B$. \begin{center} % YADE DIAGRAM E2.json @@ -807,6 +816,24 @@ % END OF GENERATED LATEX \end{center} + The first component of the isomorphism is the following isomorphism, where $\eta_{i-1}^{FG}$ if the counit of the adjunction $F_{i-1} \vdash G_{i-1}$, that we know to be an isomorphism from the induction hypothesis. + + \begin{center} + % YADE DIAGRAM E3.json + % GENERATED LATEX + \input{graphs/E3.tex} + % END OF GENERATED LATEX + \end{center} + + And the second component is made using the isomorphism constructed by the pullback, that makes the diagram commute. + \begin{center} + % YADE DIAGRAM E4.json + % GENERATED LATEX + \input{graphs/E4.tex} + % END OF GENERATED LATEX + \end{center} + + \end{document} @@ -838,6 +865,20 @@ + + + + + + + + + + + + + + diff --git a/Report/graphs/D4.json b/Report/graphs/D4.json index 18b103f..195f3ad 100644 --- a/Report/graphs/D4.json +++ b/Report/graphs/D4.json @@ -1 +1 @@ -{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":6,"label":{"kind":"normal","label":"\\Cstr^X","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":7,"label":{"kind":"normal","label":"(R_0^{i-1} (\\inj_1^{i-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":8,"label":{"kind":"normal","label":"H_iF_{i-1}\\inj_1^{i-1}","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":4,"id":9,"label":{"kind":"normal","label":"R_0^{i-1}(\\inj_1^{i-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":3,"id":10,"label":{"kind":"normal","label":"(\\inj_1^{i-1} \\circ \\dash)^{-1}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"normal","position":0.5,"tail":"none"},"zindex":-3},"to":5},{"from":5,"id":11,"label":{"kind":"normal","label":"\\Cstr^X","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":0,"id":12,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":4,"id":13,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":3,"id":14,"label":{"kind":"normal","label":"\\Cstr^{X \\oplus L_0^i Y}","style":{"alignment":"left","bend":0.1,"color":"green","dashed":true,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2}],"nodes":[{"id":0,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i X)","pos":[236.5,73.5],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"(R_0^i X)_\\UU","pos":[1013,73.8125],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^{i-1} (R_{i-1}^i X \\oplus L_0^{i-1} Y))_\\UU","pos":[1017.5,249.5],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}(R_{i-1}^i X \\oplus_{i-1} L_0^{i-1} Y)","pos":[236.5,249.5],"zindex":-10000}},{"id":4,"label":{"isMath":true,"label":"(R_0^i X)_\\UU","pos":[706,235.8125],"zindex":-10000}},{"id":5,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i X","pos":[556,234.8125],"zindex":-10000}}],"sizeGrid":147,"title":"1"}]},"version":12} \ No newline at end of file +{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":6,"label":{"kind":"normal","label":"\\Cstr^X","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":7,"label":{"kind":"normal","label":"(R_0^{i-1} (\\inj_1^{i-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":8,"label":{"kind":"normal","label":"H_iF_{i-1}\\inj_1^{i-1}","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":4,"id":9,"label":{"kind":"normal","label":"R_0^{i-1}(\\inj_1^{i-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":3,"id":10,"label":{"kind":"normal","label":"(H_iF_{i-1}\\inj_1^{i-1})^{-1}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":-3},"to":5},{"from":5,"id":11,"label":{"kind":"normal","label":"\\Cstr^X","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":0,"id":12,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":4,"id":13,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":3,"id":14,"label":{"kind":"normal","label":"\\Cstr^{X \\oplus L_0^i Y}","style":{"alignment":"left","bend":0.1,"color":"green","dashed":true,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2}],"nodes":[{"id":0,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i X","pos":[236.5,73.5],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"(R_0^i X)_\\UU","pos":[1013,73.8125],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^{i-1} (R_{i-1}^i X \\oplus L_0^{i-1} Y))_\\UU","pos":[1017.5,249.5],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}(R_{i-1}^i X \\oplus_{i-1} L_0^{i-1} Y)","pos":[236.5,249.5],"zindex":-10000}},{"id":4,"label":{"isMath":true,"label":"(R_0^i X)_\\UU","pos":[706,235.8125],"zindex":-10000}},{"id":5,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i X","pos":[556,234.8125],"zindex":-10000}}],"sizeGrid":147,"title":"1"}]},"version":12} \ No newline at end of file diff --git a/Report/graphs/E1.json b/Report/graphs/E1.json index fc2c024..60bd9d6 100644 --- a/Report/graphs/E1.json +++ b/Report/graphs/E1.json @@ -1 +1 @@ -{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\CC{{\\ensuremath{\\mathcal{C}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":4,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":5,"label":{"kind":"normal","label":"R_0^{i-1}(G_{i-1}X \\oplus L_0^{i-1} \\Hbar(G_{i-1}X,\\Rtsc))_\\El","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":6,"label":{"kind":"normal","label":"h","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":7,"label":{"kind":"normal","label":"\\widetilde{\\inj_2}","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":6,"id":8,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":4}],"nodes":[{"id":0,"label":{"isMath":true,"label":"A","pos":[201,81],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"R_0^{i-1}(G_{i-1}X \\oplus L_0^{i-1} \\Hbar(G_{i-1}X,\\Rtsc))_\\El","pos":[624,81],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"R_0^{i-1}(G_{i-1}X \\oplus L_0^{i-1} \\Hbar(G_{i-1}X,\\Rtsc))_\\UU","pos":[624,180],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}(G_{i-1}X\\oplus L_0^{i-1}\\Hbar_\\bullet(\\bullet))","pos":[201,180],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12} \ No newline at end of file +{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\CC{{\\ensuremath{\\mathcal{C}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":4,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":5,"label":{"kind":"normal","label":"R_0^{i-1}(G_{i-1}X \\oplus L_0^{i-1} \\Hbar(G_{i-1}X,(B,g)))_\\El","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":6,"label":{"kind":"normal","label":"h","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":7,"label":{"kind":"normal","label":"\\widetilde{\\inj_2}","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":6,"id":8,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":4}],"nodes":[{"id":0,"label":{"isMath":true,"label":"A","pos":[201,81],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"R_0^{i-1}(G_{i-1}X \\oplus L_0^{i-1} \\Hbar(G_{i-1}X,(B,g)))_\\El","pos":[624,81],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"R_0^{i-1}(G_{i-1}X \\oplus L_0^{i-1} \\Hbar(G_{i-1}X,(B,g)))_\\UU","pos":[624,180],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}(G_{i-1}X\\oplus L_0^{i-1}\\Hbar_\\bullet(X,(B,g)))","pos":[201,180],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12} \ No newline at end of file diff --git a/Report/graphs/E2.json b/Report/graphs/E2.json index a3dba3c..57d322e 100644 --- a/Report/graphs/E2.json +++ b/Report/graphs/E2.json @@ -1 +1 @@ -{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\CC{{\\ensuremath{\\mathcal{C}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":8,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":true,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":2},"to":1},{"from":1,"id":9,"label":{"kind":"normal","label":"h","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":1,"id":10,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":11,"label":{"kind":"normal","label":"(\\en_0^i)^{-1}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":3,"id":12,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":4,"id":13,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"blue","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":5,"id":14,"label":{"kind":"normal","label":"(\\en_0^i)^{-1}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":2,"id":15,"label":{"kind":"normal","label":"\\widetilde{inj_2}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":0,"id":16,"label":{"kind":"normal","label":"h'","style":{"alignment":"left","bend":0,"color":"blue","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":7,"id":17,"label":{"kind":"normal","label":"H_iF_{i-1}(\\inj_1^i)","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":-3},"to":2},{"from":7,"id":18,"label":{"kind":"normal","label":"\\inj_2","style":{"alignment":"left","bend":0,"color":"blue","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":0,"id":19,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"blue","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":-1},"to":4},{"from":9,"id":20,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":10},{"from":16,"id":21,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":19}],"nodes":[{"id":0,"label":{"isMath":true,"label":"A'","pos":[100,100],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"A","pos":[300,164],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"H_iF_i(G_{i-1}X \\oplus L_0^{i-1}\\Hbar(\\bullet))","pos":[300,293],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"R_0^{i-1}(G_{i-1}X\\oplus L_0^{i-1}\\Hbar(\\bullet))_\\El","pos":[596,164],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"(R_0^{i-1}G_{i-1}X)_\\El \\oplus \\Hbar(\\bullet)_\\El","pos":[813,100],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"R_0^{i-1}(G_{i-1}X\\oplus L_0^{i-1}\\Hbar(\\bullet))_\\UU","pos":[596,293],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"(R_0^{i-1}G_{i-1}X)_\\UU \\oplus \\Hbar(\\bullet)_\\UU","pos":[813,373],"zindex":0}},{"id":7,"label":{"isMath":true,"label":"H_iF_{i-1}G_{i-1}X","pos":[100,373],"zindex":-10000}}],"sizeGrid":200,"title":"1"}]},"version":12} \ No newline at end of file +{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\CC{{\\ensuremath{\\mathcal{C}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":10,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":true,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":2},"to":1},{"from":1,"id":11,"label":{"kind":"normal","label":"h","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":1,"id":12,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":13,"label":{"kind":"normal","label":"(\\en_0^i)^{-1}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":3,"id":14,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":4,"id":15,"label":{"kind":"normal","label":"\\bullet \\oplus g","style":{"alignment":"left","bend":0,"color":"blue","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":-1},"to":6},{"from":5,"id":16,"label":{"kind":"normal","label":"(\\en_0^i)^{-1}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":2,"id":17,"label":{"kind":"normal","label":"\\widetilde{inj_2}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":0,"id":18,"label":{"kind":"normal","label":"g","style":{"alignment":"left","bend":0,"color":"blue","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":-2},"to":7},{"from":7,"id":19,"label":{"kind":"normal","label":"H_iF_{i-1}(\\inj_1^i)","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":-3},"to":2},{"from":7,"id":20,"label":{"kind":"normal","label":"\\inj_2","style":{"alignment":"left","bend":0,"color":"blue","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":0,"id":21,"label":{"kind":"normal","label":"\\inj_2","style":{"alignment":"left","bend":0,"color":"blue","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":4,"id":22,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":8},{"from":6,"id":23,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":9},{"from":11,"id":24,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":12},{"from":18,"id":25,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":21}],"nodes":[{"id":0,"label":{"isMath":true,"label":"B","pos":[100,140],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"A","pos":[248,241],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"H_iF_i(G_{i-1}X \\oplus L_0^{i-1}\\Hbar(G_{i-1}X,(B,g)))","pos":[248,343],"zindex":2}},{"id":3,"label":{"isMath":true,"label":"R_0^{i-1}(G_{i-1}X\\oplus L_0^{i-1}\\Hbar(G_{i-1}X,(B,g)))_\\El","pos":[639,241],"zindex":1}},{"id":4,"label":{"isMath":true,"label":"(R_0^{i-1}G_{i-1}X)_\\El \\oplus \\Hbar(G_{i-1}X,(B,g))_\\El","pos":[773,140],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"R_0^{i-1}(G_{i-1}X\\oplus L_0^{i-1}\\Hbar(G_{i-1}X,(B,g)))_\\UU","pos":[639,343],"zindex":1}},{"id":6,"label":{"isMath":true,"label":"(R_0^{i-1}G_{i-1}X)_\\UU \\oplus \\Hbar(G_{i-1}X,(B,g))_\\UU","pos":[773,423],"zindex":0}},{"id":7,"label":{"isMath":true,"label":"H_iF_{i-1}G_{i-1}X","pos":[100,423],"zindex":-10000}},{"id":8,"label":{"isMath":true,"label":"\\bullet \\oplus B","pos":[773,82],"zindex":0}},{"id":9,"label":{"isMath":true,"label":"\\bullet \\oplus H_iF_{i-1}G_{i-1}X","pos":[773,479],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12} \ No newline at end of file diff --git a/Report/graphs/E3.json b/Report/graphs/E3.json new file mode 100644 index 0000000..23663a3 --- /dev/null +++ b/Report/graphs/E3.json @@ -0,0 +1 @@ +{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\CC{{\\ensuremath{\\mathcal{C}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":3,"label":{"kind":"normal","label":"\\eta^{FG}_{i-1}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":4,"label":{"kind":"normal","label":"F_{i-1}(\\inj_1^{i-1})","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":2}],"nodes":[{"id":0,"label":{"isMath":true,"label":"X","pos":[100,100],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"F_{i-1}G_{i-1}X","pos":[300,100],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"F_{i-1}(G_{i-1}X \\oplus L_0^{i-1}\\Hbar_\\bullet(G_{i-1}X,(B,g)))","pos":[626,100],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12} \ No newline at end of file diff --git a/Report/graphs/E4.json b/Report/graphs/E4.json new file mode 100644 index 0000000..a9920f4 --- /dev/null +++ b/Report/graphs/E4.json @@ -0,0 +1 @@ +{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\CC{{\\ensuremath{\\mathcal{C}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":6,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":7,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":8,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":1,"id":9,"label":{"kind":"normal","label":"H_i\\eta^{FG}_{i-1} \\circ g","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":4,"id":10,"label":{"kind":"normal","label":"H_iF_{i-1}\\inj_0^{i-1}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":0,"id":11,"label":{"kind":"normal","label":"g","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":5,"id":12,"label":{"kind":"normal","label":"H_i\\text{HR}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4}],"nodes":[{"id":0,"label":{"isMath":true,"label":"B","pos":[100,100],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"B","pos":[300,100],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"A","pos":[678,100],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}(G_{i-1}X \\oplus L_0^{i-1}\\Hbar_\\bullet(G_{i-1}X,(B,g)))","pos":[678,211],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"H_iF_{i-1}G_{i-1}X","pos":[300,211],"zindex":-10000}},{"id":5,"label":{"isMath":true,"label":"H_iX","pos":[100,211],"zindex":-10000}}],"sizeGrid":200,"title":"1"}]},"version":12} \ No newline at end of file