diff --git a/Report/M2Report.tex b/Report/M2Report.tex index adfc790..28f83e7 100644 --- a/Report/M2Report.tex +++ b/Report/M2Report.tex @@ -28,7 +28,7 @@ \subsection*{General Context} - Generalized Algebraic Theories a.k.a. GATs are syntactic objects introduced in 1986 by Cartmell \cite{CartmellGATs}. They enable us to describe algebraic structures that we can see as a generalization of Type Theory's inductive types. For example, we can describe the models of some type theory using a GAT. + Generalized Algebraic Theories a.k.a. GATs are syntactic objects introduced in 1986 by Cartmell \cite{CartmellGATs}. We can see them as a generalization of Type Theory's inductive types as they enable us to describe algebraic structures. For example, we can describe the models of first order logic using a GAT. A GAT is made of a list of \enquote{sorts} called a \enquote{sort specification} that describes sets, usually followed by a list of \enquote{constructors}. @@ -121,9 +121,9 @@ $\Con : \mathcal{O}$ & One sort object is called \enquote{$\Con$} \\ $\Ty : (\Gamma : \underline{\Con}) \to \mathcal{O}$ & For each object $\Gamma$ corresponding to the sort object $\Con$, another sort object called \enquote{$\Ty\;\Gamma$} \\ - $\Tm : (\Gamma : \underline{\Con}) \to (A : \underline{\Ty\;\Delta}) \to \mathcal{O}$ & - For each object $\Gamma$ corresponding to the sort object $\Con$, - and for every object $A$ corresponding to the sort object $\Ty\;\Gamma$, another sort object called \enquote{$\Tm\;\Gamma\;A$}\\ + $\Tm : (\Delta : \underline{\Con}) \to (A : \underline{\Ty\;\Delta}) \to \mathcal{O}$ & + For each object $\Delta$ corresponding to the sort object $\Con$, + and for every object $A$ corresponding to the sort object $\Ty\;\Delta$, another sort object called \enquote{$\Tm\;\Delta\;A$}\\ $\operatorname{unit} : (\Gamma : \underline{\Con}) \to \underline{\Ty\;\Gamma}$ & For each object $\Gamma$ corresponding to the sort object $\Con$, an object called "$\operatorname{unit} \Gamma$" corresponding to the sort object $\Ty\;\Gamma$\\ $\operatorname{tt}: (\Gamma : \underline{\Con}) \to \underline{\Tm\;(\operatorname{unit}\;\Gamma)}$ & @@ -243,7 +243,7 @@ \subsection{Type theory example} - We will take as a first example the sort specification of type theory presented in the introduction. The sort specification and its transformation are as follows: + Our next example is the sort specification of type theory presented in the introduction. We recall that the sort specification and its transformation are as follows: \vspace{1ex} \begin{center} @@ -279,7 +279,7 @@ We have seen in the introduction a description of a model of the type theory sort specification. We will rebuild the category of those models inductively, adding one sort at a time. - To construct those categories generically, we will define functors $H_X : \CC_{X-1} \to \Set$ that will describe the \enquote{parameters} of the sort declaration. + To construct those categories generically, we will define functors $H_i : \CC_{i-1} \to \Set$ that will describe the \enquote{parameters} of the sort declaration. \[ \boxed{\Con : \Set} @@ -550,7 +550,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 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$. This operation follows a specific universal property: For every morphism $g : X \to Z$ and $h : Y \to R_0^iZ$, there is a unique morphism $\{g;h\}$ such that the following two diagrams respectively in $\BB_i$ and $\BB_0$ commute: + \item An operator $\tl^i : \BB_i \times \BB_0 \to \BB_i$ along with two morphisms $\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$. This operation follows a specific universal property: For every morphism $g : X \to Z$ and $h : Y \to R_0^iZ$, there is a unique morphism $\{g;h\}$ such that the following two diagrams respectively in $\BB_i$ and $\BB_0$ commute: \label{sec:tlUniversalProperty} \begin{center} @@ -658,7 +658,7 @@ \end{remark} \subsection{Initialization} - In this subsection, we will recall objects built in \autoref{sec:EmptySortSpec}, and build some other objects corresponding to the empty sort specification i.e. the first step of our induction. + In this subsection, we will recall objects built in the example of \nameref{sec:EmptySortSpec}, and build some other objects corresponding to the empty sort specification i.e. the first step of our induction. \begin{itemize} \setlength\itemsep{-1ex} @@ -668,11 +668,11 @@ \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 - \[\Hom(G_0 \star,X) = \Hom(0_\TSet,X) \cong \one \cong \Hom(\star,F_0 X)\] + \[\Hom(G_0 \star,X) = \Hom(0_\TSet,X) \cong 1_\Set \cong \Hom(\star,F_0 X)\] (reminder: $\star$ is the only object of $\one$) Therefore, we have that $F_0 \vdash G_0$. \item $F_0G_0 : \one \to \one$ so $F_0G_0 = \Id_\one$ as $\one$ is terminal in $\Cat$ - \item $F_i\inj_1 = \id_\star$ which is an isomorphism + \item $F_i\inj^0_1 = \id_\star$ which is an isomorphism \end{itemize} @@ -865,7 +865,7 @@ \] \paragraph{Universal Property} - We will now show that the universal property stated in \autoref{sec:tlUniversalProperty} holds. + We will now show that the universal property stated in the introduction of this section 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 diagrams of $\BB_i$ and $\BB_0$ commute. \begin{center} @@ -883,29 +883,18 @@ \paragraph{Building morphisms} - For any two morphisms $g : X \to X'$ of $\BB_i$ and $h : Y \to Y'$ of $\BB_0$, we will create a morphism $X \tl^i Y \to X' \tl^i Y'$ as follows: + For any two morphisms $g : X \to X'$ of $\BB_i$ and $h : Y \to Y'$ of $\BB_0$, we check that the morphism $R_{i-1}^ig \tl^{i-1} h$ verifies the morphism property of $\BB_i$ in Appendix \ref{apx:tlMorphismOfBi}, so that we can define a morphism $g\tl^ih : X \tl^i Y \to X' \tl^i Y'$ such that \[ - g\tl^ih := R_{i-1}^ig \tl^{i-1} h + R_{i-1}^i\left(g\tl^ih\right) = \left(R_{i-1}^ig\right) \tl^{i-1} h \] - 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_1^i) : F_iX \to F_i(X \tl^i Y)$ is an isomorphism. - Morphisms $\BB_{i}$ are morphisms of $\BB_{i-1}$ that follow 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}$. + Morphisms $\BB_{i}$ are morphisms of $\BB_{i-1}$ that follow 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_1^i)$ is an isomorphism. + So, we just need to prove that $R_{i-1}^i(F_{i-1}\inj_1^i)$ is an isomorphism. \[ 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} @@ -928,7 +917,7 @@ The input data describing the GAT will be a sequence of finite functors $\Gamma_i : S_{i-1} \to \Set$. - We will then construct the category $S_i$ by adding a single object $\alpha_i$ to the category $S_{i-1}$, along with morphisms $f : \alpha_j \to \alpha_{i+1}$ for $f \in \Gamma_{i+1}(\alpha_j)$ and $j \leq i$. The morphisms follow the composition condition, describing that every pair of morphisms $f : \alpha_j \to \alpha_{i+1}$ and $g : \alpha_k \to \alpha_{i+1}$ (i.e. $f\in\Gamma_{i+1}(\alpha_k)$ and $g\in\Gamma_{i+1}(\alpha_j)$) and for every morphism of $S_{i}$ $h : \alpha_j \to \alpha_k$, we have $\Gamma_{i+1}(h)(f) \circ f = g$. + We will then construct the category $S_i$ by adding a single object $\alpha_i$ to the category $S_{i-1}$, along with morphisms $f : \alpha_j \to \alpha_{i+1}$ for $f \in \Gamma_{i+1}(\alpha_j)$ and $j \leq i$. The morphisms follow the composition condition, describing that every pair of morphisms $f : \alpha_j \to \alpha_{i+1}$ and $g : \alpha_k \to \alpha_{i+1}$ (i.e. $f\in\Gamma_{i+1}(\alpha_k)$ and $g\in\Gamma_{i+1}(\alpha_j)$) and for every morphism $h : \alpha_j \to \alpha_k$ of $S_{i}$, we have $\Gamma_{i+1}(h)(f) \circ f = g$. The final category is simply $S = \bigcup S_i$. @@ -1100,7 +1089,7 @@ \subsection{$W(g,h)$ morphism of $\BB_i$} \label{apx:wdefsound} - The morphism $W(g,h) = g \tl_{i-1} K_{H_iF_{i-1}}(g,h)$ is a morphism of $\BB_i$ as it makes the following diagram commute: + The morphism $R_{i-1}^iW(g,h) = g \tl_{i-1} K_{H_iF_{i-1}}(g,h)$ is a morphism of $\BB_i$ as it makes the following diagram commute: \begin{center} % YADE DIAGRAM WghMorphismOfBi.json % GENERATED LATEX @@ -1111,7 +1100,7 @@ \subsection{$\inj_1^i$ morphism of $\BB_i$} \label{apx:inj1morphism} - The morphism $\inj_1^i := \inj_1^{i-1}$ is a morphism of $\BB_i$ as it makes the following diagram commute: + The morphism $R_{i-1}^i \inj_1^i = \inj_1^{i-1}$ is a morphism of $\BB_i$ as it makes the following diagram commute: \begin{center} % YADE DIAGRAM TlInj1MorphismOfBi.json % GENERATED LATEX @@ -1120,10 +1109,9 @@ \end{center} \subsection{$\{g,h\}_i$ morphism of $\BB_i$} - \label{apx:universalpropertymorphismIsMorphism}รง - - $\{g,h\}_i := \{R_{i-1}^ig,h\}_{i-1}$ is a morphism of $\BB_i$ as it makes the following diagram commute: + \label{apx:universalpropertymorphismIsMorphism} + $R_{i-1}^i\{g,h\}_i := \{R_{i-1}^ig,h\}_{i-1}$ is a morphism of $\BB_i$ as it makes the following diagram commute: \begin{center} % YADE DIAGRAM TlUniversalMorphismIsOfBi.json % GENERATED LATEX @@ -1131,6 +1119,19 @@ % END OF GENERATED LATEX \end{center} + \subsection{$g \tl_i h$ morphism of $\BB_i$} + + \label{apx:tlMorphismOfBi} + + $(R_{i-1}^ig)\tl_{i-1}h$ is 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} \section{$W \dashv E$ adjunction} \label{apx:adjunction} @@ -1200,13 +1201,7 @@ % GENERATED LATEX \input{graphs/CompositionSecondComponent.tex} % END OF GENERATED LATEX - \end{center} - - - \todo{Justifier que la partie du haut commute, i.e. que \[ - (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 property of the pullback $E(Z)$ @@ -1215,7 +1210,7 @@ Now, the converse composition is \[ - \phi_{XYZ}^{-1} (\phi_{XYZ}(f)) = \left\{R_{i-1}^i f \circ \inj_1^{i-1} ; \square \right\} + \phi_{XYZ}^{-1} (\phi_{XYZ}(f)) = \left\{R_{i-1}^i f \circ \inj_1^{i-1} ; \square \right\}_{i-1} \] where $\square$ follows the following diagram @@ -1258,6 +1253,8 @@ &=& \left[E(f) \circ \phi_{XYZ}(\ii) \circ (g,h)\right]_1 \end{array}\] + The notation $k^+$ denotes the morphism of $\BB_i$ such that $R_{i-1}^i(k^+) = k$ when the morphism property has already been proven. + The second components are defined by the pullback properties of $E(Z)$ and $E(Z')$. The two sides that define each morphism are given separately in the two following diagrams. \begin{center} @@ -1313,9 +1310,7 @@ % 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}$, which we know to be an isomorphism from the induction hypothesis. + The first component of the isomorphism is the following isomorphism, where $\eta_{i-1}$ if the counit of the adjunction $F_{i-1} \vdash G_{i-1}$, which we know to be an isomorphism from the induction hypothesis. \begin{center} % YADE DIAGRAM ReflectionFGIsomorphismFirst.json @@ -1342,7 +1337,7 @@ % \begin{center} % % YADE DIAGRAM BiMorphismDiagram.json % GENERATED LATEX -\input{graphs/BiMorphismDiagram.tex} +%\input{graphs/BiMorphismDiagram.tex} % END OF GENERATED LATEX % % GENERATED LATEX % \input{graphs/BiMorphismDiagram.tex} @@ -1381,3 +1376,10 @@ + + + + + + + diff --git a/Report/graphs/CompositionSecondComponent.json b/Report/graphs/CompositionSecondComponent.json index 945dae5..7ab7863 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":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 +{"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":"right","bend":0.1,"color":"black","dashed":true,"head":"default","kind":"normal","position":0.4,"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/PhiXYZSndComponentPullback.json b/Report/graphs/PhiXYZSndComponentPullback.json index 4824dd7..7d62df0 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":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 +{"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_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}^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":[409,222],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"(R_0^i Z)_\\El","pos":[569,222],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[569,375],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i Z","pos":[409,375],"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":[569,132],"zindex":0}},{"id":8,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i(W(X,Y))","pos":[125,375],"zindex":-10000}}],"sizeGrid":80,"title":"1"}]},"version":12} \ No newline at end of file diff --git a/Report/graphs/ReflectionFGIsomorphismFirst.json b/Report/graphs/ReflectionFGIsomorphismFirst.json index 04357f1..f64995f 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":"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 +{"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_{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 c316713..d5ca810 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":"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 +{"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_{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}","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/Wdef.json b/Report/graphs/Wdef.json index a3180d1..8ac46b3 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":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 +{"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