From b3af01088285b07251af15f8c5c7552e9315ffaa Mon Sep 17 00:00:00 2001 From: Samy Avrillon Date: Fri, 2 Aug 2024 11:41:32 +0200 Subject: [PATCH] Replaced a lot of oplus to tl --- Report/M2Report.tex | 342 +++++++++++++++---------------- Report/graphs/D1.json | 2 +- Report/graphs/D2.json | 2 +- Report/graphs/D3a.json | 2 +- Report/graphs/D3b.json | 2 +- Report/graphs/D4.json | 2 +- Report/graphs/D5.json | 2 +- Report/graphs/D6.json | 2 +- Report/graphs/D8.json | 2 +- Report/graphs/G1.json | 2 +- Report/graphs/TlConstructor.json | 1 + Report/graphs/TlUniversal.json | 1 + Report/graphs/Wdef.json | 1 + Report/header.tex | 1 + 14 files changed, 179 insertions(+), 185 deletions(-) create mode 100644 Report/graphs/TlConstructor.json create mode 100644 Report/graphs/TlUniversal.json create mode 100644 Report/graphs/Wdef.json diff --git a/Report/M2Report.tex b/Report/M2Report.tex index 902fec9..9c7b3ba 100644 --- a/Report/M2Report.tex +++ b/Report/M2Report.tex @@ -118,7 +118,7 @@ \paragraph{Structure of the proof} - We will only only formalize the transformation for \emph{sort specification} (i.e. lists of sort declaration). We can add constructors on a later step, as described in \autoref{sec:constructors2trans}. + We will only only formalize the transformation for \emph{sort specification} (i.e. lists of sort declaration). We will show how we take into account the constructors in \autoref{sec:constructors2trans}. This proof is a big induction on the number of sorts taken into account. At each step, we will add a new sort declaration, represented by a functor $H_i$ described later \inlinetodo{MISSING REF}. @@ -128,46 +128,36 @@ \item The category of models of the GAT $\CC_i$ \item The category of models of the transformed GAT $\BB_i$ \item A functor $R_{i-1}^i : \BB_i \to \BB_{i-1}$ and $R_0^i : \BB_i \to \BB_0$, taking track of the fixed sort specification of the transformed GAT. \inlinetodo{Mal Dit, est-ce nécessaire ?} - \item An operator $\tl^i : \BB_i \times \BB_0 \to \BB_i$ along with morphisms $\inj_1^i : X \to X \tl Y$ + \item An bifunctor $\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$, and an isomorphism $\en_{i-1}^i : R_{i-1}^i (X \tl^i Y) \to (R_{i-1}^i X) \tl^{i-1} Y$. This bifunctor 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: + \begin{center} + % YADE DIAGRAM TlUniversal.json + % GENERATED LATEX + \input{graphs/TlUniversal.tex} + % END OF GENERATED LATEX + \end{center} + + where $\en_0^i$ is the composition $\en_0^1 \circ R_0^1\en_1^2 \circ \dots \circ R_0^{i-1}\en_{i-1}^i : R_0^i(X \tl^i Y) \to (R_0^iX) \oplus Y = (R_0^iX)\tl^0 Y$. + + \todo{Faut indiquer $\oplus = \tl^0$ à un moment :/} + \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_1$ is an isomorphism - \item A proof that \end{itemize} - We will construct both categories $\CC$ and $\BB$ sort declaration by sort declaration in one big recursive process. At each step, we will build the categories $\CC_i$ and $\BB_i$, the adjunction $F_i \vdash G_i$, and keep some invariants that will be stated in \autoref{sec:hypotheses}. - - At the i-th recursion step, we will build the category $\CC_i$ which is the category of models of the $i$ first sorts of the sort specification. Likewise, $\BB_i$ will be the category of models of the 2-sorted $i$ first sorts of the sort specification. - - The overall recursive construction of the categories and of the adjunctions $F_i \vdash G_i$ is given below. - + Here is a figure that describes the recursive construction of some of the above objects + \begin{center} + % YADE DIAGRAM G1.json + % GENERATED LATEX + \input{graphs/G1.tex} + % END OF GENERATED LATEX + \end{center} \subsection{Preliminaries} - \paragraph{Category of models of the two-sort sort specification} - - The usual way of defining the category of models of the two-sort specification $\BB_0$ is by taking the category of families of sets. However, we will rather use a the category of models of the two-sort specification the category $\TSet$ of presheaves over the category with one arrow. - - In the rest of the document, we will denote this category with one arrow as $\TT$. The objects and arrow of this category are pictured below. - - \begin{center} - % YADE DIAGRAM G0.json - % GENERATED LATEX - \input{graphs/G0.tex} - % END OF GENERATED LATEX - \end{center} - - With this formalisation, a model of the two-sort GAT is a functor $X : \TSet$, such that - \begin{itemize} - \item $X_\UU$ is the set of the \enquote{sort objects} - \item For each sort object $\Gamma \in X_\UU$, the set of objects corresponding to the sort object is $X_p^-1(\{\Gamma\}) \subset X_\El$ - \end{itemize} - - Therefore the categories of models of the transformed GATs will be built atop of this category $\BB_0 = \TSet$. - - \paragraph{Grothendieck Construction} + \paragraph{Grothendieck Construction} For a category $\mathcal{C}$ and a functor $F : \mathcal{C} \to \Cat$, the Grothendieck construction is a category whose objects are pairs of \begin{itemize} \item $X$ an object of $\mathcal{C}$ @@ -193,6 +183,29 @@ We will often concatenate the two method above to create from a category $\mathcal{C}$ and a functor $H : \mathcal{C} \to \Set$ a new category $(X : \mathcal{C}) \times \left(\Set\middle/H(X)\right)$. + \paragraph{Category of models of the two-sort sort specification} + + The usual way of defining the category of models of the two-sort specification $\BB_0$ is by taking the category of families of sets. However, we will rather use a the category of models of the two-sort specification the category $\TSet$ of presheaves over the category with one arrow. + + In the rest of the document, we will denote this category with one arrow as $\TT$. The objects and arrow of this category are pictured below. + + \begin{center} + % YADE DIAGRAM G0.json + % GENERATED LATEX + \input{graphs/G0.tex} + % END OF GENERATED LATEX + \end{center} + + With this formalisation, a model of the two-sort GAT is a functor $X : \TSet$, such that + \begin{itemize} + \item $X_\UU$ is the set of the \enquote{sort objects} + \item For each sort object $\Gamma \in X_\UU$, the set of objects corresponding to the sort object is $X_p^-1(\{\Gamma\}) \subset X_\El$ + \end{itemize} + + Therefore the categories of models of the transformed GATs will be built atop of this category $\BB_0 = \TSet$. + + \todo{Rewrite this part explaining the correspondance} + \paragraph{$\Hbar$ functor} Where $\Hbar_A$ is a functor $(X:C) \times (\Set/A(X)) \to \TSet$ defined as @@ -204,81 +217,79 @@ \begin{remark} This functor can be constructed using the formal construction of the Grothendieck construction as a pullback in the category of categories $\Cat$ \end{remark} + + \subsection{Initialization} + In the first step, corresponding to an empty sort specification, the objects are defined as follows: + + \begin{itemize} + \setlength\itemsep{-1ex} + \item $\CC_i$ is $\one$, the category with only one object and one morphism (i.e. the terminal category of $\Cat$), because the empty sort specification only has one model. \inlinetodo{Isn't it up to isomorphism ?} + \item $\BB_i$ is $\TSet$, the category of sorts of the ($\mathcal{O},\El$ sort specification) + \item $\tl^0 : \BB_0 \times \BB_0 \to \BB_0$ is the coproduct of $\TSet$, with $\inj_\tl^0 : X \to X \oplus Y$ being the first injector of the coproduct. We will also denote as $\inj_2^0$ the second injector of this coproduct. \inlinetodo{Est-ce que ça pose problème de parler de \emph{the} coproduct ?} + \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 With $\star$ being the object of $\one$, and for $X$ an object of $\TSet$, we have + \[\Hom(G_0 \star,X) = \Hom(0_\TSet,X) \cong 1 \cong \Hom(\star,F_0 X)\] + Therefore, we have that $F_0 \vdash G_0$ \inlinetodo{Are the iso/equiv equalities correct ?} + \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 + \end{itemize} + \subsection{Constructing the categories} - We will construct both categories $\CC$ and $\BB$ sort declaration by sort declaration in one big recursive process. At each step, we will build the categories $\CC_i$ and $\BB_i$, the adjunction $F_i \vdash G_i$, and keep some invariants that will be stated in \autoref{sec:hypotheses}. + In this part, i will show how we construct recursively both categories $\CC_i$ and $\BB_i$, along with the functor $R_{i-1}^i : \BB_i \to \BB_{i-1}$. We will use the loop invariants that we expressed in the introduction of this section. - At the i-th recursion step, we will build the category $\CC_i$ which is the category of models of the $i$ first sorts of the sort specification. Likewise, $\BB_i$ will be the category of models of the 2-sorted $i$ first sorts of the sort specification. - - The overall recursive construction of the categories and of the adjunctions $F_i \vdash G_i$ is given below. - - \begin{center} - % YADE DIAGRAM G1.json - % GENERATED LATEX - \input{graphs/G1.tex} - % END OF GENERATED LATEX - \end{center} - - The first step of our recursion is the trivial adjunction $\lambda . \star \vdash \lambda . 1$ between the categories $\BB_0 = \TSet$ and $\CC_0 = 1$, the category with one object and one morphism (i.e. the terminal element of $\Cat$). $\lambda. \star$ is the terminal morphism of this object, and its right adjoint sends the only object of $1$ to the terminal object of the category $\TSet$. - - The functors $R_{i-1}^i$ are the forgetful monadic functors that forget about the $i$-th sort contsructor. They have a left adjoint denoted $L_{i-1}^i$. - As we can compose the adjunctions $R_0^1$,$R_1^2$,...,$R_{i-1}^i$, we will use the two following adjunctions - \[\begin{array}{c} - R_0^i = R_{0}^{i-1} \circ R_{i-1}^{i} = R_{0}^{1} \circ ... \circ R_{i-1}^{i}\\ - L_0^i = L_{i-1}^{i} \circ L_{0}^{i-1} = L_{i-1}^{i} \circ ... \circ L_{0}^{1} - \end{array}\] + In order to construct the categories, we need some object describing the specific sort we are adding to the categories. This object is a specific functor $H_i : \CC_{i-1} \to \Set$. We suppose that those $H_i$ functors are given. \begin{remark} - There is also an adjunction chain between $\CC_0$,$\dots$,$\CC_{i-1}$,$\CC_i$, but we don't use it in the proof. + There is a way of getting the functor $H_i$ from the syntax, which is described in \autoref{sec:HiFromSyntax}. \end{remark} \subsubsection{Constructing $\CC_i$} - We construct the category $\CC_i$ as the following pair: + We construct the category $\CC_i$ as the following Grothendieck pair: \[ \CC_i = (X : \CC_{i-1}) \times \left(\Set\middle/H_i(X)\right) = (X : \CC_{i-1}) \times \left(\Set^{H_i(X)}\right) \] - and where $H_i$ is a specific functor $\CC_{i-1} \to \Set$, such that $H_i(X)$ is the set of parameters for the construction of the new sort. + and where $H_i$ is the specific functor described above. \todo{Do we need this functor to be representable. If so, precise it} \paragraph{$H_i$ functors for our Type Theory example} - Let us give an example of those $H_i$ objects for our type theory example. We begin with + Let us now give an example of those $H_i$ objects for our type theory example. + + We begin with the following functor, corresponding to the sort declaration $\boxed{\Con : \Set}$ \[ - H_1(\star) = 1 \in \operatorname{Obj}(\Set) + H_1(\star) = 1 \in \operatorname{Obj}(\Set) \] which corresponds to the fact that $\Con$ takes no parameter. - Therefore $\CC_1 = 1 \times \Set^1 = \Set$, and the set of a model corresponds to \enquote{the set of contexts}. + Therefore $\CC_1 = 1 \times \Set^1 = \Set$, which is as expected: a model is a set. - Then, we take the functor $H_2(X_\Con) = X_\Con$ (this means, that types need \emph{one} context to be built). + Then, we take the functor $H_2(X_\Con) = X_\Con$, corresponding to the sort declaration $\boxed{\Ty : (\Gamma : \Con) \to \Set}$ (this means, that types need \emph{one} context to be built). - Therefore $\CC_2 = (X:\Set) \times \Set^X \cong \FamSet$, families of sets. + Therefore $\CC_2 = (X:\Set) \times (\Set/X) \simeq (X:\Set) \times (\Set^X) = \FamSet$, a model is a family of sets. - Finally, we take the functor $H_3(X_\Con,X_\Ty) = \sum_{\Gamma : X_\Con}X_\Ty(\Gamma)$ (this means that terms need \emph{one} context, and \emph{one} type of that context). + Finally, we take the functor $H_3(X_\Con,X_\Ty) = \sum_{\Gamma : X_\Con}X_\Ty(\Gamma)$, that corresponds to the sort declaration $\boxed{\Tm : (\Delta : \Con) \to (A : \Ty\;\Delta) \to \Set}$ (this means that terms need \emph{one} context, and \emph{one} type of that context). - The final category $\CC_3$ is composed of triples $(X_\Con: \Set, X_\Ty : X_\Con \to \Set, X_\Tm : (\Delta: X_\Con) \to X_\Ty(\Delta) \to \Set)$ - - \begin{remark} - There is a way of getting the functor $H_i$ from the syntax, which is given in \autoref{sec:CtoSSetFiore}. - \end{remark} + An object of that final category $\CC_3$ is a triple $(X_\Con: \Set, X_\Ty : X_\Con \to \Set, X_\Tm : (\Delta: X_\Con) \to X_\Ty(\Delta) \to \Set)$ \subsubsection{Constructing $\BB_i$} - \paragraph{The category} We construct the category $\BB_i$ as follows. + We construct the category $\BB_i$ as follows. An object of $\BB_i$ is \begin{itemize} \item an object $X$ of $\BB_{i-1}$ - \item a \enquote{sort constructor} $\Cstr_i$ as a function $H_i(F_{i-1}X) \to (R_0^{i-1}X)_\UU$ + \item a \enquote{sort constructor} $\Cstr$ as a function $H_iF_{i-1}X \to (R_0^{i-1}X)_\UU$ \newline - where $H_i$ is the functor $\CC_{i-1} \to \Set$ that describe the sort constructor being processed, and $F_{i-1}$ is the right part of the adjunction $\BB_{i-1} \to \CC_{i-1}$ that we are defining recursively at the same time. - This $H_i$ functor will be so that $H_i \circ F_{i-1} \circ \inj_1^{i-1}$ is an isomorphism. \inlinetodo{Pas déclaré ici, c'est grâve ?} + where $H_i$ is the functor $\CC_{i-1} \to \Set$ described above and $F_{i-1}$ is the right part of the adjunction $\BB_{i-1} \to \CC_{i-1}$ that we are defining recursively at the same time. \end{itemize} + If we have an object $X$ of $\BB_i$, the first component is denoted as $R_{i-1}^iX$, and the second component is denoted as $\Cstr^X : R_{i-1}^i \to (R_0^iX)_\UU$. - A morphism $(X,\Cstr_i) \to (X',\Cstr'_i)$ of $\BB_i$ is a morphism $f : X \to X'$ in $\BB_{i-1}$ such that the following diagram commutes. + A morphism $X \to X'$ of $\BB_i$ is a morphism $f : R_{i-1}^iX \to R_{i-1}^iX'$ in $\BB_{i-1}$ such that the following diagram commutes. \begin{center} % YADE DIAGRAM D1.json @@ -287,62 +298,15 @@ % END OF GENERATED LATEX \end{center} + For a morphism $f : X \to X'$ of $\BB_i$, we denote as $R_{i-1}^if$ the underlying morphism $R_{i-1}^i X \to R_{i-1}^i X'$. + Identities and compositions are that of the category $\BB_{i-1}$, and categorical equalities are trivially derived from the diagram above. - \paragraph{The adjunction} - We also define a functor $R_{i-1}^i : \BB_i \to \BB_{i-1}$ that sends objects and morphisms to their first component. This functor is a \emph{right adjoint} of another functor we call $L_{i-1}^i$. - - We will also denote $\eta_i^j : \mathbf{1} \to R_i^j L_i^j$ and $\varepsilon_i^j : L_i^j R_i^j \to \mathbf{1}$ to be the unit and counit of the adjunction $R_i^j \vdash L_i^j$. - - \paragraph{The coproduct} - For an object $X$ in $\BB_i$ and $Y$ in $\BB_0$, there is a coproduct $X \oplus_i L_0^i Y$ in the category $\BB_{i-1}$. We will denote as $\inj_1^i : X \to X \oplus L_0^iY$ (resp. $\inj_2^i : L_0^iY \to X \oplus L_0^iY$) the first (resp. second) injector of the coproduct of $\BB_i$. For every morphism $f : X \to Z$ and $g : L_0^iY \to Z$, we will denote with $\{f;g\}$ the unique morphism from $X \oplus L_0^iY$ to $Z$ such that $\{f;g\} \circ \inj^i_1 = f$ and $\{f;g\} \circ \inj^i_2 = g$. - - \begin{remark} - This adjunction and the existence of a coproduct comes from seeing $\BB_i$ being a category of algebras in $\BB_{i-1}$ over the morphism $inj_1 : G_{i-1}O_i \to G_{i-1}O_i \oplus L_0^{i-1} y\UU$. \inlinetodo{Ça ne marche plus du coup :/} - \end{remark} - - - \subsection{Induction Hypotheses} - - In order to build and prove the adjunction, we will state some recurrence invariants that we will prove after having built objects. - - \begin{property}[H1] - - The canonical morphism - \[ - \simpleArrow{R_{i-1}^i X \oplus L_0^{i-1} Y}{\left\{R_{i-1}^i \inj_1^i ; R_{i-1}^i \inj_2^i \circ \eta_{i-1}^i\right\}}{R_{i-1}^i(X \oplus_i L_0^i Y)} - \] - that we will denote as $\en_{i-1}^i$ is an isomorphism. - - Its recursive version is the following isomorphism, denoted as $\en_0^i$ - \[ - \simpleArrow{ R_{0}^i X \oplus_0 Y}{\left\{R_0^i \inj_1^i ; R_0^i \inj_2^i \circ \eta_0^i\right\}}{R_0^i(X \oplus_i L_0^i Y)} - \] - \end{property} - - \begin{property}[H3] - \[ - \simpleArrow{F_i X}{F(\inj_1^i)}{F_i(X \oplus L_0^i Y)} - \] - is an isomorphism. - - We will often this equality along with the $F_i \vdash G_i$ adjunction (for an object $O$ in $\CC_i$) - \[ - \Hom(G_i O, X) \cong \Hom(O, F_i X) \cong \Hom(O, F_i(X \oplus L_0^i Y)) \cong \Hom(G_i O, X \oplus L_0^i Y) - \] - - This new isomorphism is the following: - \[ - \simpleArrow{\Hom(G_i O, X)}{(inj_1^i \circ \dash)}{\Hom(G_i O,X \oplus L_0^i Y)} - \] - - \todo{Du coup techniquement, c'est une propriété de $H_i$. Faut réussir que c'est \emph{parce que} $H_i$ est représentable que l'on peut déduire H3' de H3.} - - \end{property} + $R_{i-1}^i$ acts on objects and morphisms, and therefore creates a functor $\BB_i \to \BB_{i-1}$. \subsection{Constructing the functors} - In order to use all the power of the recurrence, we will build the $F_i \vdash G_i$ adjunction using the $F_{i-1} \vdash G_{i-1}$ adjunction, following the diagram below. + Build the $F_i \vdash G_i$ adjunction using the two functors of the $F_{i-1} \vdash G_{i-1}$ adjunction, following the diagram below. \begin{center} % YADE DIAGRAM G2.json @@ -351,34 +315,39 @@ % END OF GENERATED LATEX \end{center} - \todo{$G_{i-1} \times \id$ et son compère, c'est bien legit ?} - - The first part $G_{i-1} \times \id \dashv F_{i-1} \times \id$ is proven and defined as an adjunction from the previous step of the recurrence. + Where + \[ + (F_{i-1} \times \id)(X,(Y,y)) = (F_{i-1}X,(Y,y)) + \] + and + \[ + (G_{i-1} \times \id)(X,(Y,y)) = (G_{i-1}X,(Y,H_i\eta_{i-1} \circ y)) + \] + \todo{Définir $\eta_{i-1}$ ici !} + \todo{Plus de précision sur ces constructions ?} + \todo{Expliquer pourquoi $(F_{i-1} \times \id) \vdash (G_{i-1} \times \id)$ est une adjonction} \subsubsection{W definition} - We define a functor $W : \left(X : \BB_{i-1}\right) \times \Set/H_i(F_{i-1}X) \to \BB_{i}$ + We define a functor $W : \left(X : \BB_{i-1}\right) \times \Set/H_iF_{i-1}X \to \BB_{i}$ The action on objects is as follows: \[ - W(X,Y) := \left(X \oplus L_0^{i-1} \Hbar_{H_iF_{i-1}}(X,Y), \widetilde{\inj_2} \right) + W(X,Y) := \left(X \tl^{i-1} K_{H_iF_{i-1}}(X,Y), \widetilde{\inj_2} \right) \] - With $\widetilde{\inj_2}$ being defined by \inlinetodo{Changer les noms des hypothèses H3' et H1r} - \[ - \begin{array}{lcl} - H_iF_{i-1}(X \oplus L_0^{i-1} \Hbar_\bullet(X,Y))) - & \to^{\text{H3'}} & H_i(F_{i-1}X)\\ - & = & \left(\Hbar_{H_iF_{i-1}}(X,Y)\right)_\UU \\ - & \to^{\inj_2^0} & \left(R_0^{i-1}X \oplus \Hbar_\bullet(X,Y)\right)_\UU \\ - & \to^{\text{H1r}} & \left(R_0^{i-1}(X \oplus L_0^{i-1}\Hbar_\bullet(X,Y))\right)_\UU - \end{array} - \] + With $\widetilde{\inj_2}$ being defined by the composition + \begin{center} + % YADE DIAGRAM Wdef.json + % GENERATED LATEX + \input{graphs/Wdef.tex} + % END OF GENERATED LATEX + \end{center} - The action on a morphism $(g,h)$ from $(X,Y)$ to $(X',Y')$ is the following: + The action on a morphism $(g,h)$ from $(X,(Y,y))$ to $(X',(Y',y'))$ is the following: \[ - W(g,h) := \left(g \oplus L_0^{i-1} \Hbar_{H_iF_{i-1}}(g,h)\right) + W(g,h) := \left(g \tl^{i-1} K_{H_iF_{i-1}}(g,h)\right) \] It is indeed a morphism from $\BB_{i}$ as it makes the following diagram commute. @@ -396,7 +365,7 @@ The action on objects is \[ - E(X) = (R_{i-1}^i X, (A,h)) + E(X) = (R_{i-1}^i X, (A,h)) \] Where $(A,h)$ is defined as the following pullback: @@ -433,7 +402,7 @@ Let $f$ be in $\Hom(W(X,Y),Z)$. We want to construct $\phi_{XYZ}(f) : (X,Y) \to E(Z)$. - The first component of $\phi_{XYZ}(f)$ is $R_{i-1}^i f \circ inj_1^{i-1} : X \to R_{i-1}^i Z$, with $R_{i-1}^i f$ being a morphism of $\BB_{i-1}$ from $R_{i-1}^i(W(X,Y)) = X \oplus_{i-1} L_0^{i-1}$ to $R_{i-1}^i Z$. + The first component of $\phi_{XYZ}(f)$ is $R_{i-1}^i f \circ inj_\tl^{i-1} : X \to R_{i-1}^i Z$, with $R_{i-1}^i f$ being a morphism of $\BB_{i-1}$ from $R_{i-1}^i(W(X,Y)) = X \tl^{i-1}K_{H_iF_{i-1}}(X,Y)$ to $R_{i-1}^i Z$. The second component is defined through the universal property of the pullback defined by $E(Z)$ according to the following diagram: @@ -448,7 +417,8 @@ Now, we take $(g,h)$ a morphism from $(X,Y)$ to $E(Z)$. - We define $\phi^{-1}_{XYZ}(g,h)$ as a morphism of $\BB_i$ from $W(X,Y)$ to $Z$, i.e. a morphism of $\BB_{i-1}$ from $X \oplus_{i-1} L_0^{i-1} \Hbar (X,Y)$ to $R_0^{i-1}(Z)$ that makes a certain diagram commute: + We define $\phi^{-1}_{XYZ}(g,h)$ as a morphism of $\BB_i$ from $W(X,Y)$ to $Z$, i.e. a morphism of $\BB_{i-1}$ from $X \tl^{i-1} K_{H_iF_{i-1}} (X,Y)$ to $R_{i-1}^i(Z)$ that is built using the universal property of $\tl^{i-1}$ + \todo{Describe the initial property} \[ \phi^{-1}_{XYZ}(g,h) := \left\{g ; \varepsilon_0^i \circ L_0^{i-1} \square \right\} \] @@ -465,7 +435,7 @@ This is indeed a morphism of $\BB_i$ from $W(X,Y)$ to $Z$ as it makes the following diagram commute \begin{center} - % YADE DIAGRAM D8.json + % YADE DIAGRAM D8.json % GENERATED LATEX \input{graphs/D8.tex} % END OF GENERATED LATEX @@ -480,30 +450,29 @@ The proof is given in \autoref{apx:FG-refl}. - \subsection{Proof of the hypotheses} - \subsubsection{Proof of H1} + \subsection{Other objects} + \subsubsection{Constructing $\tl^i$} - \todo{Relire + réeexpliquer pourquoi ça prouve} \label{sec:coproductConstr} - We will define the sums of the form $X \oplus_i L_0^i Y$ in $\BB_i$. + \paragraph{Constructing the objects} + We will define the $\tl^i$ bifunctor of two objects $X$ from $\BB_i$ and $Y$ from $\BB_0$ as follows: \[ - X \oplus_i L_0^i Y := \left(R_{i-1}^i X \oplus_{i-1} L_0^{i-1} Y, (R_0^{i-1} \inj_1^{i-1})_\UU \circ \Cstr_i^X \circ (H_iF_{i-1}\inj_1^{i-1})^{-1}\right) + 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) \] - - Here, $(\inj_1^{i-1} \circ \dash)^{-1}$ is the inverse of the isomorphism of hypothesis H3', and - + The constructor goes as follows: - \[ - H_iF_{i-1}(R_{i-1}^i X \oplus_{i-1} L_0^{i-1} Y) \equiv - H_iF_{i-1}(R_{i-1}^i X) \to - (R_0^{i-1} X)_\UU \to - (R_0^i (R_{i-1}^i X \oplus_{i-1} L_0^{i-1} Y))_\UU - \] - The first injector $X \to X \oplus_i L_0^i Y$ is defined as follows: + \begin{center} + % YADE DIAGRAM TlConstructor.json + % GENERATED LATEX + \input{graphs/TlConstructor.tex} + % END OF GENERATED LATEX + \end{center} + + The injector $\inj_\tl^i : X \to X \tl^i Y$ is defined as follows: \[ - \inj_1^i := \inj_1^{i-1} : R_{i-1}^i X \to R_{i-1}^i (X \oplus_i L_0^i Y) = R_{i-1}^i X \oplus_{i-1} L_0^{i-1} Y + \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 \] It is a morphism of $\BB_i$ as it makes the following diagram commute: @@ -515,20 +484,18 @@ % END OF GENERATED LATEX \end{center} + \paragraph{Universal Property} + We will now show that that the universal property stated holds. + To that extent, 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. - The second injector is defined as follows: - \[ - \inj_2^i := (\varepsilon_i \oplus_i \id_{L_0^i Y}) \circ L_{i-1}^i \inj_2^{i-1} - \] + \begin{center} + % YADE DIAGRAM TlUniversal.json + % GENERATED LATEX + \input{graphs/TlUniversal.tex} + % END OF GENERATED LATEX + \end{center} - Where $\varepsilon_i$ is the counit of the adjunction $R_{i-1}^i \vdash L_{i-1}^i$, going from $L_{i-1}^i R_{i-1}^i X$ to $X$. - - This goes from $L_0^i Y = L_{i-1}^i L_0^{i-1} Y$ to $L_{i-1}^i(R_{i-1}^i X \oplus_{i-1} L_0^{i-1} Y)$, which is equivalent to $L_{i-1}^i R_{i-1}^i X \oplus_i L_0^i Y$ as $L_{i-1}^i$ is a left-adjoint functor and therefore it preserves colimits; then goes to $X \oplus_i L_0^i Y$. - - We will now show that this definition is actually a definition of the coproduct in $\BB_i$. - To that extent, we take two objects $X$ and $Z$ in $\BB_i$, $Y$ in $\TSet$ and two morphisms of $\BB_i$ $\varphi_1 : X \to Z$ and $\varphi_2 : L_0^i Y \to Z$. - - We define $\{\varphi_1 ; \varphi_2\}_{i } = \{R_{i-1}^i \varphi_1 ; R_{i-1}^i \varphi_2 \circ \eta^i_{L_0^{i-1} Y}\}_{i-1}$ a morphism of $\BB_i$ as it makes the following diagram commute: + We define $\{g ; h\}_i = \{R_{i-1}^i g ; h\}_{i-1}$ a morphism of $\BB_i$ as it makes the following diagram commute: \begin{center} % YADE DIAGRAM D5.json @@ -537,13 +504,11 @@ % END OF GENERATED LATEX \end{center} + With this definition, the isomorphism $\en_{i-1}^i : R_{i-1}^i(X \tl^i Y) \to (R_{i-1}^i X) \tl^{i-1} Y$ is simply the identity morphism. - \todo{Justifier $R_{i-1}^i(\varepsilon_i \oplus_i \id_{L_0^i Y}) = R_{i-1}^i \varepsilon_i \oplus_{i-1} \id_{L_0^{i-1} Y}$ (with H1 ?)} - - \subsubsection{Proof of H3} - - We need to prove that, for any objects $(X,\Cstr)$ in $\BB_i$ and $Y$ in $\TSet$, that the morphism - $F_i(\inj_1^i) : F_i(X,\Cstr) \to F_i((X,\Cstr) \oplus L_0^i Y)$ is an isomorphism. + \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. We know from \autoref{sec:coproductConstr} that $\inj_1^i := \inj_1^{i-1}$ as a morphism of $\BB_{i}$ is a morphism $\BB_{i-1}$ that verifies some equalities. @@ -697,6 +662,9 @@ This equality allows us to construct the $\Gamma_i$ functors from the final $S$ category. \end{remark} + \subsection{Consructing the $H_i$ functors from the syntax} + \label{sec:HiFromSyntax} + \section{Summary} \lipsum[2-3] @@ -906,6 +874,28 @@ + + + + + + + + + + + + + + + + + + + + + + diff --git a/Report/graphs/D1.json b/Report/graphs/D1.json index a37a59d..58d3443 100644 --- a/Report/graphs/D1.json +++ b/Report/graphs/D1.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{---}\\;}}","tabs":[{"active":true,"edges":[{"from":0,"id":4,"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":5,"label":{"kind":"normal","label":"R_0^{i-1} X_\\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":6,"label":{"kind":"normal","label":"f \\circ \\dash","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":7,"label":{"kind":"normal","label":"\\Cstr^{X'}","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_i(F_{i-1}X)","pos":[180,60],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"(R_0^{i-1} X)_\\UU","pos":[450,60],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^{i-1} X')_\\UU","pos":[450,143],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_i(F_{i-1}X')","pos":[180,143],"zindex":-10000}}],"sizeGrid":120,"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{---}\\;}}","tabs":[{"active":true,"edges":[{"from":0,"id":4,"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":5,"label":{"kind":"normal","label":"(R_0^{i-1} f)_\\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":6,"label":{"kind":"normal","label":"H_iF_{i-1}f","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":7,"label":{"kind":"normal","label":"\\Cstr^{X'}","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","pos":[180,60],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"(R_0^i X)_\\UU","pos":[450,60],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i X')_\\UU","pos":[450,143],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^iX'","pos":[180,143],"zindex":-10000}}],"sizeGrid":120,"title":"1"}]},"version":12} \ No newline at end of file diff --git a/Report/graphs/D2.json b/Report/graphs/D2.json index da0776b..176d221 100644 --- a/Report/graphs/D2.json +++ b/Report/graphs/D2.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":"\\text{H3'}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":-1},"to":1},{"from":2,"id":11,"label":{"kind":"normal","label":"\\inj_2^0","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":"\\text{H1r}","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^i(g \\oplus L_0^{i-1}\\Hbar_\\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 \\Hbar_\\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":6},{"from":6,"id":15,"label":{"kind":"normal","label":"\\text{H1r}","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":16,"label":{"kind":"normal","label":"\\left[\\Hbar_\\bullet(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":"g \\circ \\dash","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 \\oplus L_0^{i-1}\\Hbar_\\bullet(g,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":20,"label":{"kind":"normal","label":"H3'","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":8},{"from":7,"id":21,"label":{"kind":"normal","label":"\\inj_2^0","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 \\oplus L_0^{i-1}\\Hbar_\\bullet(X,Y))","pos":[306,72],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"H_iF_{i-1}(X)","pos":[530,72],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\left[\\Hbar_\\bullet(X,Y)\\right]_\\UU","pos":[682,72],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\left[R_0^{i-1} X \\oplus \\Hbar_\\bullet(X,Y)\\right]_\\UU","pos":[916,72],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"R_0^{i-1}(X \\oplus L_0^{i-1} \\Hbar_\\bullet(X,Y))_\\UU","pos":[1194,72],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"R_0^{i-1}(X' \\oplus L_0^{i-1} \\Hbar_\\bullet(X',Y'))_\\UU","pos":[1194,230],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"\\left[R_0^{i-1} X' \\oplus \\Hbar_\\bullet(X',Y')\\right]_\\UU","pos":[916,230],"zindex":-10000}},{"id":7,"label":{"isMath":true,"label":"\\left[\\Hbar_\\bullet(X',Y')\\right]_\\UU","pos":[682,230],"zindex":0}},{"id":8,"label":{"isMath":true,"label":"H_iF_{i-1}(X')","pos":[530,230],"zindex":0}},{"id":9,"label":{"isMath":true,"label":"H_iF_{i-1}(X' \\oplus L_0^{i-1}\\Hbar_\\bullet(X',Y'))","pos":[306,230],"zindex":0}}],"sizeGrid":200,"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":10,"label":{"kind":"normal","label":"(H_iF_{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":-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})^{-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_{H_iF_{i-1}}(g,h))_\\UU","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":15,"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":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_{H_iF_{i-1}}(g,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":20,"label":{"kind":"normal","label":"(H_iF_{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":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":[306,64],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"H_iF_{i-1}X","pos":[634,64],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\left[K_{H_iF_{i-1}}(X,Y)\\right]_\\UU","pos":[810,64],"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":[1068,64],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"R_0^{i-1}(X \\tl^{i-1} K_\\bullet(X,Y))_\\UU","pos":[1396,64],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"R_0^{i-1}(X' \\tl^{i-1} K_\\bullet(X',Y'))_\\UU","pos":[1396,206],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"\\left[R_0^{i-1} X' \\oplus K_{H_iF_{i-1}}(X',Y')\\right]_\\UU","pos":[1068,206],"zindex":-10000}},{"id":7,"label":{"isMath":true,"label":"\\left[K_{H_iF_{i-1}}(X',Y')\\right]_\\UU","pos":[810,206],"zindex":0}},{"id":8,"label":{"isMath":true,"label":"H_iF_{i-1}X'","pos":[634,206],"zindex":0}},{"id":9,"label":{"isMath":true,"label":"H_iF_{i-1}(X' \\tl^{i-1}K_{H_iF_{i-1}}(X',Y'))","pos":[306,206],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12} \ No newline at end of file diff --git a/Report/graphs/D3a.json b/Report/graphs/D3a.json index bbde53b..7e74d8a 100644 --- a/Report/graphs/D3a.json +++ b/Report/graphs/D3a.json @@ -1 +1 @@ -{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":4,"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":1},{"from":0,"id":5,"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":2},{"from":2,"id":6,"label":{"kind":"normal","label":"R_0^i(X)_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":7,"label":{"kind":"normal","label":"\\Cstr^X_i","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":"A","pos":[100,117.8125],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"H_iF_{i-1}(R_{i-1}^i X)","pos":[100,195.8125],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"R_0^i(X)_\\El","pos":[358,117.8125],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"R_0^i(X)_\\UU","pos":[358,195.8125],"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":4,"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":1},{"from":0,"id":5,"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":2},{"from":2,"id":6,"label":{"kind":"normal","label":"R_0^i(X)_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":7,"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":3},{"from":4,"id":8,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":5}],"nodes":[{"id":0,"label":{"isMath":true,"label":"A","pos":[100,117.8125],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i X","pos":[100,195.8125],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"R_0^i(X)_\\El","pos":[358,117.8125],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"R_0^i(X)_\\UU","pos":[358,195.8125],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12} \ No newline at end of file diff --git a/Report/graphs/D3b.json b/Report/graphs/D3b.json index 27b1733..6194562 100644 --- a/Report/graphs/D3b.json +++ b/Report/graphs/D3b.json @@ -1 +1 @@ -{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":8,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":9,"label":{"kind":"normal","label":"R_0^i(X)_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":10,"label":{"kind":"normal","label":"h","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.30000000000000004,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":11,"label":{"kind":"normal","label":"\\Cstr^X_i","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":12,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":5,"id":13,"label":{"kind":"normal","label":"R_0^i(X')_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":4,"id":14,"label":{"kind":"normal","label":"h'","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.30000000000000004,"tail":"none"},"zindex":0},"to":7},{"from":7,"id":15,"label":{"kind":"normal","label":"\\Cstr^{X'}_i","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":0,"id":16,"label":{"kind":"normal","label":"!","style":{"alignment":"left","bend":0,"color":"black","dashed":true,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":1},"to":4},{"from":1,"id":17,"label":{"kind":"normal","label":"R_0^i(f)_\\El","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":18,"label":{"kind":"normal","label":"H_iF_{i-1}R_{i-1}^i f","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.10000000000000003,"tail":"none"},"zindex":0},"to":7},{"from":2,"id":19,"label":{"kind":"normal","label":"R_0^i(f)_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.6,"tail":"none"},"zindex":0},"to":6},{"from":14,"id":20,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":12},{"from":10,"id":21,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":8}],"nodes":[{"id":0,"label":{"isMath":true,"label":"A","pos":[125,115],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"R_0^i(X)_\\El","pos":[403,115],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"R_0^i(X)_\\UU","pos":[403,297],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}(R_{i-1}^i X)","pos":[125,297],"zindex":-10000}},{"id":4,"label":{"isMath":true,"label":"A'","pos":[249,190.8125],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"R_0^i(X')_\\El","pos":[521,190.8125],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"R_0^i(X')_\\UU","pos":[521,372.8125],"zindex":0}},{"id":7,"label":{"isMath":true,"label":"H_iF_{i-1}(R_{i-1}^i X')","pos":[249,372.8125],"zindex":-10000}}],"sizeGrid":250,"title":"1"}]},"version":12} \ No newline at end of file +{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":8,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":9,"label":{"kind":"normal","label":"R_0^i(X)_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":10,"label":{"kind":"normal","label":"h","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.30000000000000004,"tail":"none"},"zindex":0},"to":3},{"from":3,"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":2},{"from":4,"id":12,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":5,"id":13,"label":{"kind":"normal","label":"R_0^i(X')_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":4,"id":14,"label":{"kind":"normal","label":"h'","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.30000000000000004,"tail":"none"},"zindex":0},"to":7},{"from":7,"id":15,"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":6},{"from":0,"id":16,"label":{"kind":"normal","label":"!","style":{"alignment":"left","bend":0,"color":"black","dashed":true,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":1},"to":4},{"from":1,"id":17,"label":{"kind":"normal","label":"R_0^i(f)_\\El","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":18,"label":{"kind":"normal","label":"H_iF_{i-1}R_{i-1}^i f","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.10000000000000003,"tail":"none"},"zindex":0},"to":7},{"from":2,"id":19,"label":{"kind":"normal","label":"R_0^i(f)_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.6,"tail":"none"},"zindex":0},"to":6},{"from":14,"id":20,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":12},{"from":10,"id":21,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":8}],"nodes":[{"id":0,"label":{"isMath":true,"label":"A","pos":[125,115],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"R_0^i(X)_\\El","pos":[403,115],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"R_0^i(X)_\\UU","pos":[403,297],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i X","pos":[125,297],"zindex":-10000}},{"id":4,"label":{"isMath":true,"label":"A'","pos":[249,190.8125],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"R_0^i(X')_\\El","pos":[521,190.8125],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"R_0^i(X')_\\UU","pos":[521,372.8125],"zindex":0}},{"id":7,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i X'","pos":[249,372.8125],"zindex":-10000}}],"sizeGrid":250,"title":"1"}]},"version":12} \ No newline at end of file diff --git a/Report/graphs/D4.json b/Report/graphs/D4.json index 195f3ad..6266f0d 100644 --- a/Report/graphs/D4.json +++ b/Report/graphs/D4.json @@ -1 +1 @@ -{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":6,"label":{"kind":"normal","label":"\\Cstr^X","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":7,"label":{"kind":"normal","label":"(R_0^{i-1} (\\inj_1^{i-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":8,"label":{"kind":"normal","label":"H_iF_{i-1}\\inj_1^{i-1}","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":4,"id":9,"label":{"kind":"normal","label":"R_0^{i-1}(\\inj_1^{i-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":3,"id":10,"label":{"kind":"normal","label":"(H_iF_{i-1}\\inj_1^{i-1})^{-1}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":-3},"to":5},{"from":5,"id":11,"label":{"kind":"normal","label":"\\Cstr^X","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":0,"id":12,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":4,"id":13,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":3,"id":14,"label":{"kind":"normal","label":"\\Cstr^{X \\oplus L_0^i Y}","style":{"alignment":"left","bend":0.1,"color":"green","dashed":true,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2}],"nodes":[{"id":0,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i X","pos":[236.5,73.5],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"(R_0^i X)_\\UU","pos":[1013,73.8125],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^{i-1} (R_{i-1}^i X \\oplus L_0^{i-1} Y))_\\UU","pos":[1017.5,249.5],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}(R_{i-1}^i X \\oplus_{i-1} L_0^{i-1} Y)","pos":[236.5,249.5],"zindex":-10000}},{"id":4,"label":{"isMath":true,"label":"(R_0^i X)_\\UU","pos":[706,235.8125],"zindex":-10000}},{"id":5,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i X","pos":[556,234.8125],"zindex":-10000}}],"sizeGrid":147,"title":"1"}]},"version":12} \ No newline at end of file +{"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_iF_{i-1}\\inj_1^{i-1})^{-1}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":-3},"to":5},{"from":5,"id":11,"label":{"kind":"normal","label":"\\Cstr^X","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":0,"id":12,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":4,"id":13,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":3,"id":14,"label":{"kind":"normal","label":"\\Cstr^{X \\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 diff --git a/Report/graphs/D5.json b/Report/graphs/D5.json index f8d010b..1212588 100644 --- a/Report/graphs/D5.json +++ b/Report/graphs/D5.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_iF_{i-1}\\inj^{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":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}\\{\\varphi_1 ; \\varphi_2\\}","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":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.6,"tail":"none"},"zindex":-1},"to":4},{"from":4,"id":10,"label":{"kind":"normal","label":"(R_0^i \\{\\varphi_1;\\varphi_2\\})_\\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":"R_{i-1}^i \\varphi_1 \\circ \\dash","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":13,"label":{"kind":"normal","label":"(R_0^i \\varphi_1)_\\UU","style":{"alignment":"left","bend":0,"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 \\oplus L_0^{i-1} Y)","pos":[225,75],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i X","pos":[477,75],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i X)_\\UU","pos":[571,142.8125],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i Z","pos":[225,365],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"(R_0^{i-1} (R_{i-1}^i X \\oplus L_0^{i-1} Y))_\\UU","pos":[777,75],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[777,365],"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,"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,"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":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":2,"id":13,"label":{"kind":"normal","label":"(R_0^i g)_\\UU","style":{"alignment":"left","bend":0,"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":[225,69],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i X","pos":[495,69],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i X)_\\UU","pos":[645,69],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i Z","pos":[225,251],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"(R_0^{i-1} (R_{i-1}^i X \\tl^{i-1} Y))_\\UU","pos":[893,69],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[893,251],"zindex":0}}],"sizeGrid":150,"title":"1"}]},"version":12} \ No newline at end of file diff --git a/Report/graphs/D6.json b/Report/graphs/D6.json index 7dbbc54..fdcc18e 100644 --- a/Report/graphs/D6.json +++ b/Report/graphs/D6.json @@ -1 +1 @@ -{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":6,"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":7,"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":8,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":9,"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":10,"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":11,"label":{"kind":"normal","label":"H_iF_{i-1}(R_{i-1}^i f \\circ \\inj_1)","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.10000000000000003,"tail":"hook"},"zindex":8},"to":3},{"from":4,"id":12,"label":{"kind":"normal","label":"\\left[R_{i-1}^i f \\circ \\inj_2\\right]_\\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":4,"id":13,"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}],"nodes":[{"id":0,"label":{"isMath":true,"label":"E(z)","pos":[290,174],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"(R_0^i Z)_\\El","pos":[490,174],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[490,304],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i Z","pos":[290,304],"zindex":-10000}},{"id":4,"label":{"isMath":true,"label":"A","pos":[100,100],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"H_iF_{i-1}X","pos":[101,224.8125],"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":6,"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":7,"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":8,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":9,"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":10,"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":11,"label":{"kind":"normal","label":"H_iF_{i-1}(R_{i-1}^i f \\circ \\inj_\\tl^{i-1})","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.10000000000000003,"tail":"hook"},"zindex":8},"to":3},{"from":4,"id":12,"label":{"kind":"normal","label":"\\left[R_{i-1}^i f \\circ \\inj_\\tl^{i-1}\\right]_\\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":4,"id":13,"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":8,"id":14,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":6}],"nodes":[{"id":0,"label":{"isMath":true,"label":"E(z)","pos":[290,174],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"(R_0^i Z)_\\El","pos":[490,174],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[490,304],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i Z","pos":[290,304],"zindex":-10000}},{"id":4,"label":{"isMath":true,"label":"A","pos":[100,100],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"H_iF_{i-1}X","pos":[101,224.8125],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12} \ No newline at end of file diff --git a/Report/graphs/D8.json b/Report/graphs/D8.json index fc8d7c4..4e27a56 100644 --- a/Report/graphs/D8.json +++ b/Report/graphs/D8.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":8,"label":{"kind":"normal","label":"\\text{H3'}","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.30000000000000004,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":9,"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":10,"label":{"kind":"normal","label":"\\inj_2^0","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":"\\text{H1r}","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":12,"label":{"kind":"normal","label":"R_0^{i-1}\\left\\{g;\\eta_0^i \\circ L_0^{i-1} \\square \\right\\}","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":13,"label":{"kind":"normal","label":"(\\varepsilon_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":6},{"from":6,"id":14,"label":{"kind":"normal","label":"(R_0^{i-1} \\inj_2^{i-1})_\\UU","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":15,"label":{"kind":"normal","label":"R_0^{i-1}(\\eta_0^i \\circ L_0^{i-1} \\square)_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.7,"tail":"none"},"zindex":0},"to":5},{"from":2,"id":16,"label":{"kind":"normal","label":"\\Cstr^Z \\circ H_iF_{i-1}g","style":{"alignment":"right","bend":0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.30000000000000004,"tail":"none"},"zindex":0},"to":5},{"from":0,"id":17,"label":{"kind":"normal","label":"H_iF_{i-1}\\left\\{g;\\eta_0^i \\circ L_0^{i-1} \\square \\right\\}","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":18,"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":19,"label":{"kind":"normal","label":"H_iF_{i-1}g","style":{"alignment":"left","bend":0,"color":"red","dashed":false,"head":"default","kind":"normal","position":0.4,"tail":"none"},"zindex":0},"to":7}],"nodes":[{"id":0,"label":{"isMath":true,"label":"H_iF_{i-1}(X \\oplus L_0^{i-1}\\Hbar_\\bullet(X,Y))","pos":[210,64],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"H_iF_{i-1}X","pos":[329,129.8125],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\Hbar(X,Y)_\\UU","pos":[410,64.8125],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\left[R_0^{i-1} X \\oplus \\Hbar(X,Y)\\right]_\\UU","pos":[604.9999999999999,61.8125],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"R_0^{i-1}\\left(X \\oplus L_0^{i-1}\\Hbar(X,Y)\\right)","pos":[853,61.8125],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[853,303.8125],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"\\left[R_0^{i-1}L_0^{i-1}\\Hbar(X,Y)\\right]_\\UU","pos":[688,198.625],"zindex":0}},{"id":7,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i Z","pos":[210,306],"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":7,"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":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":"normal","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":2,"id":12,"label":{"kind":"normal","label":"\\square_\\UU","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"none","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":0,"id":13,"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":14,"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":15,"label":{"kind":"normal","label":"H_iF_{i-1}g","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.4,"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":[210,64],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"H_iF_{i-1}X","pos":[492,64],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"K_{H_iF_{i-1}}(X,Y)_\\UU","pos":[616,64],"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":[870,64],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"R_0^{i-1}\\left(X \\tl^{i-1} K_\\bullet(X,Y)\\right)_\\UU","pos":[870,158],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[870,250],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i Z","pos":[210,250],"zindex":0}}],"sizeGrid":140,"title":"1"}]},"version":12} \ No newline at end of file diff --git a/Report/graphs/G1.json b/Report/graphs/G1.json index 52f2064..1c6c8fd 100644 --- a/Report/graphs/G1.json +++ b/Report/graphs/G1.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":"F_i","style":{"alignment":"right","bend":0.20000000000000004,"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_i","style":{"alignment":"right","bend":0.20000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":0,"id":9,"label":{"kind":"normal","label":"R_{i-1}^i","style":{"alignment":"right","bend":0.20000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":10,"label":{"kind":"normal","label":"L_{i-1}^i","style":{"alignment":"right","bend":0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":2,"id":11,"label":{"kind":"normal","label":"F_{i-1}","style":{"alignment":"right","bend":0.2,"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":"G_{i-1}","style":{"alignment":"right","bend":0.2,"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":"","style":{"alignment":"left","bend":0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":4,"id":14,"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":2},{"from":4,"id":15,"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":5},{"from":5,"id":16,"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":4},{"from":5,"id":17,"label":{"kind":"normal","label":"L_0^i","style":{"alignment":"right","bend":-0.5,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":0,"id":18,"label":{"kind":"normal","label":"R_0^i","style":{"alignment":"right","bend":0.7,"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":"\\lambda.\\star","style":{"alignment":"right","bend":0.20000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":6,"id":20,"label":{"kind":"normal","label":"\\lambda.1","style":{"alignment":"right","bend":0.20000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":18,"id":21,"label":{"kind":"adjunction","label":"\\vdash","style":{"alignment":"over","bend":0,"color":"black","dashed":false,"head":"none","kind":"none","position":0.5,"tail":"none"},"zindex":0},"to":17},{"from":9,"id":22,"label":{"kind":"adjunction","label":"\\vdash","style":{"alignment":"over","bend":0,"color":"black","dashed":false,"head":"none","kind":"none","position":0.5,"tail":"none"},"zindex":0},"to":10},{"from":7,"id":23,"label":{"kind":"adjunction","label":"\\vdash","style":{"alignment":"over","bend":0,"color":"black","dashed":false,"head":"none","kind":"none","position":0.5,"tail":"none"},"zindex":0},"to":8},{"from":11,"id":24,"label":{"kind":"adjunction","label":"\\vdash","style":{"alignment":"over","bend":0,"color":"black","dashed":false,"head":"none","kind":"none","position":0.5,"tail":"none"},"zindex":0},"to":12},{"from":19,"id":25,"label":{"kind":"adjunction","label":"\\vdash","style":{"alignment":"over","bend":0,"color":"black","dashed":false,"head":"none","kind":"none","position":0.5,"tail":"none"},"zindex":0},"to":20},{"from":13,"id":26,"label":{"kind":"adjunction","label":"\\vdash","style":{"alignment":"over","bend":0,"color":"black","dashed":false,"head":"none","kind":"none","position":0.5,"tail":"none"},"zindex":0},"to":14},{"from":15,"id":27,"label":{"kind":"adjunction","label":"\\vdash","style":{"alignment":"over","bend":0,"color":"black","dashed":false,"head":"none","kind":"none","position":0.5,"tail":"none"},"zindex":0},"to":16}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\BB_i","pos":[195,61],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\CC_i","pos":[474,61],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\BB_{i-1}","pos":[195,221],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\CC_{i-1}","pos":[474,221],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"\\vdots","pos":[195,327],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"\\BB_0 = \\TSet","pos":[195,430],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"\\CC_0 = 1","pos":[474,430],"zindex":0}}],"sizeGrid":130,"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":7,"label":{"kind":"normal","label":"F_i","style":{"alignment":"right","bend":0.20000000000000004,"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_i","style":{"alignment":"right","bend":0.20000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":0,"id":9,"label":{"kind":"normal","label":"R_{i-1}^i","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":10,"label":{"kind":"normal","label":"F_{i-1}","style":{"alignment":"right","bend":0.2,"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":"G_{i-1}","style":{"alignment":"right","bend":0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"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":4},{"from":4,"id":13,"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":0,"id":14,"label":{"kind":"normal","label":"R_0^i","style":{"alignment":"right","bend":0.30000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":5,"id":15,"label":{"kind":"normal","label":"F_0","style":{"alignment":"right","bend":0.20000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":6,"id":16,"label":{"kind":"normal","label":"G_0","style":{"alignment":"right","bend":0.20000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":7,"id":17,"label":{"kind":"adjunction","label":"\\vdash","style":{"alignment":"over","bend":0,"color":"black","dashed":false,"head":"none","kind":"none","position":0.5,"tail":"none"},"zindex":0},"to":8},{"from":10,"id":18,"label":{"kind":"adjunction","label":"\\vdash","style":{"alignment":"over","bend":0,"color":"black","dashed":false,"head":"none","kind":"none","position":0.5,"tail":"none"},"zindex":0},"to":11},{"from":15,"id":19,"label":{"kind":"adjunction","label":"\\vdash","style":{"alignment":"over","bend":0,"color":"black","dashed":false,"head":"none","kind":"none","position":0.5,"tail":"none"},"zindex":0},"to":16}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\BB_i","pos":[195,61],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\CC_i","pos":[388,61],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\BB_{i-1}","pos":[195,173],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\CC_{i-1}","pos":[388,173],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"\\vdots","pos":[195,251],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"\\BB_0","pos":[195,328],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"\\CC_0","pos":[388,328],"zindex":0}}],"sizeGrid":130,"title":"1"}]},"version":12} \ No newline at end of file diff --git a/Report/graphs/TlConstructor.json b/Report/graphs/TlConstructor.json new file mode 100644 index 0000000..a32ce29 --- /dev/null +++ b/Report/graphs/TlConstructor.json @@ -0,0 +1 @@ +{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\CC{{\\ensuremath{\\mathcal{C}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":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 diff --git a/Report/graphs/TlUniversal.json b/Report/graphs/TlUniversal.json new file mode 100644 index 0000000..0311d47 --- /dev/null +++ b/Report/graphs/TlUniversal.json @@ -0,0 +1 @@ +{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\CC{{\\ensuremath{\\mathcal{C}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":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)^{-1}","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 diff --git a/Report/graphs/Wdef.json b/Report/graphs/Wdef.json new file mode 100644 index 0000000..9e79174 --- /dev/null +++ b/Report/graphs/Wdef.json @@ -0,0 +1 @@ +{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\CC{{\\ensuremath{\\mathcal{C}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":5,"label":{"kind":"normal","label":"(H_iF_{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})^{-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 diff --git a/Report/header.tex b/Report/header.tex index a61ee6d..0dedfd7 100644 --- a/Report/header.tex +++ b/Report/header.tex @@ -112,6 +112,7 @@ \newcommand\Hom{{\ensuremath{\operatorname{\mathcal{H}om}}}} \newcommand\this{{\ensuremath{\operatorname{\texttt{this}}}}} \newcommand\Hbar{{\ensuremath{K}}} +\newcommand\one{{\ensuremath{\mathbf{1}}}} \newcommand\dash{{\;\textrm{---}\;}} \renewcommand\enquote[1]{``#1''} \newcommand\tl{{\triangleleft}}