diff --git a/Report/M2Report.tex b/Report/M2Report.tex index 8776d78..280293a 100644 --- a/Report/M2Report.tex +++ b/Report/M2Report.tex @@ -1,5 +1,5 @@ % !TeX spellcheck = en_US -\documentclass[10pt,a4paper]{article} +\documentclass[11pt,a4paper]{article} \input{./header.tex} @@ -19,6 +19,7 @@ \hsep + \setcounter{tocdepth}{2} \tableofcontents \newpage @@ -509,7 +510,7 @@ \[ R_0^i := R^1_0 \circ \dots \circ R_{i-1}^i \] - \item An operator $\tl^i : \BB_i \times \BB_0 \to \BB_i$ along with a morphism $\inj_\tl^i : X \to X \tl^i Y$ for every $X,Y$ in $\BB_i \times \BB_0$, such that the canonical morphism $\en_{i-1}^i : (R_{i-1}^i X) \tl^{i-1} Y \to R_{i-1}^i (X \tl^i Y)$ is an isomorphism. This operation follows a specific universal property: For every morphisms $g : X \to Z$ and $h : Y \to R_0^iZ$, there is an unique morphism $\{g;h\}$ such that the two following diagrams commute: + \item An operator $\tl^i : \BB_i \times \BB_0 \to \BB_i$ along with two morphism $\inj_1^i : X \to X \tl^i Y$ and $\inj_2^i : Y \to R_0^i(X \tl^i Y)$ for every $X,Y$ in $\BB_i \times \BB_0$, such that the canonical morphism $\en_{i-1}^i : (R_{i-1}^i X) \tl^{i-1} Y \to R_{i-1}^i (X \tl^i Y)$ is an isomorphism. This operation follows a specific universal property: For every morphisms $g : X \to Z$ and $h : Y \to R_0^iZ$, there is an unique morphism $\{g;h\}$ such that the following diagrams commute: \label{sec:tlUniversalProperty} \begin{center} @@ -519,19 +520,16 @@ % END OF GENERATED LATEX \end{center} - where $\en_0^i$ is the following composition: - + We will also denote a composition morphism as such: \[\en_0^i := R_0^{i-1} \en_{i-1}^i \circ \dots \circ R_0^1\en_1^2 \circ \en_0^1 : (R_0^i X) \oplus Y = (R_0^i X) \tl^0 Y \to R_0^i (X \tl^i Y)\] - And where $\inj_2$ is the second injector of $\oplus$, the coproduct of the category $\BB_0 = \TSet$. We will define $\tl^0$ to be $\oplus$, so the equality above holds. - The operator is also defined on morphisms, such that for any morphism $g : X \to X'$ in $\BB_i$ and $h : Y \to Y'$ in $\BB_0$, there is a morphism $g \tl^i h : X \tl^i Y \to X' \tl^i Y'$ in $\BB_i$. \item A functor $F_i : \BB_i \to \CC_i$ \item A functor $G_i : \CC_i \to \BB_i$ \item An adjunction between them $F_i \vdash G_i$ \item A proof that $F_iG_i \cong \Id_{\CC_i}$ (i.e. $F_i \vdash G_i$ make up a coreflection) - \item A proof that $F_i\inj_\tl^i$ is an isomorphism. The inverse isomorphism will be denoted as $(F_i\inj_\tl^i)^{-1}$ + \item A proof that $F_i\inj_1^i$ is an isomorphism. The inverse isomorphism will be denoted as $(F_i\inj_1^i)^{-1}$ \end{itemize} Here is a figure that describes the recursive construction of some of the above objects @@ -625,7 +623,7 @@ \setlength\itemsep{-1ex} \item $\CC_0$ is $\one$, the category with only one object $\star$ and one trivial morphism (i.e. the terminal category of $\Cat$) \item $\BB_0$ is $\TSet$, the category of models of the $(\mathcal{O},\El)$ sort specification. - \item The universal property of $\tl^0$ is that of the coproduct. Therefore, we will define $\tl^0 : \BB_0 \times \BB_0 \to \BB_0$ to be the coproduct $\oplus$ of $\TSet$, with $\inj_\tl^0 : X \to X \oplus Y$ being the first injector of the coproduct. The second injector of the coproduct $\oplus$ will be refered as $\inj_2$. + \item The universal property of $\tl^0$ is that of the coproduct. Therefore, we will define $\tl^0 : \BB_0 \times \BB_0 \to \BB_0$ to be the coproduct $\oplus$ of $\TSet$, with $\inj_1^0 : X \to X \tl^0 Y$ being the first injector of the coproduct and $\inj_2^0 : Y \to X \tl^0 Y$ being the second injector. \item $F_0 : \TSet \to \one$ is the terminal functor of $\Cat$ \item $G_0 : \one \to \TSet$ is the functor that sends the only object of $\one$ to the initial object of $\TSet$: $0_\TSet$ \item For $X$ an object of $\TSet$, we have @@ -808,7 +806,7 @@ \paragraph{Constructing the objects} We will define the $\tl^i$ operator of two objects $X$ from $\BB_i$ and $Y$ from $\BB_0$ as follows: \[ - X \tl_i Y := \left((R_{i-1}^i X) \tl^{i-1} Y, (R_0^{i-1} \inj_\tl^{i-1})_\UU \circ \Cstr_i^X \circ (H_iF_{i-1}\inj_\tl^{i-1})^{-1}\right) + X \tl_i Y := \left((R_{i-1}^i X) \tl^{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) \] The constructor goes as follows: @@ -820,9 +818,9 @@ % END OF GENERATED LATEX \end{center} - The injector $\inj_\tl^i : X \to X \tl^i Y$ is defined as follows: + The first injector $\inj_1^i : X \to X \tl^i Y$ is defined as follows: \[ - \inj_\tl^i := \inj_\tl^{i-1} : R_{i-1}^i X \to R_{i-1}^i (X \tl^i Y) = R_{i-1}^i X \tl^{i-1} Y + \inj_1^i := \inj_1^{i-1} : R_{i-1}^i X \to R_{i-1}^i (X \tl^i Y) = R_{i-1}^i X \tl^{i-1} Y \] It is a morphism of $\BB_i$ as it makes the following diagram commute: @@ -833,9 +831,14 @@ % END OF GENERATED LATEX \end{center} + The second injector is defined as + \[ + \inj_2^i := \inj_2^{i-1} : Y \to R_0^{i-1} (R_{i-1}^iX \tl^{i-1} Y) = R_0^i (X \tl^i Y) + \] + \paragraph{Universal Property} We will now show that that the universal property stated in \autoref{sec:tlUniversalProperty} holds. - To that end, we take two objects $X$ and $Z$ in $\BB_i$, $Y$ in $\BB_0$, a morphism $g : X \to Z$ in $\BB_i$ and a morphism $h : Y \to R_0^iZ$ in $\BB_0$. We want to build a morphism $\{g,h\}$ of $\BB_i$ such that the following two diagrams commute. + To that end, we take two objects $X$ and $Z$ in $\BB_i$, $Y$ in $\BB_0$, a morphism $g : X \to Z$ in $\BB_i$ and a morphism $h : Y \to R_0^iZ$ in $\BB_0$. We want to build a morphism $\{g,h\}$ of $\BB_i$ such that the following diagram commute. \begin{center} % YADE DIAGRAM TlUniversal.json @@ -853,6 +856,8 @@ % END OF GENERATED LATEX \end{center} + And this morphism $\{g;h\}_i$ is such that the universal property for it is exactly the same as the one of $\{R_{i-1}^i g, h\}$. + With this definition, the isomorphism $\en_{i-1}^i : (R_{i-1}^i X) \tl^{i-1} Y \to R_{i-1}^i(X \tl^i Y)$ is simply the identity morphism. \paragraph{Building morphisms} @@ -866,25 +871,27 @@ This is indeed a morphism of $\BB_i$ as it makes the following diagram commute: \begin{center} + \begin{scaletikzpicturetowidth}{.9\textwidth} % YADE DIAGRAM TlDefOnMorphisms.json % GENERATED LATEX \input{graphs/TlDefOnMorphisms.tex} % END OF GENERATED LATEX + \end{scaletikzpicturetowidth} \end{center} \paragraph{Composition with $F_i$} We finally need to prove, for any objects $X$ in $\BB_i$ and $Y$ in $\TSet$, that the morphism - $F_i(\inj_\tl^i) : F_iX \to F_i(X \tl^i Y)$ is an isomorphism. + $F_i(\inj_1^i) : F_iX \to F_i(X \tl^i Y)$ is an isomorphism. - Morphisms $\BB_{i}$ are morphisms of $\BB_{i-1}$ that follows some equations, and composition is the same. Moreover, we know from the definition above that $R_{i-1^i} \inj_\tl^i := \inj_\tl^{i-1}$. + Morphisms $\BB_{i}$ are morphisms of $\BB_{i-1}$ that follows some equations, and composition is the same. Moreover, we know from the definition above that $R_{i-1^i} \inj_1^i := \inj_1^{i-1}$. - So, we just need to know that $R_{i-1}^i(F_{i-1}\inj_\tl^i)$ is an isomorphism. + So, we just need to know that $R_{i-1}^i(F_{i-1}\inj_1^i)$ is an isomorphism. \[ - R_{i-1}^iF_i\inj_\tl^i = \left[(F_{i-1} \times \id) (E(\inj_\tl^i))\right]_1 = \left[(F_{i-1} \times \id) (R_{i-1}^i \inj_\tl^i,!)\right]_1 = F_{i-1} \inj_\tl^{-1} + R_{i-1}^iF_i\inj_1^i = \left[(F_{i-1} \times \id) (E(\inj_1^i))\right]_1 = \left[(F_{i-1} \times \id) (R_{i-1}^i \inj_1^i,!)\right]_1 = F_{i-1} \inj_1^{i-1} \] - And we know from the previous induction step that $F_{i-1}\inj_\tl^{i-1}$ is an isomorphism. Therefore, $F_i\inj_\tl^i$ is an isomorphism. + And we know from the previous induction step that $F_{i-1}\inj_1^{i-1}$ is an isomorphism. Therefore, $F_i\inj_1^i$ is an isomorphism. \section{Other Properties} @@ -1093,7 +1100,7 @@ \section{Summary} - \lipsum[2-3] + \lipsum[1-3] @@ -1112,7 +1119,7 @@ \section{$W \dashv E$ adjunction} \label{apx:adjunction} - \subsubsection{Constructing $\phi_{XYZ}$} + \subsection{Constructing $\phi_{XYZ}$} Let $f$ be in $\Hom(W(X,Y),Z)$. We want to construct $\phi_{XYZ}(f) : (X,Y) \to E(Z)$. @@ -1133,10 +1140,9 @@ % GENERATED LATEX \input{graphs/PhiXYZSndComponentPullback.tex} % END OF GENERATED LATEX - \end{center} - \subsubsection{Constructing $\phi^{-1}_{XYZ}$} + \subsection{Constructing $\phi^{-1}_{XYZ}$} Now, we take $(g,h)$ a morphism from $(X,Y)$ to $E(Z)$. @@ -1165,14 +1171,13 @@ % GENERATED LATEX \input{graphs/PhiXYZ-1MorphismOfBi.tex} % END OF GENERATED LATEX - \end{center} \subsection{Composition $\phi_{XYZ} \circ \phi_{XYZ}^{-1}$} The first component of $\phi_{XYZ} (\phi_{XYZ}^{-1}(g,h))$ is \[ - R_{i-1}^i(\phi_{XYZ}^{-1}(g,h)) \circ \inj_\tl^{i-1} = \left\{g ; \square \right\} \circ \inj_\tl^{i-1} = g + R_{i-1}^i\left(\phi_{XYZ}^{-1}(g,h)\right) \circ \inj_1^{i-1} = \left\{g ; \square \right\} \circ \inj_1^{i-1} = g \] The second component of $\phi_{XYZ} (\phi_{XYZ}^{-1}(g,h))$ follows the following diagram @@ -1183,11 +1188,11 @@ \input{graphs/CompositionSecondComponent.tex} % END OF GENERATED LATEX -\end{center} + \end{center} \todo{Justifier que la partie du haut commute, i.e. que \[ - (R_0^{i-1}\{g,\square\})_\El \circ (\en_0^i)_\El \circ (\inj_2)_\El = \square_\El + (R_0^{i-1}\{g,\square\})_\El \circ (\inj^{i-1}_2)_\El = \square_\El \]} The diagram commutes, and so we can deduce that the second component of $\phi_{XYZ}(f)$ is $h$, by proprty of the pullback $E(Z)$ @@ -1197,7 +1202,7 @@ Now, the converse composition is \[ - \phi_{XYZ}^{-1} (\phi_{XYZ}(f)) = \left\{R_{i-1}^i f \circ \inj_\tl^{i-1} ; \square \right\} + \phi_{XYZ}^{-1} (\phi_{XYZ}(f)) = \left\{R_{i-1}^i f \circ \inj_1^{i-1} ; \square \right\} \] where $\square$ follows the following diagram @@ -1208,13 +1213,13 @@ % END OF GENERATED LATEX \end{center} - We want to show that $\phi_{XYZ}^{-1} (\phi_{XYZ}(f)) = f$. By definition of $\{;\}$ in $\BB_i$, it suffices to show that $\square = R_0^i f \circ \en_0^{i-1} \circ \inj_2$. + We want to show that $\phi_{XYZ}^{-1} (\phi_{XYZ}(f)) = f$. By definition of $\{;\}$ in $\BB_i$, it suffices to show that $\square = R_0^i f \circ \inj^{i-1}_2$. The two required equalities are proved by the diagram above: \begin{align*} - \square_\El = \left(R_0^i f \circ \en_0^{i-1} \circ \inj_2\right)_\El \\ - \square_\UU = \left(R_0^i f \circ \en_0^{i-1} \circ \inj_2\right)_\UU + \square_\El = \left(R_0^i f \circ \inj^{i-1}_2\right)_\El \\ + \square_\UU = \left(R_0^i f \circ \inj^{i-1}_2\right)_\UU \end{align*} \subsection{Naturality} @@ -1234,23 +1239,30 @@ \[\begin{array}{rcl} \phi_{X'Y'Z'}(f \circ \ii \circ W(g,h))_1 - &=& R_{i-1}^i\left(f \circ \ii \circ (g \tl^{i-1} K_\bullet(g,h))^+\right) \circ \inj_\tl^{i-1} \\ - &=& R_{i-1}^i f \circ R_{i-1}^i \ii \circ (g \tl^{i-1} K_\bullet(g,h)) \circ \inj_\tl^{i-1} \\ - &=& R_{i-1}^i f \circ R_{i-1}^i \ii \circ \inj_\tl^{i-1} \circ g \\ + &=& R_{i-1}^i\left(f \circ \ii \circ (g \tl^{i-1} K_\bullet(g,h))^+\right) \circ \inj_1^{i-1} \\ + &=& R_{i-1}^i f \circ R_{i-1}^i \ii \circ (g \tl^{i-1} K_\bullet(g,h)) \circ \inj_1^{i-1} \\ + &=& R_{i-1}^i f \circ R_{i-1}^i \ii \circ \inj_1^{i-1} \circ g \\ &=& \left[E(f) \circ \phi_{XYZ}(\ii) \circ (g,h)\right]_1 \end{array}\] - The second components are defined as described by the following diagram + The second components are defined by the pullback properties of $E(Z)$ and $E(Z')$. The two sides that define each morphism are give separately in the two following diagrams. \begin{center} - % YADE DIAGRAM NaturalityDoublePullbackDefinition.json + % YADE DIAGRAM NaturalityDoublePullbackDefinition1.json % GENERATED LATEX - \input{graphs/NaturalityDoublePullbackDefinition.tex} + \input{graphs/NaturalityDoublePullbackDefinition1.tex} % END OF GENERATED LATEX \end{center} - The second projection of $\phi_{XYZ}(f \circ \ii \circ W(g,h))$ is defined by the pullback of $E(Z')$ commuting with the two path highlighted by the inner blue line. And that of $\phi_{X'Y'Z'}(\ii)$ is defined by the red outer line. - The outer squares commute, and therefore, by the pullback property, we get that + \begin{center} + % YADE DIAGRAM NaturalityDoublePullbackDefinition2.json + % GENERATED LATEX + \input{graphs/NaturalityDoublePullbackDefinition2.tex} + % END OF GENERATED LATEX + \end{center} + + The second projection of $\phi_{XYZ}(f \circ \ii \circ W(g,h))$ is defined by the pullback of $E(Z')$ commuting with the blue bottom path. And that of $\phi_{X'Y'Z'}(\ii)$ is defined by the red top path. + both diagrams commute, and therefore, by the pullback property, we get that \[ \phi_{X'Y'Z'}(f\circ\ii\circ W(g,h))_2 = \left[E(f) \circ \phi_{XYZ}(\ii) \circ (g,h)\right]_2 \] @@ -1279,7 +1291,7 @@ % END OF GENERATED LATEX \end{center} - We can extend this pullback with the two isomorphisms $\en_0^i$ and $H_iF_{i-1}(\inj_\tl^{i-1})$ in another pullback. This new pullback is over the injection morphism $\inj_2$ of the coproduct of $\TSet$, so the new pullback object is the second component of the $\bullet \oplus B$ i.e. $B$. + We can extend this pullback with the isomorphisms $H_iF_{i-1}(\inj_\tl^{i-1})$ into another pullback. This new pullback is over the injection morphism $\inj_2$ of the coproduct of $\TSet$, so the new pullback object is the second component of the $\bullet \oplus B$ i.e. $B$, by property of the coproduct. \begin{center} % YADE DIAGRAM ReflectionFGExtendedPullback.json @@ -1288,6 +1300,8 @@ % END OF GENERATED LATEX \end{center} + \todo{Il manque l'info $\inj_2^{i-1} \circ \en_0^{i-1} = \inj_2^0$ OU ALORS que $\inj_2^{i-1}$ se transpose dans les pullbacks aussi.} + 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} @@ -1307,153 +1321,3 @@ \end{document} - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - diff --git a/Report/graphs/CompositionSecondComponent.json b/Report/graphs/CompositionSecondComponent.json index 8c79bd2..945dae5 100644 --- a/Report/graphs/CompositionSecondComponent.json +++ b/Report/graphs/CompositionSecondComponent.json @@ -1 +1 @@ -{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"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":1},{"from":1,"id":11,"label":{"kind":"normal","label":"(R_0^i Z)_p","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":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":"\\Cstr^Z","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":4,"id":14,"label":{"kind":"normal","label":"y","style":{"alignment":"right","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":"\\phi_{XYZ}(f)_2","style":{"alignment":"left","bend":0.1,"color":"black","dashed":true,"head":"default","kind":"normal","position":0.6,"tail":"none"},"zindex":0},"to":0},{"from":4,"id":16,"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":6},{"from":7,"id":17,"label":{"kind":"normal","label":"\\en_0^{i-1}","style":{"alignment":"left","bend":-0.2,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":8},{"from":8,"id":18,"label":{"kind":"normal","label":"(R_0^{i-1}\\left\\{g,\\square\\right\\})_\\El","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":5,"id":19,"label":{"kind":"normal","label":"H_iF_{i-1}\\inj_\\tl^{i-1}","style":{"alignment":"left","bend":0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.6,"tail":"none"},"zindex":6},"to":9},{"from":9,"id":20,"label":{"kind":"normal","label":"H_iF_{i-1}R_{i-1}^i\\left\\{g,\\square\\right\\}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":6,"id":21,"label":{"kind":"normal","label":"(\\inj_2)_\\El","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":5,"id":22,"label":{"kind":"normal","label":"H_iF_{i-1}g","style":{"alignment":"left","bend":-0.1,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":4,"id":23,"label":{"kind":"normal","label":"h","style":{"alignment":"left","bend":-0.1,"color":"black","dashed":true,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":4,"id":24,"label":{"kind":"normal","label":"\\square_\\El","style":{"alignment":"left","bend":-0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":12,"id":25,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":10}],"nodes":[{"id":0,"label":{"isMath":true,"label":"E(Z)","pos":[473,329.8125],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"(R_0^i Z)_\\El","pos":[632,329.8125],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[632,459.8125],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i Z","pos":[473,459.8125],"zindex":-10000}},{"id":4,"label":{"isMath":true,"label":"Y","pos":[108,167.8125],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"H_iF_{i-1}X","pos":[108,329.8125],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"(K_{H_iF_{i-1}}(X,Y))_\\El","pos":[108,87.8125],"zindex":0}},{"id":7,"label":{"isMath":true,"label":"\\left(R_0^{i-1}X \\oplus K_{H_iF_{i-1}}(X,Y)\\right)_\\El","pos":[393,87.8125],"zindex":0}},{"id":8,"label":{"isMath":true,"label":"R_0^{i-1}(X \\tl^{i-1} K_{H_iF_{i-1}}(X,Y))_\\El","pos":[632,167.8125],"zindex":0}},{"id":9,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i(W(X,Y))","pos":[182,459.8125],"zindex":-10000}}],"sizeGrid":200,"title":"1"}]},"version":12} \ No newline at end of file +{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":9,"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":10,"label":{"kind":"normal","label":"(R_0^i Z)_p","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":11,"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":12,"label":{"kind":"normal","label":"\\Cstr^Z","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":4,"id":13,"label":{"kind":"normal","label":"y","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":4,"id":14,"label":{"kind":"normal","label":"\\phi_{XYZ}(f)_2","style":{"alignment":"left","bend":0.1,"color":"black","dashed":true,"head":"default","kind":"normal","position":0.6,"tail":"none"},"zindex":0},"to":0},{"from":4,"id":15,"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":6},{"from":7,"id":16,"label":{"kind":"normal","label":"(R_0^{i-1}\\left\\{g,\\square\\right\\})_\\El","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":5,"id":17,"label":{"kind":"normal","label":"H_iF_{i-1}\\inj_1^{i-1}","style":{"alignment":"left","bend":0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.6,"tail":"none"},"zindex":6},"to":8},{"from":8,"id":18,"label":{"kind":"normal","label":"H_iF_{i-1}R_{i-1}^i\\left\\{g,\\square\\right\\}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":5,"id":19,"label":{"kind":"normal","label":"H_iF_{i-1}g","style":{"alignment":"left","bend":-0.1,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":4,"id":20,"label":{"kind":"normal","label":"h","style":{"alignment":"left","bend":-0.1,"color":"black","dashed":true,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":4,"id":21,"label":{"kind":"normal","label":"\\square_\\El","style":{"alignment":"left","bend":-0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":6,"id":22,"label":{"kind":"normal","label":"(\\inj_2^{i-1})_\\El","style":{"alignment":"left","bend":-0.1,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":11,"id":23,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":9}],"nodes":[{"id":0,"label":{"isMath":true,"label":"E(Z)","pos":[473,329.8125],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"(R_0^i Z)_\\El","pos":[632,329.8125],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[632,459.8125],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i Z","pos":[473,459.8125],"zindex":-10000}},{"id":4,"label":{"isMath":true,"label":"Y","pos":[108,167.8125],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"H_iF_{i-1}X","pos":[108,329.8125],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"(K_{H_iF_{i-1}}(X,Y))_\\El","pos":[108,87.8125],"zindex":0}},{"id":7,"label":{"isMath":true,"label":"R_0^{i-1}(X \\tl^{i-1} K_{H_iF_{i-1}}(X,Y))_\\El","pos":[632,167.8125],"zindex":0}},{"id":8,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i(W(X,Y))","pos":[182,459.8125],"zindex":-10000}}],"sizeGrid":200,"title":"1"}]},"version":12} \ No newline at end of file diff --git a/Report/graphs/CompositionSquareConstruction.json b/Report/graphs/CompositionSquareConstruction.json index 7469d41..54b406e 100644 --- a/Report/graphs/CompositionSquareConstruction.json +++ b/Report/graphs/CompositionSquareConstruction.json @@ -1 +1 @@ -{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":13,"label":{"kind":"normal","label":"\\phi_{XYZ}(f)_2","style":{"alignment":"right","bend":0,"color":"black","dashed":true,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":14,"label":{"kind":"normal","label":"","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":15,"label":{"kind":"normal","label":"(R_0^i Z)_p","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":16,"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":4},{"from":4,"id":17,"label":{"kind":"normal","label":"\\Cstr^Z","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":18,"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":5},{"from":5,"id":19,"label":{"kind":"normal","label":"H_i(F_{i-1}\\inj_\\tl^{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":6,"id":20,"label":{"kind":"normal","label":"H_iF_{i-1}R_{i-1}^i f","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":21,"label":{"kind":"normal","label":"\\square_\\El","style":{"alignment":"left","bend":-0.1,"color":"blue","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":5,"id":22,"label":{"kind":"normal","label":"\\square_\\UU","style":{"alignment":"right","bend":0.2,"color":"blue","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":5,"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":7},{"from":7,"id":24,"label":{"kind":"normal","label":"(\\inj_2)_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":8},{"from":8,"id":25,"label":{"kind":"normal","label":"(\\en_0^{i-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":9},{"from":9,"id":26,"label":{"kind":"normal","label":"(R_0^i f)_\\UU","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":6,"id":27,"label":{"kind":"normal","label":"\\Cstr^{W(X,Y)}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":9},{"from":12,"id":28,"label":{"kind":"normal","label":"(R_0^if)_\\El","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":11,"id":29,"label":{"kind":"normal","label":"(\\en_0^{i-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":12},{"from":10,"id":30,"label":{"kind":"normal","label":"(\\inj_2)_\\El","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":11},{"from":0,"id":31,"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":10},{"from":16,"id":32,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":14}],"nodes":[{"id":0,"label":{"isMath":true,"label":"Y","pos":[80,179],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"E(Z)","pos":[720,179],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i Z)_\\El","pos":[880,179],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[880,302],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i Z","pos":[720,302],"zindex":-10000}},{"id":5,"label":{"isMath":true,"label":"H_iF_{i-1}X","pos":[80,302],"zindex":-10000}},{"id":6,"label":{"isMath":true,"label":"H_iF_{i-1}(X\\tl^{i-1} K_\\bullet (X,Y))","pos":[400,302],"zindex":-10000}},{"id":7,"label":{"isMath":true,"label":"K_\\bullet(X,Y)_\\UU","pos":[80,453],"zindex":0}},{"id":8,"label":{"isMath":true,"label":"\\left[R_0^{i-1} X \\oplus K_\\bullet(X,Y)\\right]_\\UU","pos":[400,453],"zindex":0}},{"id":9,"label":{"isMath":true,"label":"\\left[R_0^i(W(X,Y))\\right]_\\UU","pos":[720,453],"zindex":0}},{"id":10,"label":{"isMath":true,"label":"K_\\bullet(X,Y)_\\El","pos":[80,80],"zindex":0}},{"id":11,"label":{"isMath":true,"label":"(R_0^{i-1}X\\oplus K_\\bullet(X,Y))_\\El","pos":[400,80],"zindex":0}},{"id":12,"label":{"isMath":true,"label":"R_0^{i-1}(X \\tl^{i-1} K_\\bullet(X,Y))","pos":[720,80],"zindex":0}}],"sizeGrid":160,"title":"1"}]},"version":12} \ No newline at end of file +{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":11,"label":{"kind":"normal","label":"\\phi_{XYZ}(f)_2","style":{"alignment":"right","bend":0,"color":"black","dashed":true,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":12,"label":{"kind":"normal","label":"","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":13,"label":{"kind":"normal","label":"(R_0^i Z)_p","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":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":4},{"from":4,"id":15,"label":{"kind":"normal","label":"\\Cstr^Z","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":16,"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":5},{"from":5,"id":17,"label":{"kind":"normal","label":"H_i(F_{i-1}\\inj_1^{i-1})","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":6,"id":18,"label":{"kind":"normal","label":"H_iF_{i-1}R_{i-1}^i f","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":19,"label":{"kind":"normal","label":"\\square_\\El","style":{"alignment":"left","bend":-0.1,"color":"blue","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":5,"id":20,"label":{"kind":"normal","label":"\\square_\\UU","style":{"alignment":"right","bend":0.2,"color":"blue","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":5,"id":21,"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":7},{"from":8,"id":22,"label":{"kind":"normal","label":"(R_0^i f)_\\UU","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":6,"id":23,"label":{"kind":"normal","label":"\\Cstr^{W(X,Y)}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":8},{"from":10,"id":24,"label":{"kind":"normal","label":"(R_0^if)_\\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":25,"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":9,"id":26,"label":{"kind":"normal","label":"(\\inj_2^{i-1})_\\El","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":10},{"from":7,"id":27,"label":{"kind":"normal","label":"(\\inj_2^{i-1})_\\El","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":8},{"from":5,"id":28,"label":{"kind":"normal","label":"\\simeq","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":14,"id":29,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":12}],"nodes":[{"id":0,"label":{"isMath":true,"label":"Y","pos":[80,179],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"E(Z)","pos":[691,179],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i Z)_\\El","pos":[851,179],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[851,292],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i Z","pos":[691,292],"zindex":-10000}},{"id":5,"label":{"isMath":true,"label":"H_iF_{i-1}X","pos":[80,292],"zindex":-10000}},{"id":6,"label":{"isMath":true,"label":"H_iF_{i-1}(X\\tl^{i-1} K_\\bullet (X,Y))","pos":[407,292],"zindex":-10000}},{"id":7,"label":{"isMath":true,"label":"K_\\bullet(X,Y)_\\UU","pos":[80,443],"zindex":0}},{"id":8,"label":{"isMath":true,"label":"\\left[R_0^i(W(X,Y))\\right]_\\UU","pos":[691,443],"zindex":0}},{"id":9,"label":{"isMath":true,"label":"K_\\bullet(X,Y)_\\El","pos":[80,80],"zindex":0}},{"id":10,"label":{"isMath":true,"label":"R_0^{i-1}(X \\tl^{i-1} K_\\bullet(X,Y))","pos":[691,80],"zindex":0}}],"sizeGrid":160,"title":"1"}]},"version":12} \ No newline at end of file diff --git a/Report/graphs/NaturalityDoublePullbackDefinition.json b/Report/graphs/NaturalityDoublePullbackDefinition.json deleted file mode 100644 index 9b039ee..0000000 --- a/Report/graphs/NaturalityDoublePullbackDefinition.json +++ /dev/null @@ -1 +0,0 @@ -{"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":20,"label":{"kind":"normal","label":"E(f)_2","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.7,"tail":"none"},"zindex":1},"to":1},{"from":1,"id":21,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":1},"to":2},{"from":0,"id":22,"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":23,"label":{"kind":"normal","label":"H_iF_{i-1}R_{i-1}^if","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":1,"id":24,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":1},"to":4},{"from":2,"id":25,"label":{"kind":"normal","label":"\\Cstr^{Z'}","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":4,"id":26,"label":{"kind":"normal","label":"(R_0^i Z')_p","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":27,"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":6},{"from":6,"id":28,"label":{"kind":"normal","label":"(R_0^i Z)_\\El","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":6,"id":29,"label":{"kind":"normal","label":"(R_0^i Z)_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"normal","position":0.7,"tail":"none"},"zindex":0},"to":7},{"from":7,"id":30,"label":{"kind":"normal","label":"(R_0^i Z)_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":3,"id":31,"label":{"kind":"normal","label":"\\Cstr^Z","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":8,"id":32,"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":9},{"from":9,"id":33,"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":10},{"from":8,"id":34,"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":11},{"from":11,"id":35,"label":{"kind":"normal","label":"H_iF_{i-1}g","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":10},{"from":12,"id":36,"label":{"kind":"normal","label":"R_0^i\\ii_\\El","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":1},"to":6},{"from":8,"id":37,"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":13},{"from":9,"id":38,"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":14},{"from":14,"id":39,"label":{"kind":"normal","label":"\\inj_2","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":15},{"from":13,"id":40,"label":{"kind":"normal","label":"\\inj_2","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":16},{"from":16,"id":41,"label":{"kind":"normal","label":"\\left(R_0^{i-1}g \\oplus K_\\bullet(g,h)\\right)_\\El","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":15},{"from":15,"id":42,"label":{"kind":"normal","label":"\\en_0^{i-1}","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":12},{"from":16,"id":43,"label":{"kind":"normal","label":"\\en_0^{i-1}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":17},{"from":17,"id":44,"label":{"kind":"normal","label":"R_0^iW(g,h)_\\El","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":12},{"from":10,"id":45,"label":{"kind":"normal","label":"H_iF_{i-1}\\inj_\\tl^{i-1}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":18},{"from":11,"id":46,"label":{"kind":"normal","label":"H_iF_{i-1}\\inj_\\tl^{i-1}","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":1},"to":19},{"from":19,"id":47,"label":{"kind":"normal","label":"H_iF_{i-1}R_{i-1}^iW(g,h)","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":18},{"from":18,"id":48,"label":{"kind":"normal","label":"H_iF_{i-1}R_{i-1}^i\\ii","style":{"alignment":"left","bend":0.20000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":9,"id":49,"label":{"kind":"normal","label":"\\phi_{XYZ}(\\ii)","style":{"alignment":"right","bend":0,"color":"red","dashed":true,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":8,"id":50,"label":{"kind":"normal","label":"\\phi_{X'Y'Z'}(f\\circ \\ii \\circ W(g,h))","style":{"alignment":"right","bend":0.10000000000000003,"color":"blue","dashed":true,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":8,"id":51,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":-0.1,"color":"blue","dashed":false,"head":"none","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":11},{"from":11,"id":52,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":-0.1,"color":"blue","dashed":false,"head":"none","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":19},{"from":19,"id":53,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":-0.1,"color":"blue","dashed":false,"head":"none","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":18},{"from":18,"id":54,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"blue","dashed":false,"head":"none","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":55,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":-0.1,"color":"blue","dashed":false,"head":"none","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":8,"id":56,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0.1,"color":"blue","dashed":false,"head":"none","kind":"normal","position":0.4,"tail":"none"},"zindex":0},"to":13},{"from":13,"id":57,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0.1,"color":"blue","dashed":false,"head":"none","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":16},{"from":16,"id":58,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0.1,"color":"blue","dashed":false,"head":"none","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":17},{"from":17,"id":59,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0.2,"color":"blue","dashed":false,"head":"none","kind":"normal","position":0.4,"tail":"none"},"zindex":0},"to":12},{"from":12,"id":60,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0.2,"color":"blue","dashed":false,"head":"none","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":6,"id":61,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0.1,"color":"blue","dashed":false,"head":"none","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":9,"id":62,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0.1,"color":"red","dashed":false,"head":"none","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":10},{"from":10,"id":63,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0.1,"color":"red","dashed":false,"head":"none","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":18},{"from":18,"id":64,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0.4,"color":"red","dashed":false,"head":"none","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":9,"id":65,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":-0.1,"color":"red","dashed":false,"head":"none","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":14},{"from":14,"id":66,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":-0.1,"color":"red","dashed":false,"head":"none","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":15},{"from":15,"id":67,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":-0.1,"color":"red","dashed":false,"head":"none","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":12},{"from":12,"id":68,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":-0.30000000000000004,"color":"red","dashed":false,"head":"none","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":22,"id":69,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":27},{"from":21,"id":70,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":24}],"nodes":[{"id":0,"label":{"isMath":true,"label":"E(Z)","pos":[875,454.8125],"zindex":1}},{"id":1,"label":{"isMath":true,"label":"E(Z')","pos":[945,524.8125],"zindex":1}},{"id":2,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i Z'","pos":[945,734.8125],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i Z","pos":[875,664.8125],"zindex":-10000}},{"id":4,"label":{"isMath":true,"label":"(R_0^i Z')_\\El","pos":[1155,524.8125],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"(R_0^i Z')_\\UU","pos":[1155,734.8125],"zindex":-10000}},{"id":6,"label":{"isMath":true,"label":"(R_0^i Z)_\\El","pos":[1085,454.8125],"zindex":-10000}},{"id":7,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[1085,664.8125],"zindex":0}},{"id":8,"label":{"isMath":true,"label":"Y'","pos":[455,313],"zindex":0}},{"id":9,"label":{"isMath":true,"label":"Y","pos":[595,383],"zindex":0}},{"id":10,"label":{"isMath":true,"label":"H_iF_{i-1}X","pos":[595,523],"zindex":0}},{"id":11,"label":{"isMath":true,"label":"H_iF_{i-1}X'","pos":[455,453],"zindex":-10000}},{"id":12,"label":{"isMath":true,"label":"R_0^iW(X,Y)_\\El","pos":[1085,315],"zindex":0}},{"id":13,"label":{"isMath":true,"label":"K_\\bullet(X',Y')_\\El","pos":[525,243],"zindex":0}},{"id":14,"label":{"isMath":true,"label":"K_\\bullet(X,Y)_\\El","pos":[665,315],"zindex":1}},{"id":15,"label":{"isMath":true,"label":"\\left(R_0^{i-1}X \\oplus K_\\bullet(X,Y)\\right)_\\El","pos":[875,315],"zindex":0}},{"id":16,"label":{"isMath":true,"label":"\\left(R_0^{i-1}X' \\oplus K_\\bullet(X',Y')\\right)_\\El","pos":[875,245],"zindex":0}},{"id":17,"label":{"isMath":true,"label":"R_0^iW(X',Y')_\\El","pos":[1085,245],"zindex":-10000}},{"id":18,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^iW(X,Y)","pos":[665,665],"zindex":0}},{"id":19,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^iW(X',Y)","pos":[525,595],"zindex":-10000}}],"sizeGrid":70,"title":"1"}]},"version":12} \ No newline at end of file diff --git a/Report/graphs/NaturalityDoublePullbackDefinition1.json b/Report/graphs/NaturalityDoublePullbackDefinition1.json new file mode 100644 index 0000000..efca1cc --- /dev/null +++ b/Report/graphs/NaturalityDoublePullbackDefinition1.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\\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":14,"label":{"kind":"normal","label":"E(f)_2","style":{"alignment":"right","bend":0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":1},"to":1},{"from":1,"id":15,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":1},"to":2},{"from":0,"id":16,"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":17,"label":{"kind":"normal","label":"(R_0^i Z)_\\El","style":{"alignment":"left","bend":0,"color":"blue","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":4,"id":18,"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":5},{"from":6,"id":19,"label":{"kind":"normal","label":"R_0^i\\ii_\\El","style":{"alignment":"left","bend":0,"color":"purple","dashed":false,"head":"default","kind":"normal","position":0.30000000000000004,"tail":"none"},"zindex":1},"to":3},{"from":4,"id":20,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"blue","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":5,"id":21,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"red","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":8},{"from":9,"id":22,"label":{"kind":"normal","label":"R_0^iW(g,h)_\\El","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":23,"label":{"kind":"normal","label":"\\phi_{XYZ}(\\ii)","style":{"alignment":"left","bend":-0.1,"color":"red","dashed":true,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":4,"id":24,"label":{"kind":"normal","label":"\\phi_{X'Y'Z'}(f\\circ \\ii \\circ W(g,h))","style":{"alignment":"right","bend":0.10000000000000003,"color":"blue","dashed":true,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":7,"id":25,"label":{"kind":"normal","label":"\\inj_2^{i-1}","style":{"alignment":"left","bend":0,"color":"blue","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":9},{"from":8,"id":26,"label":{"kind":"normal","label":"\\inj_2^{i-1}","style":{"alignment":"left","bend":0,"color":"red","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":3,"id":27,"label":{"kind":"normal","label":"(R_0^iZ)_p","style":{"alignment":"left","bend":0,"color":"red","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":10},{"from":0,"id":28,"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":11},{"from":11,"id":29,"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":10},{"from":2,"id":30,"label":{"kind":"normal","label":"(R_0^i Z')_p","style":{"alignment":"left","bend":0,"color":"blue","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":12},{"from":1,"id":31,"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":13},{"from":13,"id":32,"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":12},{"from":11,"id":33,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":-0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":13},{"from":16,"id":34,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":28},{"from":15,"id":35,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":31}],"nodes":[{"id":0,"label":{"isMath":true,"label":"E(Z)","pos":[1015,175],"zindex":1}},{"id":1,"label":{"isMath":true,"label":"E(Z')","pos":[1015,595],"zindex":1}},{"id":2,"label":{"isMath":true,"label":"(R_0^i Z')_\\El","pos":[1015,455],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"(R_0^i Z)_\\El","pos":[1015,315],"zindex":-10000}},{"id":4,"label":{"isMath":true,"label":"Y'","pos":[455,455],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"Y","pos":[455,315],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"R_0^iW(X,Y)_\\El","pos":[805,315],"zindex":0}},{"id":7,"label":{"isMath":true,"label":"K_\\bullet(X',Y')_\\El","pos":[595,455],"zindex":0}},{"id":8,"label":{"isMath":true,"label":"K_\\bullet(X,Y)_\\El","pos":[595,315],"zindex":1}},{"id":9,"label":{"isMath":true,"label":"R_0^iW(X',Y')_\\El","pos":[805,455],"zindex":-10000}},{"id":10,"label":{"isMath":true,"label":"(R_0^iZ)_\\UU","pos":[1155,315],"zindex":0}},{"id":11,"label":{"isMath":true,"label":"","pos":[1155,175],"zindex":0}},{"id":12,"label":{"isMath":true,"label":"(R_0^i Z')_\\UU","pos":[1155,455],"zindex":0}},{"id":13,"label":{"isMath":true,"label":"","pos":[1155,595],"zindex":0}}],"sizeGrid":70,"title":"1"}]},"version":12} \ No newline at end of file diff --git a/Report/graphs/NaturalityDoublePullbackDefinition2.json b/Report/graphs/NaturalityDoublePullbackDefinition2.json new file mode 100644 index 0000000..35619aa --- /dev/null +++ b/Report/graphs/NaturalityDoublePullbackDefinition2.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\\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":14,"label":{"kind":"normal","label":"E(f)_2","style":{"alignment":"right","bend":0.30000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":1},"to":1},{"from":1,"id":15,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":1},"to":2},{"from":0,"id":16,"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":17,"label":{"kind":"normal","label":"H_iF_{i-1}R_{i-1}^if","style":{"alignment":"left","bend":0,"color":"blue","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":18,"label":{"kind":"normal","label":"\\Cstr^{Z'}","style":{"alignment":"right","bend":0,"color":"blue","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":5,"id":19,"label":{"kind":"normal","label":"(R_0^i Z)_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":3,"id":20,"label":{"kind":"normal","label":"\\Cstr^Z","style":{"alignment":"left","bend":0,"color":"red","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":6,"id":21,"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":7},{"from":7,"id":22,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"red","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":8},{"from":6,"id":23,"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":9},{"from":9,"id":24,"label":{"kind":"normal","label":"H_iF_{i-1}g","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":8},{"from":8,"id":25,"label":{"kind":"normal","label":"H_iF_{i-1}\\inj_1^{i-1}","style":{"alignment":"left","bend":0,"color":"red","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":10},{"from":9,"id":26,"label":{"kind":"normal","label":"H_iF_{i-1}\\inj_1^{i-1}","style":{"alignment":"left","bend":0,"color":"blue","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":1},"to":11},{"from":11,"id":27,"label":{"kind":"normal","label":"H_iF_{i-1}R_{i-1}^iW(g,h)","style":{"alignment":"right","bend":0,"color":"blue","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":10},{"from":10,"id":28,"label":{"kind":"normal","label":"H_iF_{i-1}R_{i-1}^i\\ii","style":{"alignment":"right","bend":0,"color":"purple","dashed":false,"head":"default","kind":"normal","position":0.30000000000000004,"tail":"none"},"zindex":0},"to":3},{"from":7,"id":29,"label":{"kind":"normal","label":"\\phi_{XYZ}(\\ii)","style":{"alignment":"left","bend":-0.1,"color":"red","dashed":true,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":6,"id":30,"label":{"kind":"normal","label":"\\phi_{X'Y'Z'}(f\\circ \\ii \\circ W(g,h))","style":{"alignment":"right","bend":0.10000000000000003,"color":"blue","dashed":true,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":0,"id":31,"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":12},{"from":12,"id":32,"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":1,"id":33,"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":13},{"from":13,"id":34,"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":4},{"from":12,"id":35,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":-0.30000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":13},{"from":31,"id":36,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":16},{"from":33,"id":37,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":15}],"nodes":[{"id":0,"label":{"isMath":true,"label":"E(Z)","pos":[1172,35],"zindex":1}},{"id":1,"label":{"isMath":true,"label":"E(Z')","pos":[1172,455],"zindex":1}},{"id":2,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i Z'","pos":[1172,315],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i Z","pos":[1172,175],"zindex":-10000}},{"id":4,"label":{"isMath":true,"label":"(R_0^i Z')_\\UU","pos":[1312,315],"zindex":-10000}},{"id":5,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[1312,175],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"Y'","pos":[455,315],"zindex":0}},{"id":7,"label":{"isMath":true,"label":"Y","pos":[455,175],"zindex":0}},{"id":8,"label":{"isMath":true,"label":"H_iF_{i-1}X","pos":[542,175],"zindex":0}},{"id":9,"label":{"isMath":true,"label":"H_iF_{i-1}X'","pos":[542,315],"zindex":-10000}},{"id":10,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^iW(X,Y)","pos":[822,175],"zindex":0}},{"id":11,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^iW(X',Y')","pos":[822,315],"zindex":-10000}},{"id":12,"label":{"isMath":true,"label":"","pos":[1312,35],"zindex":-10000}},{"id":13,"label":{"isMath":true,"label":"","pos":[1312,455],"zindex":0}}],"sizeGrid":70,"title":"1"}]},"version":12} \ No newline at end of file diff --git a/Report/graphs/PhiXYZ-1MorphismOfBi.json b/Report/graphs/PhiXYZ-1MorphismOfBi.json index 818ea8e..f7baa33 100644 --- a/Report/graphs/PhiXYZ-1MorphismOfBi.json +++ b/Report/graphs/PhiXYZ-1MorphismOfBi.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":7,"label":{"kind":"normal","label":"H_iF_{i-1}\\inj_\\tl^{i-1}","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":8,"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":2},{"from":2,"id":9,"label":{"kind":"normal","label":"(\\inj_2)_\\UU","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":10,"label":{"kind":"normal","label":"((\\en_0^{i-1})^{-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":4,"id":11,"label":{"kind":"normal","label":"(R_0^{i-1}\\left\\{g;\\square \\right\\})_\\UU","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":12,"label":{"kind":"normal","label":"H_iF_{i-1}\\left\\{g;\\square \\right\\}","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":6,"id":13,"label":{"kind":"normal","label":"\\Cstr^Z","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":1,"id":14,"label":{"kind":"normal","label":"H_iF_{i-1}g","style":{"alignment":"left","bend":-0.30000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.4,"tail":"none"},"zindex":0},"to":6},{"from":1,"id":15,"label":{"kind":"normal","label":"\\square_\\UU","style":{"alignment":"right","bend":0.1,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5}],"nodes":[{"id":0,"label":{"isMath":true,"label":"H_iF_{i-1}(X \\tl^{i-1} K_{H_iF_{i-1}}(X,Y))","pos":[210,124],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"H_iF_{i-1}X","pos":[350,70],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"K_{H_iF_{i-1}}(X,Y)_\\UU","pos":[490,70],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\left[R_0^{i-1} X \\oplus K_{H_iF_{i-1}}(X,Y)\\right]_\\UU","pos":[630,124],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"R_0^{i-1}\\left(X \\tl^{i-1} K_\\bullet(X,Y)\\right)_\\UU","pos":[630,206],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[630,284],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i Z","pos":[210,284],"zindex":0}}],"sizeGrid":140,"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":"H_i\\left(F_{i-1}\\inj_0^{i-1}\\right)^{-1}","style":{"alignment":"left","bend":-0.2,"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":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":3,"id":8,"label":{"kind":"normal","label":"(R_0^{i-1}\\left\\{g;\\square \\right\\})_\\UU","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":9,"label":{"kind":"normal","label":"H_iF_{i-1}\\left\\{g;\\square \\right\\}","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":5,"id":10,"label":{"kind":"normal","label":"\\Cstr^Z","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":1,"id":11,"label":{"kind":"normal","label":"H_iF_{i-1}g","style":{"alignment":"left","bend":-0.30000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.4,"tail":"none"},"zindex":0},"to":5},{"from":1,"id":12,"label":{"kind":"normal","label":"\\square_\\UU","style":{"alignment":"right","bend":0.1,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":2,"id":13,"label":{"kind":"normal","label":"\\left(\\inj_2^{i-1}\\right)_\\UU","style":{"alignment":"left","bend":-0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":0,"id":14,"label":{"kind":"normal","label":"\\simeq","style":{"alignment":"right","bend":-0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1}],"nodes":[{"id":0,"label":{"isMath":true,"label":"H_iF_{i-1}(X \\tl^{i-1} K_{H_iF_{i-1}}(X,Y))","pos":[210,124],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"H_iF_{i-1}X","pos":[350,70],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"K_{H_iF_{i-1}}(X,Y)_\\UU","pos":[490,70],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"R_0^{i-1}\\left(X \\tl^{i-1} K_\\bullet(X,Y)\\right)_\\UU","pos":[630,167],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[630,269],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i Z","pos":[210,269],"zindex":0}}],"sizeGrid":140,"title":"1"}]},"version":12} \ No newline at end of file diff --git a/Report/graphs/PhiXYZFirstComponent.json b/Report/graphs/PhiXYZFirstComponent.json index f6c485e..61c8630 100644 --- a/Report/graphs/PhiXYZFirstComponent.json +++ b/Report/graphs/PhiXYZFirstComponent.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":"\\inj_\\tl^{i-1}","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":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":6,"label":{"kind":"normal","label":"R_{i-1}^i f","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","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":"X \\tl^{i-1}K_{H_iF_{i-1}}(X,Y)","pos":[300,100],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"R_{i-1}^iZ","pos":[700,100],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"R_{i-1}^i(W(X,Y))","pos":[500,100],"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":4,"label":{"kind":"normal","label":"\\inj_1^{i-1}","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":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":6,"label":{"kind":"normal","label":"R_{i-1}^i f","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","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":"X \\tl^{i-1}K_{H_iF_{i-1}}(X,Y)","pos":[300,100],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"R_{i-1}^iZ","pos":[700,100],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"R_{i-1}^i(W(X,Y))","pos":[500,100],"zindex":-10000}}],"sizeGrid":200,"title":"1"}]},"version":12} \ No newline at end of file diff --git a/Report/graphs/PhiXYZSndComponentPullback.json b/Report/graphs/PhiXYZSndComponentPullback.json index 2d5d4ad..4824dd7 100644 --- a/Report/graphs/PhiXYZSndComponentPullback.json +++ b/Report/graphs/PhiXYZSndComponentPullback.json @@ -1 +1 @@ -{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"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":1},{"from":1,"id":11,"label":{"kind":"normal","label":"(R_0^i Z)_p","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":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":"\\Cstr^Z","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":4,"id":14,"label":{"kind":"normal","label":"y","style":{"alignment":"right","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":"\\phi_{XYZ}(f)_2","style":{"alignment":"left","bend":0,"color":"black","dashed":true,"head":"default","kind":"normal","position":0.6,"tail":"none"},"zindex":0},"to":0},{"from":4,"id":16,"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":6},{"from":7,"id":17,"label":{"kind":"normal","label":"\\en_0^{i-1}","style":{"alignment":"left","bend":-0.2,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":8},{"from":8,"id":18,"label":{"kind":"normal","label":"(R_0^{i-1}f)_\\El","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":5,"id":19,"label":{"kind":"normal","label":"H_iF_{i-1}\\inj_\\tl^{i-1}","style":{"alignment":"left","bend":0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.6,"tail":"none"},"zindex":6},"to":9},{"from":9,"id":20,"label":{"kind":"normal","label":"H_iF_{i-1}R_{i-1}^if","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":6,"id":21,"label":{"kind":"normal","label":"(\\inj_2)_\\El","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":12,"id":22,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":10}],"nodes":[{"id":0,"label":{"isMath":true,"label":"E(Z)","pos":[440,280],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"(R_0^i Z)_\\El","pos":[600,280],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[600,440],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i Z","pos":[440,440],"zindex":-10000}},{"id":4,"label":{"isMath":true,"label":"Y","pos":[40,120],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"H_iF_{i-1}X","pos":[40,280],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"(K_{H_iF_{i-1}}(X,Y))_\\El","pos":[40,40],"zindex":0}},{"id":7,"label":{"isMath":true,"label":"\\left(R_0^{i-1}X \\oplus K_{H_iF_{i-1}}(X,Y)\\right)_\\El","pos":[360,40],"zindex":0}},{"id":8,"label":{"isMath":true,"label":"R_0^{i-1}(X \\tl^{i-1} K_{H_iF_{i-1}}(X,Y))_\\El","pos":[600,120],"zindex":0}},{"id":9,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i(W(X,Y))","pos":[200,440],"zindex":-10000}}],"sizeGrid":80,"title":"1"}]},"version":12} \ No newline at end of file +{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":9,"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":10,"label":{"kind":"normal","label":"(R_0^i Z)_p","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":11,"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":12,"label":{"kind":"normal","label":"\\Cstr^Z","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":4,"id":13,"label":{"kind":"normal","label":"y","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":4,"id":14,"label":{"kind":"normal","label":"\\phi_{XYZ}(f)_2","style":{"alignment":"left","bend":0,"color":"black","dashed":true,"head":"default","kind":"normal","position":0.6,"tail":"none"},"zindex":0},"to":0},{"from":4,"id":15,"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":6},{"from":7,"id":16,"label":{"kind":"normal","label":"(R_0^{i-1}f)_\\El","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":5,"id":17,"label":{"kind":"normal","label":"H_iF_{i-1}\\inj_0^{i-1}","style":{"alignment":"left","bend":0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.6,"tail":"none"},"zindex":6},"to":8},{"from":8,"id":18,"label":{"kind":"normal","label":"H_iF_{i-1}R_{i-1}^if","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":6,"id":19,"label":{"kind":"normal","label":"\\inj_2^{i-1}","style":{"alignment":"left","bend":-0.1,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":11,"id":20,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":9}],"nodes":[{"id":0,"label":{"isMath":true,"label":"E(Z)","pos":[440,222],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"(R_0^i Z)_\\El","pos":[600,222],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[600,382],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i Z","pos":[440,382],"zindex":-10000}},{"id":4,"label":{"isMath":true,"label":"Y","pos":[40,121],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"H_iF_{i-1}X","pos":[40,222],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"(K_{H_iF_{i-1}}(X,Y))_\\El","pos":[40,40],"zindex":0}},{"id":7,"label":{"isMath":true,"label":"R_0^{i-1}(X \\tl^{i-1} K_{H_iF_{i-1}}(X,Y))_\\El","pos":[600,132],"zindex":0}},{"id":8,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i(W(X,Y))","pos":[200,382],"zindex":-10000}}],"sizeGrid":80,"title":"1"}]},"version":12} \ No newline at end of file diff --git a/Report/graphs/ReflectionFGExtendedPullback.json b/Report/graphs/ReflectionFGExtendedPullback.json index 63a26ab..6244050 100644 --- a/Report/graphs/ReflectionFGExtendedPullback.json +++ b/Report/graphs/ReflectionFGExtendedPullback.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":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","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 (H_i\\eta_{i-1}\\circ 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","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":"H_i\\eta_{i-1}\\circ 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,144],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"A","pos":[232,238],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"H_iF_{i-1}(G_{i-1}X \\tl^{i-1} K(G_{i-1}X,(B,H_i\\eta_{i-1}\\circ g)))","pos":[232,340],"zindex":2}},{"id":3,"label":{"isMath":true,"label":"R_0^{i-1}(G_{i-1}X\\tl^{i-1}K_\\bullet(G_{i-1}X,(B,H_i\\eta_{i-1}\\circ g)))_\\El","pos":[693,238],"zindex":1}},{"id":4,"label":{"isMath":true,"label":"(R_0^{i-1}G_{i-1}X)_\\El \\oplus K_\\bullet(G_{i-1}X,(B,H_i\\eta_{i-1}\\circ g))_\\El","pos":[827,144],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"R_0^{i-1}(G_{i-1}X\\tl^{i-1}K(G_{i-1}X,(B,H_i\\eta_{i-1}\\circ g)))_\\UU","pos":[693,340],"zindex":1}},{"id":6,"label":{"isMath":true,"label":"(R_0^{i-1}G_{i-1}X)_\\UU \\oplus K_\\bullet(G_{i-1}X,(B,H_i\\eta_{i-1}\\circ g))_\\UU","pos":[827,479],"zindex":0}},{"id":7,"label":{"isMath":true,"label":"H_iF_{i-1}G_{i-1}X","pos":[100,479],"zindex":-10000}},{"id":8,"label":{"isMath":true,"label":"\\bullet \\oplus B","pos":[827,82],"zindex":0}},{"id":9,"label":{"isMath":true,"label":"\\bullet \\oplus H_iF_{i-1}G_{i-1}X","pos":[827,535],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12} \ No newline at end of file +{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":10,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":true,"head":"default","kind":"normal","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","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","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 (H_i\\eta_{i-1}\\circ 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","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","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":"H_i\\eta_{i-1}\\circ 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":"normal","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":7,"id":24,"label":{"kind":"normal","label":"\\simeq","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":7,"id":25,"label":{"kind":"normal","label":"\\inj_2^{i-1}","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":26,"label":{"kind":"normal","label":"\\inj_2^{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":3,"id":27,"label":{"kind":"normal","label":"\\simeq","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":5,"id":28,"label":{"kind":"normal","label":"\\simeq","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":11,"id":29,"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":30,"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":[330,150],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"A","pos":[450,270],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"H_iF_{i-1}(G_{i-1}X \\tl^{i-1} K(G_{i-1}X,(B,H_i\\eta_{i-1}\\circ g)))","pos":[450,390],"zindex":2}},{"id":3,"label":{"isMath":true,"label":"R_0^{i-1}(G_{i-1}X\\tl^{i-1}K_\\bullet(G_{i-1}X,(B,H_i\\eta_{i-1}\\circ g)))_\\El","pos":[930,270],"zindex":1}},{"id":4,"label":{"isMath":true,"label":"(R_0^{i-1}G_{i-1}X)_\\El \\oplus K_\\bullet(G_{i-1}X,(B,H_i\\eta_{i-1}\\circ g))_\\El","pos":[1050,150],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"R_0^{i-1}(G_{i-1}X\\tl^{i-1}K(G_{i-1}X,(B,H_i\\eta_{i-1}\\circ g)))_\\UU","pos":[930,390],"zindex":1}},{"id":6,"label":{"isMath":true,"label":"(R_0^{i-1}G_{i-1}X)_\\UU \\oplus K_\\bullet(G_{i-1}X,(B,H_i\\eta_{i-1}\\circ g))_\\UU","pos":[1050,510],"zindex":0}},{"id":7,"label":{"isMath":true,"label":"H_iF_{i-1}G_{i-1}X","pos":[330,510],"zindex":-10000}},{"id":8,"label":{"isMath":true,"label":"\\bullet \\oplus B","pos":[1050,90],"zindex":0}},{"id":9,"label":{"isMath":true,"label":"\\bullet \\oplus H_iF_{i-1}G_{i-1}X","pos":[1050,570],"zindex":0}}],"sizeGrid":60,"title":"1"}]},"version":12} \ No newline at end of file diff --git a/Report/graphs/ReflectionFGIsomorphismFirst.json b/Report/graphs/ReflectionFGIsomorphismFirst.json index d3646d0..04357f1 100644 --- a/Report/graphs/ReflectionFGIsomorphismFirst.json +++ b/Report/graphs/ReflectionFGIsomorphismFirst.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":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_\\tl^{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 \\tl^{i-1}K_\\bullet(G_{i-1}X,(B,H_i\\eta_{i-1}\\circ g)))","pos":[626,100],"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":3,"label":{"kind":"normal","label":"\\eta^{FG}_{i-1}","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":4,"label":{"kind":"normal","label":"F_{i-1}(\\inj_1^{i-1})","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":5,"label":{"kind":"normal","label":"\\simeq","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":6,"label":{"kind":"normal","label":"\\simeq","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","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 \\tl^{i-1}K_\\bullet(G_{i-1}X,(B,H_i\\eta_{i-1}\\circ g)))","pos":[626,100],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12} \ No newline at end of file diff --git a/Report/graphs/ReflectionFGIsomorphismSecond.json b/Report/graphs/ReflectionFGIsomorphismSecond.json index 38e7773..c316713 100644 --- a/Report/graphs/ReflectionFGIsomorphismSecond.json +++ b/Report/graphs/ReflectionFGIsomorphismSecond.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":6,"label":{"kind":"normal","label":"\\id_B","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":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":"h","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_\\tl^{i-1}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","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\\eta_{i-1}^{FG}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","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 \\tl^{i-1}K_\\bullet(G_{i-1}X,(B,H_i\\eta_{i-1}\\circ 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 +{"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":"\\id_B","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":"\\simeq","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":8,"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":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_1^{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\\eta_{i-1}^{FG}","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":13,"label":{"kind":"normal","label":"\\simeq","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":5,"id":14,"label":{"kind":"normal","label":"\\simeq","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":4,"id":15,"label":{"kind":"normal","label":"\\simeq","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3}],"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 \\tl^{i-1}K_\\bullet(G_{i-1}X,(B,H_i\\eta_{i-1}\\circ 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 diff --git a/Report/graphs/TlConstructor.json b/Report/graphs/TlConstructor.json index a32ce29..75b6eee 100644 --- a/Report/graphs/TlConstructor.json +++ b/Report/graphs/TlConstructor.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":"H_i(F_{i-1}\\inj_\\tl^{i-1})^{-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":5,"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":2},{"from":2,"id":6,"label":{"kind":"normal","label":"(R_0^{i-1}\\inj_\\tl^{i-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3}],"nodes":[{"id":0,"label":{"isMath":true,"label":"H_iF_{i-1}(R_{i-1}^i X \\tl^{i-1} Y)","pos":[177,59],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"H_iF_{i-1}(R_{i-1}^i X)","pos":[177,135],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i X)_\\UU","pos":[177,207],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"(R_0^{i-1} (R_{i-1}^i X \\tl^{i-1} Y))_\\UU","pos":[177,285],"zindex":0}}],"sizeGrid":118,"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":"H_i(F_{i-1}\\inj_1^{i-1})^{-1}","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":"\\Cstr^X","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":6,"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":3},{"from":0,"id":7,"label":{"kind":"normal","label":"\\simeq","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1}],"nodes":[{"id":0,"label":{"isMath":true,"label":"H_iF_{i-1}(R_{i-1}^i X \\tl^{i-1} Y)","pos":[177,59],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"H_iF_{i-1}(R_{i-1}^i X)","pos":[177,177],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i X)_\\UU","pos":[177,295],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"(R_0^{i-1} (R_{i-1}^i X \\tl^{i-1} Y))_\\UU","pos":[177,413],"zindex":0}}],"sizeGrid":118,"title":"1"}]},"version":12} \ No newline at end of file diff --git a/Report/graphs/TlDefOnMorphisms.json b/Report/graphs/TlDefOnMorphisms.json index 01d9334..57d4a72 100644 --- a/Report/graphs/TlDefOnMorphisms.json +++ b/Report/graphs/TlDefOnMorphisms.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":"H_i(F_{i-1}\\inj_\\tl^{i-1})^{-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":9,"label":{"kind":"normal","label":"H_iF_{i-1}R_{i-1}^ig","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":10,"label":{"kind":"normal","label":"H_iF_{i-1}(R_{i-1}^ig\\tl^{i-1}h)","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":"H_i(F_{i-1}\\inj_\\tl^{i-1})^{-1}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":1,"id":12,"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":4,"id":13,"label":{"kind":"normal","label":"(R_0^ig)_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":2,"id":14,"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":5},{"from":4,"id":15,"label":{"kind":"normal","label":"(R_0^{i-1}\\inj_\\tl^{i-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":5,"id":16,"label":{"kind":"normal","label":"(R_0^{i-1}\\inj_\\tl^{i-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":6,"id":17,"label":{"kind":"normal","label":"R_0^{i-1}(R_{i-1}^ig\\tl^{i-1}h)_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":7}],"nodes":[{"id":0,"label":{"isMath":true,"label":"H_iF_{i-1}(R_{i-1}^iX\\tl^{i-1}Y)","pos":[100,96],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^iX","pos":[376,96],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^iX'","pos":[376,237],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}(R_{i-1}^iX'\\tl^{i-1}Y')","pos":[100,237],"zindex":-10000}},{"id":4,"label":{"isMath":true,"label":"(R_0^iX)_\\UU","pos":[576,96],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"(R_0^iX')_\\UU","pos":[576,237],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"R_0^{i-1}(R_{i-1}^iX\\tl^{i-1}Y)_\\UU","pos":[812,96],"zindex":0}},{"id":7,"label":{"isMath":true,"label":"R_0^{i-1}(R_{i-1}^iX'\\tl^{i-1}Y')_\\UU","pos":[812,237],"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":8,"label":{"kind":"normal","label":"H_i(F_{i-1}\\inj_\\tl^{i-1})^{-1}","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":9,"label":{"kind":"normal","label":"H_iF_{i-1}R_{i-1}^ig","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":10,"label":{"kind":"normal","label":"H_iF_{i-1}(R_{i-1}^ig\\tl^{i-1}h)","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":"H_i(F_{i-1}\\inj_\\tl^{i-1})^{-1}","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":"\\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":4,"id":13,"label":{"kind":"normal","label":"(R_0^ig)_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":2,"id":14,"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":5},{"from":4,"id":15,"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":6},{"from":5,"id":16,"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":7},{"from":6,"id":17,"label":{"kind":"normal","label":"R_0^{i-1}(R_{i-1}^ig\\tl^{i-1}h)_\\UU","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":0,"id":18,"label":{"kind":"normal","label":"\\simeq","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":3,"id":19,"label":{"kind":"normal","label":"\\simeq","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"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}^iX\\tl^{i-1}Y)","pos":[100,62],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^iX","pos":[487,62],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^iX'","pos":[487,203],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}(R_{i-1}^iX'\\tl^{i-1}Y')","pos":[100,203],"zindex":-10000}},{"id":4,"label":{"isMath":true,"label":"(R_0^iX)_\\UU","pos":[693,62],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"(R_0^iX')_\\UU","pos":[693,203],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"R_0^{i-1}(R_{i-1}^iX\\tl^{i-1}Y)_\\UU","pos":[1024,62],"zindex":0}},{"id":7,"label":{"isMath":true,"label":"R_0^{i-1}(R_{i-1}^iX'\\tl^{i-1}Y')_\\UU","pos":[1024,203],"zindex":-10000}}],"sizeGrid":200,"title":"1"}]},"version":12} \ No newline at end of file diff --git a/Report/graphs/TlInj1MorphismOfBi.json b/Report/graphs/TlInj1MorphismOfBi.json index dc29e48..fc71b04 100644 --- a/Report/graphs/TlInj1MorphismOfBi.json +++ b/Report/graphs/TlInj1MorphismOfBi.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_\\tl^{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_\\tl^{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_i(F_{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 \\tl^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":[939,73.8125],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^{i-1} (R_{i-1}^i X \\tl^{i-1} Y))_\\UU","pos":[943.5,243.5],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}(R_{i-1}^i X \\tl^{i-1}Y)","pos":[236.5,243.5],"zindex":-10000}},{"id":4,"label":{"isMath":true,"label":"(R_0^i X)_\\UU","pos":[676,229.8125],"zindex":-10000}},{"id":5,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i X","pos":[526,228.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_\\tl^{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_\\tl^{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_i(F_{i-1}\\inj_1^{i-1})^{-1}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","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 \\tl^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},{"from":3,"id":15,"label":{"kind":"normal","label":"\\simeq","style":{"alignment":"right","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":"\\simeq","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3}],"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":[939,73.8125],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^{i-1} (R_{i-1}^i X \\tl^{i-1} Y))_\\UU","pos":[943.5,243.5],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}(R_{i-1}^i X \\tl^{i-1}Y)","pos":[236.5,243.5],"zindex":-10000}},{"id":4,"label":{"isMath":true,"label":"(R_0^i X)_\\UU","pos":[676,229.8125],"zindex":-10000}},{"id":5,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i X","pos":[526,228.8125],"zindex":-10000}}],"sizeGrid":147,"title":"1"}]},"version":12} \ No newline at end of file diff --git a/Report/graphs/TlUniversal.json b/Report/graphs/TlUniversal.json index 8a1f1af..d388f56 100644 --- a/Report/graphs/TlUniversal.json +++ b/Report/graphs/TlUniversal.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":7,"label":{"kind":"normal","label":"\\inj_\\tl^{i-1}","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":8,"label":{"kind":"normal","label":"\\{g,h\\}","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":9,"label":{"kind":"normal","label":"g","style":{"alignment":"left","bend":0.1,"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":"\\en^i_0","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":4,"id":11,"label":{"kind":"normal","label":"R_0^i\\{g,h\\}","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":3,"id":12,"label":{"kind":"normal","label":"\\inj_2","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":6,"id":13,"label":{"kind":"normal","label":"h","style":{"alignment":"left","bend":-0.1,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5}],"nodes":[{"id":0,"label":{"isMath":true,"label":"X","pos":[100,94],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"X \\tl^i Y","pos":[300,94],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"Z","pos":[300,318],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"R_0^{i-1}X \\oplus Y","pos":[514,94],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"R_0^{i-1}(X \\tl^i Y)","pos":[515,188.8125],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"R_0^i Z","pos":[514,318],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"Y","pos":[714,94],"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":"R_0^i\\inj_1^i","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\\{g,h\\}","style":{"alignment":"left","bend":0,"color":"black","dashed":true,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":6,"label":{"kind":"normal","label":"R_0^ig","style":{"alignment":"right","bend":0.30000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":3,"id":7,"label":{"kind":"normal","label":"g","style":{"alignment":"left","bend":-0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":3,"id":8,"label":{"kind":"normal","label":"\\inj_2^i","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1}],"nodes":[{"id":0,"label":{"isMath":true,"label":"R_0^iX","pos":[100,94],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"R_0^i(X \\tl^i Y)","pos":[300,94],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"R_0^iZ","pos":[300,318],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"Y","pos":[500,94],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12} \ No newline at end of file diff --git a/Report/graphs/TlUniversalMorphismIsOfBi.json b/Report/graphs/TlUniversalMorphismIsOfBi.json index 4876d9c..6de48f5 100644 --- a/Report/graphs/TlUniversalMorphismIsOfBi.json +++ b/Report/graphs/TlUniversalMorphismIsOfBi.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":"H_i(F_{i-1}\\inj^{i-1}_1)^{-1}","style":{"alignment":"left","bend":-0.1,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":7,"label":{"kind":"normal","label":"\\Cstr^X","style":{"alignment":"right","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}\\{g,h\\}","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":2,"id":9,"label":{"kind":"normal","label":"(R_0^{i-1} \\inj_\\tl^{i-1})_\\UU","style":{"alignment":"left","bend":-0.1,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":-1},"to":4},{"from":4,"id":10,"label":{"kind":"normal","label":"(R_0^i \\{g,h\\})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":3,"id":11,"label":{"kind":"normal","label":"\\Cstr^Z","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":1,"id":12,"label":{"kind":"normal","label":"H_iF_{i-1}R_{i-1}^ig","style":{"alignment":"left","bend":-0.2,"color":"black","dashed":false,"head":"none","kind":"normal","position":0.5,"tail":"none"},"zindex":-1},"to":3},{"from":2,"id":13,"label":{"kind":"normal","label":"(R_0^i g)_\\UU","style":{"alignment":"right","bend":0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5}],"nodes":[{"id":0,"label":{"isMath":true,"label":"H_iF_{i-1}(R_{i-1}^i X \\tl^{i-1} Y)","pos":[375,125],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i X","pos":[525,75],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i X)_\\UU","pos":[675,75],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i Z","pos":[375,275],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"(R_0^{i-1} (R_{i-1}^i X \\tl^{i-1} Y))_\\UU","pos":[825,125],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[825,275],"zindex":0}}],"sizeGrid":150,"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":"H_i(F_{i-1}\\inj^{i-1}_1)^{-1}","style":{"alignment":"left","bend":-0.2,"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":"\\Cstr^X","style":{"alignment":"right","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}\\{g,h\\}","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":2,"id":9,"label":{"kind":"normal","label":"(R_0^{i-1} \\inj_1^{i-1})_\\UU","style":{"alignment":"left","bend":-0.1,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":-1},"to":4},{"from":4,"id":10,"label":{"kind":"normal","label":"(R_0^i \\{g,h\\})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":3,"id":11,"label":{"kind":"normal","label":"\\Cstr^Z","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":1,"id":12,"label":{"kind":"normal","label":"H_iF_{i-1}R_{i-1}^ig","style":{"alignment":"left","bend":-0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":-1},"to":3},{"from":2,"id":13,"label":{"kind":"normal","label":"(R_0^i g)_\\UU","style":{"alignment":"right","bend":0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":0,"id":14,"label":{"kind":"normal","label":"\\simeq","style":{"alignment":"right","bend":-0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1}],"nodes":[{"id":0,"label":{"isMath":true,"label":"H_iF_{i-1}(R_{i-1}^i X \\tl^{i-1} Y)","pos":[375,125],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i X","pos":[525,75],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i X)_\\UU","pos":[675,75],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i Z","pos":[375,275],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"(R_0^{i-1} (R_{i-1}^i X \\tl^{i-1} Y))_\\UU","pos":[825,125],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[825,275],"zindex":0}}],"sizeGrid":150,"title":"1"}]},"version":12} \ No newline at end of file diff --git a/Report/graphs/Wdef.json b/Report/graphs/Wdef.json index edb4c33..a3180d1 100644 --- a/Report/graphs/Wdef.json +++ b/Report/graphs/Wdef.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":5,"label":{"kind":"normal","label":"(H_i(F_{i-1}\\inj_\\tl^{i-1})^{-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":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":2},{"from":2,"id":7,"label":{"kind":"normal","label":"\\inj_2","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":8,"label":{"kind":"normal","label":"(\\en_0^{i-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":4}],"nodes":[{"id":0,"label":{"isMath":true,"label":"H_iF_{i-1}(X \\tl^{i-1} K_{H_iF_{i-1}}(X,Y))) ","pos":[230,46],"zindex":0}},{"id":1,"label":{"isMath":true,"label":" H_iF_{i-1}X","pos":[230,138],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\left(K_{H_iF_{i-1}}(X,Y)\\right)_\\UU","pos":[230,204],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\left(R_0^{i-1}X \\oplus K_{H_iF_{i-1}}(X,Y)\\right)_\\UU","pos":[230,296],"zindex":0}},{"id":4,"label":{"isMath":true,"label":" \\left(R_0^{i-1}(X \\tl^{i-1}K_{H_iF_{i-1}}(X,Y))\\right)_\\UU","pos":[230,388],"zindex":0}}],"sizeGrid":92,"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":"(H_i(F_{i-1}\\inj_\\tl^{i-1})^{-1})","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":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":6,"label":{"kind":"normal","label":"\\simeq","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":2,"id":7,"label":{"kind":"normal","label":"\\inj_2^{i-1}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3}],"nodes":[{"id":0,"label":{"isMath":true,"label":"H_iF_{i-1}(X \\tl^{i-1} K_{H_iF_{i-1}}(X,Y))) ","pos":[230,46],"zindex":0}},{"id":1,"label":{"isMath":true,"label":" H_iF_{i-1}X","pos":[230,138],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\left(K_{H_iF_{i-1}}(X,Y)\\right)_\\UU","pos":[230,204],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"R_0^{i-1}\\left(X \\tl^{i-1}K_{H_iF_{i-1}}(X,Y)\\right)_\\UU","pos":[230,300],"zindex":0}}],"sizeGrid":92,"title":"1"}]},"version":12} \ No newline at end of file diff --git a/Report/graphs/WghMorphismOfBi.json b/Report/graphs/WghMorphismOfBi.json index 1915678..be9f8cc 100644 --- a/Report/graphs/WghMorphismOfBi.json +++ b/Report/graphs/WghMorphismOfBi.json @@ -1 +1 @@ -{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}\n\\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\\newcommand{\\inj}{\\operatorname{inj}}\n\\newcommand{\\idr}{\\operatorname{id}}\n","tabs":[{"active":true,"edges":[{"from":0,"id":10,"label":{"kind":"normal","label":"H_i(F_{i-1}\\inj_\\tl^{i-1})^{-1}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.7,"tail":"none"},"zindex":-1},"to":1},{"from":2,"id":11,"label":{"kind":"normal","label":"(\\inj_2^0)_\\UU","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":12,"label":{"kind":"normal","label":"(\\en_0^{i-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":4,"id":13,"label":{"kind":"normal","label":"R_0^i(g \\tl^{i-1}K_\\bullet(g,h))_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":3,"id":14,"label":{"kind":"normal","label":"(R_0^i g \\oplus K_\\bullet(g,h))_\\UU","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":6,"id":15,"label":{"kind":"normal","label":"(\\en_0^{i-1})_\\UU","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.10000000000000003,"tail":"none"},"zindex":0},"to":5},{"from":2,"id":16,"label":{"kind":"normal","label":"\\left[K_{H_iF_{i-1}}(g,h)\\right]_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":1,"id":17,"label":{"kind":"normal","label":"H_iF_{i-1}g","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":8},{"from":8,"id":18,"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":7},{"from":0,"id":19,"label":{"kind":"normal","label":"H_iF_{i-1}(g \\tl^{i-1}K_\\bullet(g,h))","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":9},{"from":9,"id":20,"label":{"kind":"normal","label":"H_i(F_{i-1}\\inj_\\tl^{i-1})^{-1}","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.8999999999999999,"tail":"none"},"zindex":0},"to":8},{"from":7,"id":21,"label":{"kind":"normal","label":"(\\inj_2^0)_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":1,"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":2}],"nodes":[{"id":0,"label":{"isMath":true,"label":"H_iF_{i-1}(X \\tl^{i-1}K_{H_iF_{i-1}}(X,Y))","pos":[135,44],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"H_iF_{i-1}X","pos":[197,159],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\left[K_{H_iF_{i-1}}(X,Y)\\right]_\\UU","pos":[366,159],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\left[R_0^{i-1} X \\oplus K_\\bullet(X,Y)\\right]_\\UU","pos":[603,159],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"R_0^{i-1}(X \\tl^{i-1} K_\\bullet(X,Y))_\\UU","pos":[712,44],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"R_0^{i-1}(X' \\tl^{i-1} K_\\bullet(X',Y'))_\\UU","pos":[712,390],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"\\left[R_0^{i-1} X' \\oplus K_\\bullet(X',Y')\\right]_\\UU","pos":[603,267],"zindex":-10000}},{"id":7,"label":{"isMath":true,"label":"\\left[K_{H_iF_{i-1}}(X',Y')\\right]_\\UU","pos":[366,267],"zindex":0}},{"id":8,"label":{"isMath":true,"label":"H_iF_{i-1}X'","pos":[197,267],"zindex":0}},{"id":9,"label":{"isMath":true,"label":"H_iF_{i-1}(X' \\tl^{i-1}K_{H_iF_{i-1}}(X',Y'))","pos":[135,390],"zindex":0}}],"sizeGrid":90,"title":"1"}]},"version":12} \ No newline at end of file +{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}\n\\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\\newcommand{\\inj}{\\operatorname{inj}}\n\\newcommand{\\idr}{\\operatorname{id}}\n","tabs":[{"active":true,"edges":[{"from":0,"id":8,"label":{"kind":"normal","label":"H_i(F_{i-1}\\inj_1^{i-1})^{-1}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.7,"tail":"none"},"zindex":-1},"to":1},{"from":3,"id":9,"label":{"kind":"normal","label":"R_0^i(g \\tl^{i-1}K_\\bullet(g,h))_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":2,"id":10,"label":{"kind":"normal","label":"\\left[K_{H_iF_{i-1}}(g,h)\\right]_\\UU","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":1,"id":11,"label":{"kind":"normal","label":"H_iF_{i-1}g","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":6,"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":0,"id":13,"label":{"kind":"normal","label":"H_iF_{i-1}(g \\tl^{i-1}K_\\bullet(g,h))","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":7,"id":14,"label":{"kind":"normal","label":"H_i(F_{i-1}\\inj_1^{i-1})^{-1}","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":1,"id":15,"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":2},{"from":2,"id":16,"label":{"kind":"normal","label":"\\inj_2^{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":5,"id":17,"label":{"kind":"normal","label":"\\inj_2^{i-1}","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":18,"label":{"kind":"normal","label":"\\Cstr^{W(X,Y)}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":7,"id":19,"label":{"kind":"normal","label":"\\Cstr^{W(X',Y')}","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":20,"label":{"kind":"normal","label":"\\simeq","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":7,"id":21,"label":{"kind":"normal","label":"\\simeq","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6}],"nodes":[{"id":0,"label":{"isMath":true,"label":"H_iF_{i-1}(X \\tl^{i-1}K_{H_iF_{i-1}}(X,Y))","pos":[225,45],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"H_iF_{i-1}X","pos":[405,135],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\left[K_{H_iF_{i-1}}(X,Y)\\right]_\\UU","pos":[585,135],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"R_0^{i-1}(X \\tl^{i-1} K_\\bullet(X,Y))_\\UU","pos":[765,45],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"R_0^{i-1}(X' \\tl^{i-1} K_\\bullet(X',Y'))_\\UU","pos":[765,315],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"\\left[K_{H_iF_{i-1}}(X',Y')\\right]_\\UU","pos":[585,225],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"H_iF_{i-1}X'","pos":[405,225],"zindex":0}},{"id":7,"label":{"isMath":true,"label":"H_iF_{i-1}(X' \\tl^{i-1}K_{H_iF_{i-1}}(X',Y'))","pos":[225,315],"zindex":0}}],"sizeGrid":90,"title":"1"}]},"version":12} \ No newline at end of file diff --git a/Report/header.tex b/Report/header.tex index 19e4b47..b243e3c 100644 --- a/Report/header.tex +++ b/Report/header.tex @@ -42,6 +42,7 @@ \usepackage{newunicodechar} \usepackage{txfonts} \usepackage{yade} +\usepackage{environ} \usepackage[backend=biber,style=numeric]{biblatex} \usepackage{hyperref} @@ -126,13 +127,13 @@ \node (El) at (0,1) {\El}; \draw[->] (El) -- node[anchor=east] {\ensuremath{\scriptstyle p}} (U); - \node (XU) at (1,0) {\ensuremath{#3}}; - \node (XEl) at (1,1) {\ensuremath{#1}}; + \node (XU) at (1.5,0) {\ensuremath{#3}}; + \node (XEl) at (1.5,1) {\ensuremath{#1}}; \draw[->] (XEl) -- node[anchor=west] {\ensuremath{\scriptstyle #2}} (XU); - \draw[|->] (.3,0) -- (.7,0); - \draw[|->] (.3,0.5) -- (.7,0.5); - \draw[|->] (.3,1) -- (.7,1); + \draw[|->] (.3,0) -- (1,0); + \draw[|->] (.3,0.5) -- (1,0.5); + \draw[|->] (.3,1) -- (1,1); \coordinate (base) at (.5,.4); \end{tikzpicture} @@ -169,5 +170,18 @@ % Fixing Yade green \definecolor{green}{RGB}{11,102,35} +% Environ for scaling tikz pictures +\makeatletter +\newsavebox{\measure@tikzpicture} +\NewEnviron{scaletikzpicturetowidth}[1]{% + \def\tikz@width{#1}% + \def\tikzscale{1}\begin{lrbox}{\measure@tikzpicture}% + \BODY + \end{lrbox}% + \pgfmathparse{#1/\wd\measure@tikzpicture}% + \edef\tikzscale{\pgfmathresult}% + \BODY +} +\makeatother \addbibresource{Bilibibio.bib} \ No newline at end of file