From d247b98bc5ef5faa66d90e814552e6f0dfb5a5ac Mon Sep 17 00:00:00 2001 From: Samy Avrillon Date: Fri, 12 Jul 2024 13:17:26 +0200 Subject: [PATCH] Modifications --- Report/.gitignore | 3 +- Report/M2Report.tex | 688 ++++++++++++++++++++-------- Report/graphs/B1.json | 1 + Report/graphs/D1.json | 1 + Report/graphs/D10.0.json | 1 + Report/graphs/D10.json | 1 + Report/graphs/D11.json | 1 + Report/graphs/D2.json | 1 + Report/graphs/D3a.json | 1 + Report/graphs/D3b.json | 1 + Report/graphs/D4.json | 1 + Report/graphs/D5.json | 1 + Report/graphs/D6.json | 1 + Report/graphs/D7.json | 1 + Report/graphs/D8.json | 1 + Report/graphs/D9.json | 1 + Report/graphs/G0.json | 1 + Report/graphs/G1.json | 1 + Report/graphs/G2.json | 1 + Report/header.tex | 13 + Report/yade-preamble.tex | 15 + Report/yade.sty | 960 +++++++++++++++++++++++++++++++++++++++ 22 files changed, 1499 insertions(+), 197 deletions(-) create mode 100644 Report/graphs/B1.json create mode 100644 Report/graphs/D1.json create mode 100644 Report/graphs/D10.0.json create mode 100644 Report/graphs/D10.json create mode 100644 Report/graphs/D11.json create mode 100644 Report/graphs/D2.json create mode 100644 Report/graphs/D3a.json create mode 100644 Report/graphs/D3b.json create mode 100644 Report/graphs/D4.json create mode 100644 Report/graphs/D5.json create mode 100644 Report/graphs/D6.json create mode 100644 Report/graphs/D7.json create mode 100644 Report/graphs/D8.json create mode 100644 Report/graphs/D9.json create mode 100644 Report/graphs/G0.json create mode 100644 Report/graphs/G1.json create mode 100644 Report/graphs/G2.json create mode 100644 Report/yade-preamble.tex create mode 100644 Report/yade.sty diff --git a/Report/.gitignore b/Report/.gitignore index 567609b..62c66b2 100644 --- a/Report/.gitignore +++ b/Report/.gitignore @@ -1 +1,2 @@ -build/ +.build/ +graphs/*.tex diff --git a/Report/M2Report.tex b/Report/M2Report.tex index f4ebbf7..d77a0e9 100644 --- a/Report/M2Report.tex +++ b/Report/M2Report.tex @@ -25,114 +25,262 @@ \section{Content} + Plan - \subsection{Infinite construction of $\BB_i$} - \[ - \BB_i := \left(X : \TSet, \Cstr : (a : S_{i-1}) \to \Hom_{\BB_{a-1}}(G_{a-1}\Gamma_a,R_{a-1}^i(\this)) \to X(\UU)\right) - \] - A morphism from $(X,\Cstr)$ to $(X', \Cstr')$ is a morphism from $X$ to $X'$ in $\TSet$ (i.e. a natural transformation $X \implies X'$) which makes the following diagram commute, for all $a$ in $S_{i-1}$. - - \diagram{D1} - - Identities and compositions are that of the base category $\TSet$, and categorical equalities are trivially derived from the diagram above. - - The diagram expresses as - \[ - \forall \gamma \in \Hom_{G_{a-1}\Gamma_a,X}, \quad \Cstr'_a(f \circ \gamma) = f_\UU(\Cstr_a \gamma) - \] - - \todo{Define properly the use of \this} - - \subsection{$H$ functors} + \begin{enumerate} + \item Présentation de ce qu'est un GAT, simple exemple + \item Présentation de la 2-sortification d'un GAT + \item Présentation de la catégorification de Fiore + \item Présentation de la catégorification de Altenkirsch -> Construction des $\BB_i$ récursive + \item Schéma de construction récursif de l'adjonction + \item Formulation de H1 et H3 + \item (ANNEXE?) Def de W et de E + \item (ANNEXE?) Preuve de l'adjonction / de la reflexion + \item (ANNEXE?) Preuve des propriétés + \item Définition infinie de $\BB_i$ -> Foncteur $R_0^iG_i$ -> Reflexions sur les catégories pas directes + \end{enumerate} - For every object $X$ of a locally small category $C$, we define the functor $H_X : (X/\Set) \to \TSet$ - \[ - H_X(Y,f) = \TSetObject{X}{f}{Y} - \] - - Dually, we make another functor $\Hbar_X : (\Set/X) \to \TSet$ - \[ - \Hbar_X(Y,f) = \TSetObject{Y}{f}{X} - \] - - The morphisms translate as-is, and composition and identity relies on that of $(X/\Set)$ or $(\Set/X)$. - - \todo{(small) Show that it is actually a functor (should be trivial), potentially add a diagram} - - \subsection{$G$ and $F$ infinite constructions} - \[ - G_i(Y) = \left(\sum_{a\in S_i}H_{Y(a)}\left(\lim_{(a/S_i)*}\overline{Y_a}\right), λa.λ\eta.(a,u (\inj_2 \star))\right) - \] + \section{Sort specification} + + A Generalized Algebraic Theory (or GAT) and inductive-inductive types are syntaxes describing models. + Both are composed of a sort specification, and eventually a list of constructors. + In this document, we will not ask ourselves about the specificities of both syntaxes. A \enquote{vague} interpretation of them is enough to understand the constructions that follows. + + A sort specification is a list of \emph{sort constructors} that are defined with \emph{parameters} with $\Set$ as its codomain. + + Here is an example of a classical sort specification for Type Theory. + + \[ \Con : \Set \\ + \]\[ \Ty : (\Gamma : \Con) \to \Set \\ + \]\[ \Tm : (\Gamma : \Delta) \to (A : \Ty \Delta) \to \Set + \] + This specification is to be read as follows: + + \begin{center} + There is one sort that is $\Con$ - where $u : \left(Y(a) \oplus 1, \inj_1\right) \to (\lim_{(a/S_i)*} \overline{Y_a})$ + For every element $\Gamma$ of the sort $\Con$, there is a sort $\Ty \Gamma$ - so that $\varphi_{b,f} u (\star) = \eta_\El^b(f)$ - - \[ - F_i(X,\Cstr)(a) = X(p)^{-1}\left(\Cstr_a\left(\Hom_{\BB_{a-1}}(G_{a-1}\Gamma_a,X)\right)\right) - \] - \[ - F_i(X,\Cstr)(f : a \to b)(X(p)(x); x \in \Cstr_a(\eta)) = \eta_\El^b(f) - \] - - \subsection{Hypohesis} - - \begin{property}[H3] - \[ - F_i(X \oplus L_0^i Y) \cong F_i X - \] - \end{property} - - \todo{Do we need to specify that the adjunction is (rtl) $F(inj_1^i)$ ? And prove it ?} - - \begin{property}[H3'] - \[ - \Hom(G_i\Gamma, X) \cong \Hom(G_i\Gamma,X \oplus L_0^i Y) - \] - With left to right isomorphism being $(inj_1^i \circ \dash)$ - \end{property} + For every element $\Gamma$ of the sort $\Con$, and every element $A$ of the sort $\Ty \Gamma$, there is a sort $\Tm \Gamma\;F$ + \end{center} + + We can also add constructors to a sort specification. + For example, for the previous sort specification, one can add the following constructors: + + \[ + \operatorname{unit} : (\Gamma : \Con) \to \Ty \Gamma + \] + \[ + \verb*|_| = \verb*|_|: (\Gamma : \Con) \to (A : \Ty \Gamma) \to \Tm \Gamma A \to \Tm \Gamma A \to \Ty \Gamma + \] + + Constructors construct terms and not sorts. A sort specification with or without constructor describes a class of models, which are in the intuitive sense of a model (a model implements \enquote{sort constructors}, regular constructors). + + A known process is that one can transform a specification of sorts, into a specification of sorts with two sorts and constructors. + + The two sorts are always the same: + + \[ + \mathcal{O} : \square + \] + \[ + \underline{\;\bullet\;} : \mathcal{O} \to \square + \] + + Where $\mathcal{O}$ describes the \enquote{sort of sorts}, and $\underline{\;\bullet\;}$ give for every \enquote{sort object} the sort of the \enquote{objects of that sort}. + + Then, we replace all occurrences of $\Set$ to $\mathcal{O}$, and we apply underline to every sort constructor parameter. For example, the first Type Theory of sort specification becomes that which follows: + + \[ \Con : \mathcal{O} \\ + \]\[ \Ty : (\Gamma : \underline{\Con}) \to \mathcal{O} \\ + \]\[ \Tm : (\Gamma : \underline{\Con}) \to (A : \underline{\Ty \Delta}) \to \mathcal{O} + \] + + It is known that this new sorts and constructors specification is equivalent to the former one. + + Fiore \cite{Fiore2008} describes \emph{sort specifications} as countable simple direct categories. To every object, we associate a sort, which is built using parameters pointing out of them. We often write this category $S$, and for a sort $a$ in it, the parameters needed to construct the sort are indexed by $(a/S)*$. + + As an example, here is the category version of the above specification of sorts. We also add the equality $\Gamma \circ A = \Delta$. This equality describes that the $\Gamma$-parameter i.e. the first parameter of the $\Ty$ sort constructor is the variable $\Delta$. Without this equality, $\Gamma \circ A$ would be another arrow going from $\Tm$, and therefore another parameter on type $\Con$. + + + \begin{center} + % YADE DIAGRAM B1.json + % GENERATED LATEX + \input{graphs/B1.tex} + % END OF GENERATED LATEX + \end{center} + + The category of models over a specification of sorts is then the category of presheaves over the category of Fiore $\left[S,\Set\right]$. + + Altenkirsch \cite{Altenkirch2018} has another method to directly construct the category of models of a specification of sorts. His method is more general, but it does not give a \enquote{Tiny and simple} category as Fiore does. + The other advantage of Altenkirsch's method is that they give a way of also describing the models of a constructor specification. + + What we will do is to try to make an adjunction between Fiore's category of models $\left[S,\Set\right]$, and Altenkirsch's category of models of the two-sorted GAT. + + We will describe how the two categories are constructed in detail. + + \subsection{Constructing the categories} + + We will construct both categories $S$ and $\BB$ recursively, addings new sorts one by one. + + \subsubsection{Fiore's category} + + At the same time, we construct the simple category recursively $\emptyset = S_0,S_1,S_2,...$. + + In order to construct the $i$-th sort, we use a finite functor $\Gamma_i : \left[S_{i-1} \to \Set\right]$ describing entirely the sort constructor. + This functor is to be understood as $\Gamma_i(a)$ is the set of parameters of type $a$ for our new sort. In the above example, we would have $\Gamma_\Ty(\Con) = \{"\Gamma"\} = 1$ and $\Gamma_\Tm(\Con) = \{\Delta\}$,$\Gamma_\Tm(\Ty) = \{"A"\}$,$\Gamma_\Tm(\Gamma) = \left["A" \mapsto "\Delta"\right]$. + + Then, to construct $S_i$, we add one object $i$ to $S_{i-1}$, along with morphisms $x : i \to a$ for every $x \in \Gamma_i(a)$ for every $a$ in $S_{i-1}$. We also add equalities + $s \circ x = x'$ for every $s : b \to a$ and $x \in \Gamma_i(a)$ and $x' \in \Gamma_i(b)$ where $\Gamma_i(s)(x') = x$. + + \begin{remark} + We have that $\Hom_{S_i}(a,b) = \Gamma_b(a)$ or $(a/S_i)* \equiv \Gamma_a$.TODO C'est sûr la deuxième partie ? + \end{remark} + + \subsubsection{Altenkirsch's category} + + To start our series of category, we need the category of models of the two-sort specification of sorts ($\mathcal{O}$ and $\underline{\;\bullet\;}$). We do it Fiore's way and we get a simple category that we name $\TT$ with two elements and only one non-trivial arrow between them. + + \begin{center} + % YADE DIAGRAM G0.json + % GENERATED LATEX + \input{graphs/G0.tex} + % END OF GENERATED LATEX + \end{center} + + The category of models $\TSet$ is also written $\BB_0$ as it is the first step of Altenkirsch's method of adding constructors. + + \begin{remark} + Following Altenkirsch's construction of category of models for a sort specification, we end up on the category of families of sets $(X : \Set, Y : X \to \Set)$. + This category is equivalent to $\TSet$ which allows us to give a clearer definition of functors. + \end{remark} + + Then, we recursively add constructors, constructing categories $\BB_1$,$\BB_2$, etc. + + For the $i$-th constructor, we define the category $\BB_i$ as : + + \[ + \BB_i := \left(X : \BB_{i-1}, \Cstr_i : \Hom_{\BB_{i-1}} (G_{i-1}\Gamma_i,X) \to (R_0^{i-1}X)_\UU \right) + \] + + where $\Gamma_i$ is the functor $S_{i-1} \to \Set$ that describe the sort constructor being processed, and $G_{i-1}$ is the left part of the adjunction $\left[S_{i-1}, \Set\right] \to \BB_{i-1}$ that we are defining recursively at the same time. + + A morphism $(X,\Cstr_i) \to (X',\Cstr'_i)$ in $\BB_i$ is a morphism $f : X \to X'$ in $\BB_{i-1}$ such that the following diagram commutes. + + \begin{center} + % YADE DIAGRAM D1.json + % GENERATED LATEX + \input{graphs/D1.tex} + % END OF GENERATED LATEX + \end{center} + + Identities and compositions are that of the category $\BB_{i-1}$, and categorical equalities are trivially derived from the diagram above. + + 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 adjunct} of another functor we call $L_{i-1}^i$. + + As we can compose the adjunctions $R_0^1$,$R_1^2$,...,$R_{i-1}^i$, we will create the two following syntactic sugars for the composed adjunctions. + \[ + R_i^j = R_{i}^{i+1} \circ R_{i+1}^j = R_{i}^{j-1} \circ R_{j-1}^{j} = R_{i}^{i+1} \circ ... \circ R_{j-1}^{j} + \] + \[ + L_i^j = L_{j-1}^{j} \circ L_{i}^{j-1} = L_{i+1}^{j} \circ L_{i}^{i+1} = L_{j-1}^{j} \circ ... \circ L_{i}^{i+1} + \] + + 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$. + + + + We know that this category has a coproduct, that we will denote $\oplus_i$ or just $\oplus$ when there is no ambiguity. We will also denote as $\inj_1^i : X \to X \oplus Y$ (resp. $\inj_2^i : Y \to X \oplus Y$) the first (resp. second) injector of the coproduct of $\BB_i$. For every morphisms $f : X \to Z$ and $g : Y \to Z$, we will denote with $\{f;g\}$ the unique morphism from $X \oplus Y$ 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 arrow $inj_1 : G_{i-1}\Gamma_i \to G_{i-1}\Gamma_i \oplus L_0^{i-1} y\UU$. + \end{remark} + + \subsubsection{Summary} + + Here is a graph summarizing the categories and functors. + We have constructed two chains of categories $\BB_0$,$\BB_1$,... and $S_0$,$S_1$,... + + The categories $\BB_{i-1}$ and $\BB_{i}$ are in an adjunction written $R_{i-1}^i \vdash L_{i-1}^i$. + + We will give in the next part the construction of the adjunction $F_i \vdash G_i$ at the step $i$. The functor $G_{i-1}$ is used in the definition of $\BB_i$, so the two recurrences have to be done at the same time. + + + + \begin{center} + % YADE DIAGRAM G1.json + % GENERATED LATEX + \input{graphs/G1.tex} + % END OF GENERATED LATEX + \end{center} + + + \subsection{Constructing the adjunction} + + \subsubsection{Hypotheses} + + In order to build and prove the adjunction, we will state hypotheses that we will progressively prove during our building of $\BB_i$, $F_i$, and $G_i$. \begin{property}[H1] \[ - R_{i-1}^i(X \oplus_i L_0^i Y) \cong R_{i-1}^i X \oplus L_0^{i-1} Y + \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)} \] + is an equivalence. \end{property} \begin{property}[H1r] \[ - R_{0}^i(X \oplus_i L_0^i Y) \cong R_{0}^i X \oplus_{i-1} L_0^{i-1} Y + \simpleArrow{ R_{0}^i X \oplus_{i-1} Y}{\left\{R_{i-1}^i \inj_1^i ; \eta_{i-1}^i\right\}}{R_{i-1}^i(X \oplus_i L_0^i Y)} \] - We use the sum that makes this equivalence to be an equality. + is an equivalence. + + This property is proven easily by recursion over previous property H1. \end{property} - \subsection{Notations} - \[ - R_i^j = R_{i}^{i+1} \circ R_{i+1}^j = R_{i}^{j-1} \circ R_{j-1}^{j} = R_{i}^{i+1} \circ ... \circ R_{j-1}^{j} - \] - \[ - L_i^j = L_{j-1}^{j} \circ L_{i}^{j-1} = L_{i+1}^{j} \circ L_{i}^{i+1} = L_{j-1}^{j} \circ ... \circ L_{i}^{i+1} - \] + \begin{property}[H3] + \[ + \simpleArrow{F_i X}{F(\inj_1^i)}{F_i(X \oplus L_0^i Y)} + \] + is an equivalence. + \end{property} - In any category with a coproduct, for every morphisms $f : X \to Z$ and $g : Y \to Z$, we denote with $\{f;g\}$ the unique morphism from $X \oplus Y$ to $Z$ such that $\{f;g\} \circ \inj_1 = f$ and $\{f;g\} \circ \inj_2 = g$. - \subsection{Recursive definition of $\BB_i$} + \begin{property}[H3'] + \[ + \simpleArrow{\Hom(G_i\Gamma, X)}{(inj_1^i \circ \dash)}{\Hom(G_i\Gamma,X \oplus L_0^i Y)} + \] + is an equivalence. + + This proven with the adjunction property of $F_i \vdash G_i$ and H3, as w have that + \[ + \Hom(G_i \Gamma, X) \cong \Hom(\Gamma, F_i X) \cong \Hom(\Gamma, F_i(X \oplus L_0^i Y)) \cong \Hom(G_i \Gamma, X \oplus L_0^i Y) + \] + \end{property} - \[ - \BB_i := \left(X : \BB_{i-1}, \Cstr_i : \Hom_{\BB_{i-1}} (G_{i-1}\Gamma_i,X) \to (R_0^{i-1}X)_\UU \right) - \] - - A morphism $(X,\Cstr_i) \to (X',\Cstr'_i)$ is a morphism $f : X \to X'$ in $\BB_{i-1}$ such that the following diagram commutes. - - \diagram{D1 $[a \mapsfrom i]$} - - Identities and compositions are that of the category $\BB_{i-1}$, and categorical equalities are trivially derived from the diagram above. - - \subsection{W definition} + \subsubsection{Decomposing the proof} - We define a functor $W : \displaystyle\prod_{X : \BB_{i-1}} (\Set/\Hom_{\BB_{i-1}}(G_{i-1}\Gamma_i,X)) \to \BB_{i}$ + 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. + + \begin{center} + % YADE DIAGRAM G2.json + % GENERATED LATEX + \input{graphs/G2.tex} + % END OF GENERATED LATEX + \end{center} + + The category $\left[S_i, \Set\right]$ is seen as the category $\left[S_{i-1},\Set\right]$ to which we have added an object along with morphisms described by $\Gamma_i$. The morphisms we added to the object $X$ have the shape of the slice category of the set $\Hom(\Gamma_i,X)$. + + The first part $G_{i-1} \times \id \dashv F_{i-1} \times \id$ is proven and defined as an adjunction from the last step of the recurrence. + + We will now define the two functors. + + + \subsubsection{W definition} + + We define a functor $W : \displaystyle\sum_{X : \BB_{i-1}} (\Set/\Hom_{\BB_{i-1}}(G_{i-1}\Gamma_i,X)) \to \BB_{i}$ \[ - W(X,Y) := \left(X \oplus L_0^{i-1} \Hbar_{\Hom(G_{i-1}\Gamma_i,\dash)}(X,Y), \widetilde{\inj_2} \right) + W(X,Y) := \left(X \oplus L_0^{i-1} \Hbar_{\Hom(G_{i-1}\Gamma_i,\dash)}(X,Y), \widetilde{\inj_2} \right) \] With $\widetilde{\inj_2}$ being defined by @@ -147,40 +295,58 @@ The action on a morphism $(g,h)$ from $(X,Y)$ to $(X',Y')$ is the following: \[ - W(g,h) := \left(g \oplus L_0^{i-1} \Hbar_{\Hom(G_{i-1}\Gamma_i,\dash)}(g,h)\right) + W(g,h) := \left(g \oplus L_0^{i-1} \Hbar_{\Hom(G_{i-1}\Gamma_i,\dash)}(g,h)\right) \] It is indeed a morphism from $\BB_{i}$ as it makes the following diagram commute. - \diagram{D2} - - \subsection{E definition} - - We define $E : \BB_{i} \to \displaystyle\prod_{X : \BB_{i-1}} (\Set/\Hom_{\BB_{i-1}}(G_{i-1}\Gamma_i,X))$ + \begin{center} + % YADE DIAGRAM D2.json + % GENERATED LATEX + \input{graphs/D2.tex} + % END OF GENERATED LATEX + \end{center} + + \subsubsection{E definition} + + We define $E : \BB_{i} \to \displaystyle\sum_{X : \BB_{i-1}} (\Set/\Hom_{\BB_{i-1}}(G_{i-1}\Gamma_i,X))$ \[ - 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: - \diagram{D3a} + \begin{center} + % YADE DIAGRAM D3a.json + % GENERATED LATEX + \input{graphs/D3a.tex} + % END OF GENERATED LATEX + \end{center} - The action on a morphism $f$ from $X$ to $X'$ is defined as $E(f) = (R_{i-1}^i f, !)$, with $!$ being the only morphism making the following diagram commute: + The action on a morphism $f$ from $X$ to $X'$ is defined as $E(f) = (R_{i-1}^i f, !)$, with $!$ being the only morphism making the following diagram commute (thanks to the pullback property): - \diagram{D3b} + \begin{center} + % YADE DIAGRAM D3b.json + % GENERATED LATEX + \input{graphs/D3b.tex} + % END OF GENERATED LATEX + \end{center} + + + \subsubsection{Proof of the adjunction} + + We prove that $(W,E)$ make an adjunction showing that there is a natural isomorphism between $\Hom$ sets in both categories. + + We want to construct for each $(X,Y)$ in $\displaystyle\prod_{X : \BB_{i-1}} (\Set/\Hom_{\BB_{i-1}}(G_{i-1}\Gamma_i,X))$ and $Z$ in $\BB_i$, an isomorphism $\phi_{XYZ}$. + + \[ + \phi_{XYZ} : \Hom(W(X,Y),Z) \to \Hom((X,Y),E(Z)) + \] + + I will give the construction of the isomorphisms and its inverse, the proofs are given in \autoref{apx:phi-WE-isnat}. + + \paragraph{Constructing $\phi_{XYZ}$} - \subsection{W E adjunction} - - We have an adjunction $W \dashv E$. - - Let $(X,Y)$ be in $\displaystyle\prod_{X : \BB_{i-1}} (\Set/\Hom_{\BB_{i-1}}(G_{i-1}\Gamma_i,X))$ and $Z$ be in $\BB_i$. - - We will construct a natural isomorphism. - \[ - \phi_{XYZ} : \Hom(W(X,Y),Z) \to \Hom((X,Y),E(Z)) - \] - - \subsubsection{Constructing $\phi_{XYZ}$} Let $f$ be in $\Hom(W(X,Y),Z)$. We want to construct $\phi_{XYZ}(f) : (X,Y) \to E(Z)$. @@ -188,104 +354,45 @@ The second component is defined through the universal property of the pullback defined by $E(Z)$ according to the following diagram: - \diagram{D6} + \begin{center} + % YADE DIAGRAM D6.json + % GENERATED LATEX + \input{graphs/D6.tex} + % END OF GENERATED LATEX + \end{center} - \subsubsection{Constructing $\phi^{-1}_{XYZ}$} + \paragraph{Constructing $\phi^{-1}_{XYZ}$} 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: \[ - \phi^{-1}_{XYZ}(g,h) = \left\{g ; \eta_0^i \circ L_0^{i-1} \square \right\} + \phi^{-1}_{XYZ}(g,h) := \left\{g ; \varepsilon_0^i \circ L_0^{i-1} \square \right\} \] Where $\square$ is a morphism $\Hbar (X,Y) \to R_0^i Z$ defined by the following diagram: - \diagram{D7} - + \begin{center} + % YADE DIAGRAM D7.json + % GENERATED LATEX + \input{graphs/D7.tex} + % END OF GENERATED LATEX + \end{center} This is indeed a morphism of $\BB_i$ from $W(X,Y)$ to $Z$ as it makes the following diagram commute - \diagram{D8} + \begin{center} + % YADE DIAGRAM D8.json + % GENERATED LATEX + \input{graphs/D8.tex} + % END OF GENERATED LATEX + \end{center} - We now have to show that $\phi_{XYZ}$ and $\phi_{XYZ}^{-1}$ do make a natural isomorphism. + We show in \autoref{apx:phi-WE-isnat} that $\phi_{XYZ}$ and $\phi_{XYZ}^{-1}$ do indeed make a natural isomorphism. - \subsubsection{Composition $\phi_{XYZ} \circ \phi_{XYZ}^{-1}$} - The first component of $\phi_{XYZ} (\phi_{XYZ}^{-1}(g,h))$ is - \[ - R_{i-1}^i(\left\{g ; \eta_0^i \circ L_0^{i-1} \square \right\}) \circ \inj_1^{i-1} = \left\{g ; \eta_0^i \circ L_0^{i-1} \square \right\} \circ \inj_1^{i-1} = g - \] - The second component of $\phi_{XYZ} (\phi_{XYZ}^{-1}(g,h))$ follows the following diagram - - \diagram{D9} - - The diagram commutes as the following equality holds: - \[ - \left(\left\{g ; \eta_0^i \circ L_0^{i-1} \square \right\} \circ \inj^{i-1}_2\right)_\El = \left(\eta_0^i \circ L_0^{i-1} \square\right)_\El = (\eta_0^i)_\El \circ (L_0^{i-1} \square)_\El = \square_El = \pi_1 \circ h - \] - - \todo{Justify $(\eta_0^i)_\El = id_{\BB_i}$ and $(L_0^i(f))_\El = f_\El$} - - So, as the square is a pullback, we get the complete equality - \[ - \phi_{XYZ} (\phi_{XYZ}^{-1}(g,h)) = (g,h) - \] - - \subsubsection{Composition $\phi_{XYZ}^{-1} \circ \phi_{XYZ}$} - - Now, the converse composition is - - \[ - \phi_{XYZ}^{-1} (\phi_{XYZ}(f)) = \left\{R_{i-1}^i f \circ \inj_1^{i-1} ; \eta_0^i \circ L_0^{i-1} \square \right\} - \] - where $\square$ follows the following diagram - - \diagram{D10} - - We want to show that $\phi_{XYZ}^{-1} (\phi_{XYZ}(f))$. By definition of $\{;\}$ in $\BB_1$, it suffices to show that $\eta_0^i \circ L_0^{i-1} \square = R_{i-1}^i f \circ \inj_1^{i-1}$. - - So it suffices to show that - \[ - \square = R_0^{i-1}(R_{i-1}^i f \circ \inj_2^{i-1}) \circ \varepsilon_0^{i-1} = R_0^i f \circ \left(R_0^{i-1} \inj_2^{i-1} \circ \varepsilon_0^{i-1}\right) = R_0^i f \circ \inj_2^0 - \] - - The two required equalities are proved by the diagram above: - - \begin{align*} - \square_\El = \left(R_0^i f \circ \inj_2^0\right)_\El \\ - \square_\UU = \left(R_0^i f \circ \inj_2^0\right)_\UU - \end{align*} - - \todo{Expliciter à un endroit que $\Cstr^{W(X,Y)} = inj_2^\Set \circ \left(\inj_1^{i-1} \circ \dash\right)$ (déduit de la définition et de la forme de l'iso H3' et H1r=id)} - - \todo{Show $R_0^{i-1} \inj_2^{i-1} \circ \varepsilon_0^{i-1} = \inj_2^0$} - - \subsubsection{Naturality} - - We want to show that the following diagram commutes, for any objects $X$,$Y$,$Z$,$X'$,$Y'$,$Z'$ and morphisms $f$,$g$,$h$. - - \diagram{D10.0} - - We take a morphism $\ii$ in $\Hom\left(W(X,Y),Z\right)$. We want to show that it is sent by the above diagram to the same morphism of $\Hom\left((X,Y),E(Z)\right)$. - - We first look at the first component of the result morphism. - - \[\begin{array}{rcl} - \phi_{XYZ}(f \circ \ii \circ W(g,h))_1 - &=& R_{i-1}^i\left(f \circ \ii \circ (g \oplus L_0^{i-1} \Hbar(g,h))^+\right) \circ \inj_1^{i-1} \\ - &=& R_{i-1}^i f \circ R_{i-1}^i \ii \circ \left\{\inj_1^{i-1} \circ g; \dots\right\} \circ \inj_1^{i-1} \\ - &=& R_{i-1}^i f \circ R_{i-1}^i \ii \circ \inj_1^{i-1} \circ g \\ - &=& \left[E(f) \circ \phi_{X'Y'Z'}(\ii) \circ (g,h)\right]_1 - \end{array}\] - - The second components are defined as described by the following diagram - - \diagram{D10} - - The second projection of $\phi_{XYZ}(f \circ \ii \circ W(g,h))$ is defined by the pullback of $E(Z')$ commuting with the two path highlighted by the blue line. And that of $E(f) \circ \phi_{X'Y'Z'}(\ii) \circ (g,h)$ is defined by the circled path. - As the diagram commutes and by pullback property, we get the equality. + \subsection{$F \vdash G$ make a reflexion} \subsection{Proof of H1 - Sum definition} @@ -309,26 +416,114 @@ It is a morphism of $\BB_i$ as it makes the following diagram commute: - \diagram{D4} + \begin{center} + % YADE DIAGRAM D4.json + % GENERATED LATEX + \input{graphs/D4.tex} + % END OF GENERATED LATEX + \end{center} + The second injector is defined as follows: \[ - inj_2^i := (\eta_i \oplus_i \id_{L_0^i Y}) \circ L_{i-1}^i \inj_2^{i-1} + inj_2^i := (\varepsilon_i \oplus_i \id_{L_0^i Y}) \circ L_{i-1}^i \inj_2^{i-1} \] - Where $\eta_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$. + 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-adjunct 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 \varepsilon^i_{L_0^{i-1} Y}\}_{i-1}$ a morphism of $\BB_i$ as it makes the following diagram commute: + 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: - \diagram{D5} + \begin{center} + % YADE DIAGRAM D5.json + % GENERATED LATEX + \input{graphs/D5.tex} + % END OF GENERATED LATEX + \end{center} - \todo{Justifier $R_{i-1}^i(\eta_i \oplus_i \id_{L_0^i Y}) = R_{i-1}^i \eta_i \oplus_{i-1} \id_{L_0^{i-1} Y}$ (with H1 ?)} + \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 ?)} + + \subsection{Proof of H3} + + \subsection{Infinite construction of $\BB_i$} + \[ + \BB_i := \left(X : \TSet, \Cstr : (a : S_{i-1}) \to \Hom_{\BB_{a-1}}(G_{a-1}\Gamma_a,R_{a-1}^i(\this)) \to X(\UU)\right) + \] + A morphism from $(X,\Cstr)$ to $(X', \Cstr')$ is a morphism from $X$ to $X'$ in $\TSet$ (i.e. a natural transformation $X \implies X'$) which makes the following diagram commute, for all $a$ in $S_{i-1}$. + + \begin{center} + % YADE DIAGRAM D1.json + % GENERATED LATEX + \input{graphs/D1.tex} + % END OF GENERATED LATEX + \end{center} + + Identities and compositions are that of the base category $\TSet$, and categorical equalities are trivially derived from the diagram above. + + The diagram expresses as + \[ + \forall \gamma \in \Hom_{G_{a-1}\Gamma_a,X}, \quad \Cstr'_a(f \circ \gamma) = f_\UU(\Cstr_a \gamma) + \] + + \todo{Define properly the use of \this} + + \subsection{$G$ and $F$ infinite constructions} + + \[ + G_i(Y) = \left(\sum_{a\in S_i}H_{Y(a)}\left(\lim_{(a/S_i)*}\overline{Y_a}\right), λa.λ\eta.(a,u (\inj_2 \star))\right) + \] + + where $u : \left(Y(a) \oplus 1, \inj_1\right) \to (\lim_{(a/S_i)*} \overline{Y_a})$ + + so that $\varphi_{b,f} u (\star) = \eta_\El^b(f)$ + + \[ + F_i(X,\Cstr)(a) = X(p)^{-1}\left(\Cstr_a\left(\Hom_{\BB_{a-1}}(G_{a-1}\Gamma_a,X)\right)\right) + \] + \[ + F_i(X,\Cstr)(f : a \to b)(X(p)(x); x \in \Cstr_a(\eta)) = \eta_\El^b(f) + \] + + \todo{Show that those are the same functors as those defined recursively. Prove the adjunction/reflection infinitely ?} + + + \subsection{$H$ functors} + + For every set $X$, we define the functor $H_X : (X/\Set) \to \TSet$ + \[ + H_X(Y,f) = \TSetObject{X}{f}{Y} + \] + + Dually, we make another functor $\Hbar_X : (\Set/X) \to \TSet$ + \[ + \Hbar_X(Y,f) = \TSetObject{Y}{f}{X} + \] + + The morphisms translate as-is, and composition and identity relies on that of $(X/\Set)$ or $(\Set/X)$. + + \todo{(small) Show that it is actually a functor (should be trivial), potentially add a diagram} + + + \subsection{Overview} + + We use the specification of sorts definition of Fiore \cite{Fiore2008}. + + A specification of sorts is given by a sequence of functors $\Gamma_i : S_{i-1} \to \Set$. We construct the category $S_{i+1}$ by adding a single object $\alpha_{i+1}$ to the category $S_{i}$, along with morphisms $f : \alpha_j \to \alpha_{i+1}$ for $f \in \Gamma_{i+1}(\alpha_j)$ and $j \leq i$. The morphisms follow the composition condition, describing that every pair of morphisms $f : \alpha_j \to \alpha_{i+1}$ and $g : \alpha_k \to \alpha_{i+1}$ (i.e. $f\in\Gamma_{i+1}(\alpha_k)$ and $g\in\Gamma_{i+1}(\alpha_j)$) and for every morphism of $S_{i}$ $h : \alpha_j \to \alpha_k$, we have $\Gamma_{i+1}(h)(f) \circ f = g$. + + We have define a sequence of direct categories $\emptyset = S_0 \subset S_1 \subset S_2 \subset \dots$ (with inclusions functors $I_i : S_{i+1} \to S_i$). We define the \enquote{final} direct category as $S = \bigcup S_i$ + + This definition is an isomorphism, so we can define a GAT categorically as any locally finite direct category. + + Then the semantics of the GAT is described as the category of presheaves over $S$, written $[S, \Set]$. + + Altenkirsch has another way of constructing the semantics of a specification of sorts \cite{Altenkirch2018}, and he also describes a way to describe constructors. + + So we can construct the base category, which is that of families of sets. \section{Summary} @@ -348,5 +543,106 @@ \addtocontents{toc}{\protect\setcounter{tocdepth}{-1}} \appendixpage + \section{$W \dashv E$ adjunction} + \label{apx:phi-WE-isnat} + + + \subsection{Composition $\phi_{XYZ} \circ \phi_{XYZ}^{-1}$} + + The first component of $\phi_{XYZ} (\phi_{XYZ}^{-1}(g,h))$ is + \[ + R_{i-1}^i(\left\{g ; \varepsilon_0^i \circ L_0^{i-1} \square \right\}) \circ \inj_1^{i-1} = \left\{g ; \varepsilon_0^i \circ L_0^{i-1} \square \right\} \circ \inj_1^{i-1} = g + \] + + The second component of $\phi_{XYZ} (\phi_{XYZ}^{-1}(g,h))$ follows the following diagram + + \begin{center} + % YADE DIAGRAM D9.json + % GENERATED LATEX + \input{graphs/D9.tex} + % END OF GENERATED LATEX + \end{center} + + The diagram commutes as the following equality holds: + \[ + \left(\left\{g ; \varepsilon_0^i \circ L_0^{i-1} \square \right\} \circ \inj^{i-1}_2\right)_\El = \left(\varepsilon_0^i \circ L_0^{i-1} \square\right)_\El = (\varepsilon_0^i)_\El \circ (L_0^{i-1} \square)_\El = \square_El = \pi_1 \circ h + \] + + \todo{Justify $(\varepsilon_0^i)_\El = id_{\BB_i}$ and $(L_0^i(f))_\El = f_\El$} + + So, as the square is a pullback, we get the complete equality + \[ + \phi_{XYZ} (\phi_{XYZ}^{-1}(g,h)) = (g,h) + \] + + \subsection{Composition $\phi_{XYZ}^{-1} \circ \phi_{XYZ}$} + + Now, the converse composition is + + \[ + \phi_{XYZ}^{-1} (\phi_{XYZ}(f)) = \left\{R_{i-1}^i f \circ \inj_1^{i-1} ; \varepsilon_0^i \circ L_0^{i-1} \square \right\} + \] + where $\square$ follows the following diagram + + \begin{center} + % YADE DIAGRAM D10.json + % GENERATED LATEX + \input{graphs/D10.tex} + % END OF GENERATED LATEX + \end{center} + + We want to show that $\phi_{XYZ}^{-1} (\phi_{XYZ}(f))$. By definition of $\{;\}$ in $\BB_1$, it suffices to show that $\varepsilon_0^i \circ L_0^{i-1} \square = R_{i-1}^i f \circ \inj_1^{i-1}$. + + So it suffices to show that + \[ + \square = R_0^{i-1}(R_{i-1}^i f \circ \inj_2^{i-1}) \circ \eta_0^{i-1} = R_0^i f \circ \left(R_0^{i-1} \inj_2^{i-1} \circ \eta_0^{i-1}\right) = R_0^i f \circ \inj_2^0 + \] + + The two required equalities are proved by the diagram above: + + \begin{align*} + \square_\El = \left(R_0^i f \circ \inj_2^0\right)_\El \\ + \square_\UU = \left(R_0^i f \circ \inj_2^0\right)_\UU + \end{align*} + + \todo{Expliciter à un endroit que $\Cstr^{W(X,Y)} = inj_2^\Set \circ \left(\inj_1^{i-1} \circ \dash\right)$ (déduit de la définition et de la forme de l'iso H3' et H1r=id)} + + \todo{Show $R_0^{i-1} \inj_2^{i-1} \circ \eta_0^{i-1} = \inj_2^0$} + + \subsection{Naturality} + + We want to show that the following diagram commutes, for any objects $X$,$Y$,$Z$,$X'$,$Y'$,$Z'$ and morphisms $f$,$g$,$h$. + + \begin{center} + % YADE DIAGRAM D10.0.json + % GENERATED LATEX + \input{graphs/D10.0.tex} + % END OF GENERATED LATEX + \end{center} + + We take a morphism $\ii$ in $\Hom\left(W(X,Y),Z\right)$. We want to show that it is sent by the above diagram to the same morphism of $\Hom\left((X,Y),E(Z)\right)$. + + We first look at the first component of the result morphism. + + \[\begin{array}{rcl} + \phi_{XYZ}(f \circ \ii \circ W(g,h))_1 + &=& R_{i-1}^i\left(f \circ \ii \circ (g \oplus L_0^{i-1} \Hbar(g,h))^+\right) \circ \inj_1^{i-1} \\ + &=& R_{i-1}^i f \circ R_{i-1}^i \ii \circ \left\{\inj_1^{i-1} \circ g; \dots\right\} \circ \inj_1^{i-1} \\ + &=& R_{i-1}^i f \circ R_{i-1}^i \ii \circ \inj_1^{i-1} \circ g \\ + &=& \left[E(f) \circ \phi_{X'Y'Z'}(\ii) \circ (g,h)\right]_1 + \end{array}\] + + The second components are defined as described by the following diagram + + \begin{center} + % YADE DIAGRAM D11.json + % GENERATED LATEX + \input{graphs/D11.tex} + % END OF GENERATED LATEX + \end{center} + + The second projection of $\phi_{XYZ}(f \circ \ii \circ W(g,h))$ is defined by the pullback of $E(Z')$ commuting with the two path highlighted by the blue line. And that of $E(f) \circ \phi_{X'Y'Z'}(\ii) \circ (g,h)$ is defined by the circled path. + As the diagram commutes and by pullback property, we get the equality. + \end{document} diff --git a/Report/graphs/B1.json b/Report/graphs/B1.json new file mode 100644 index 0000000..d7d4d66 --- /dev/null +++ b/Report/graphs/B1.json @@ -0,0 +1 @@ +{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":1,"id":3,"label":{"isPullshout":false,"label":"\\Gamma","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":2,"id":4,"label":{"isPullshout":false,"label":"A","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":2,"id":5,"label":{"isPullshout":false,"label":"\\Delta","style":{"alignment":"right","bend":0.10000000000000003,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":0}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\Con","pos":[100,100],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\Ty","pos":[300,100],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\Tm","pos":[500,100],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":11} \ No newline at end of file diff --git a/Report/graphs/D1.json b/Report/graphs/D1.json new file mode 100644 index 0000000..011e918 --- /dev/null +++ b/Report/graphs/D1.json @@ -0,0 +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":{"isPullshout":false,"label":"\\Cstr^X","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":5,"label":{"isPullshout":false,"label":"R_0^i X_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":6,"label":{"isPullshout":false,"label":"f \\circ \\dash","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":7,"label":{"isPullshout":false,"label":"\\Cstr^{X'}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\Hom(G_{a-1},R_{a-1}^i(X))","pos":[180,60],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"(R_0^iX)_\\UU","pos":[420,60],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i X')_\\UU","pos":[420,300],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\Hom(G_{a-1},R_{a-1}^i( X'))","pos":[180,300],"zindex":-10000}}],"sizeGrid":120,"title":"1"}]},"version":11} \ No newline at end of file diff --git a/Report/graphs/D10.0.json b/Report/graphs/D10.0.json new file mode 100644 index 0000000..e3cbf94 --- /dev/null +++ b/Report/graphs/D10.0.json @@ -0,0 +1 @@ +{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":4,"label":{"isPullshout":false,"label":"\\phi_{XYZ}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":5,"label":{"isPullshout":false,"label":"E(f) \\circ \\dash \\circ (g,h)","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":6,"label":{"isPullshout":false,"label":"f \\circ \\dash \\circ W(g,h)","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":7,"label":{"isPullshout":false,"label":"\\phi_{X'Y'Z'}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\Hom(W(X,Y),Z)","pos":[300,100],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\Hom((X,Y),E(Z))","pos":[700,100],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\Hom((X',Y'),E(Z'))","pos":[700,300],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\Hom(W(X',Y'),Z')","pos":[300,300],"zindex":-10000}}],"sizeGrid":200,"title":"1"}]},"version":11} \ No newline at end of file diff --git a/Report/graphs/D10.json b/Report/graphs/D10.json new file mode 100644 index 0000000..4ab9013 --- /dev/null +++ b/Report/graphs/D10.json @@ -0,0 +1 @@ +{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":10,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":true,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":11,"label":{"isPullshout":false,"label":"\\pi_1","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":12,"label":{"isPullshout":false,"label":"(R_0^i Z)_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":1,"id":13,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":4,"id":14,"label":{"isPullshout":false,"label":"\\Cstr^Z","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":0,"id":15,"label":{"isPullshout":false,"label":"h","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":5,"id":16,"label":{"isPullshout":false,"label":"(\\inj_1^{i-1} \\circ \\dash)","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":6,"id":17,"label":{"isPullshout":false,"label":"R_{i-1}^i f","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":0,"id":18,"label":{"isPullshout":false,"label":"\\square_\\El = \\left[R_{i-1}^i f \\circ \\inj_2^{i-1}\\right]","style":{"alignment":"left","bend":-0.1,"color":"blue","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":5,"id":19,"label":{"isPullshout":false,"label":"\\square_\\UU","style":{"alignment":"right","bend":0.2,"color":"blue","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":5,"id":20,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":true,"head":"none","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":7,"id":21,"label":{"isPullshout":false,"label":"(\\inj_2^0)_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":8},{"from":8,"id":22,"label":{"isPullshout":false,"label":"\\text{H1'}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":true,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":9},{"from":9,"id":23,"label":{"isPullshout":false,"label":"(R_0^i f)_\\UU","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":6,"id":24,"label":{"isPullshout":false,"label":"\\Cstr^{W(X,Y)}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":9},{"from":13,"id":25,"label":{"isPullshout":true,"label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"double":false,"head":"","position":0,"tail":""},"zindex":0},"to":11}],"nodes":[{"id":0,"label":{"isMath":true,"label":"Y","pos":[80,80],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"E(Z)","pos":[692,79.8125],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i Z)_\\El","pos":[880,80],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[880,240],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,R_{i-1}^i Z)","pos":[692,239.8125],"zindex":-10000}},{"id":5,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,X)","pos":[80,240],"zindex":-10000}},{"id":6,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,X \\oplus L_0^{i-1} \\Hbar Y)","pos":[400,240],"zindex":-10000}},{"id":7,"label":{"isMath":true,"label":"(\\Hbar Y)_\\UU","pos":[80,400],"zindex":0}},{"id":8,"label":{"isMath":true,"label":"\\left[R_0^{i-1} X \\oplus (\\Hbar Y)\\right]_\\UU","pos":[400,400],"zindex":0}},{"id":9,"label":{"isMath":true,"label":"\\left[R_0^i(W(X,Y))\\right]_\\UU","pos":[720,400],"zindex":0}}],"sizeGrid":160,"title":"1"}]},"version":11} \ No newline at end of file diff --git a/Report/graphs/D11.json b/Report/graphs/D11.json new file mode 100644 index 0000000..881bbeb --- /dev/null +++ b/Report/graphs/D11.json @@ -0,0 +1 @@ +{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":11,"label":{"isPullshout":false,"label":"h","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":12,"label":{"isPullshout":false,"label":"\\phi_{XYZ}(\\ii)_2","style":{"alignment":"left","bend":0,"color":"black","dashed":true,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":13,"label":{"isPullshout":false,"label":"E(f)_2","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.7,"tail":"none"},"zindex":1},"to":3},{"from":3,"id":14,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":2,"id":15,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":5,"id":16,"label":{"isPullshout":false,"label":"\\dash \\circ R_{i-1}^i f","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":3,"id":17,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":4,"id":18,"label":{"isPullshout":false,"label":"\\Cstr^{Z'}","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":6,"id":19,"label":{"isPullshout":false,"label":"(R_0^i Z')_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":2,"id":20,"label":{"isPullshout":false,"label":"\\pi_1","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":8},{"from":8,"id":21,"label":{"isPullshout":false,"label":"(R_0^i Z)_\\El","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":8,"id":22,"label":{"isPullshout":false,"label":"(R_0^i Z)_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":9},{"from":9,"id":23,"label":{"isPullshout":false,"label":"(R_0^i Z)_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":5,"id":24,"label":{"isPullshout":false,"label":"\\Cstr^Z","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":9},{"from":1,"id":25,"label":{"isPullshout":false,"label":"\\phi_{XYZ}(f \\circ \\ii \\circ W(g,h))","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":10},{"from":10,"id":26,"label":{"isPullshout":false,"label":"\\dash \\circ R_{i-1}^i \\ii","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":1,"id":27,"label":{"isPullshout":false,"label":"(R_{i-1}^i \\ii \\circ \\inj_2)_\\El","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":8},{"from":0,"id":28,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":-0.2,"color":"blue","dashed":false,"double":false,"head":"none","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":29,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":-0.30000000000000004,"color":"blue","dashed":false,"double":false,"head":"none","position":0.5,"tail":"none"},"zindex":-1},"to":8},{"from":8,"id":30,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":-0.2,"color":"blue","dashed":false,"double":false,"head":"none","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":0,"id":31,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":0.2,"color":"blue","dashed":false,"double":false,"head":"none","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":32,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":0.30000000000000004,"color":"blue","dashed":false,"double":false,"head":"none","position":0.5,"tail":"none"},"zindex":0},"to":10},{"from":10,"id":33,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":10,"id":34,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":0.30000000000000004,"color":"blue","dashed":false,"double":false,"head":"none","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":5,"id":35,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":0.30000000000000004,"color":"blue","dashed":false,"double":false,"head":"none","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":15,"id":36,"label":{"isPullshout":true,"label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"double":false,"head":"","position":0,"tail":""},"zindex":0},"to":20},{"from":14,"id":37,"label":{"isPullshout":true,"label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"double":false,"head":"","position":0,"tail":""},"zindex":0},"to":17}],"nodes":[{"id":0,"label":{"isMath":true,"label":"Y'","pos":[300,300],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"Y","pos":[500,300],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"E(Z)","pos":[700,300],"zindex":1}},{"id":3,"label":{"isMath":true,"label":"E(Z')","pos":[900,300],"zindex":1}},{"id":4,"label":{"isMath":true,"label":"\\Hom(R_{i-1}^i Z')","pos":[900,500],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"\\Hom(R_{i-1}^i Z)","pos":[700,500],"zindex":-10000}},{"id":6,"label":{"isMath":true,"label":"(R_0^i Z')_\\El","pos":[1000,144.8125],"zindex":0}},{"id":7,"label":{"isMath":true,"label":"(R_0^i Z')_\\UU","pos":[1000,344.8125],"zindex":-10000}},{"id":8,"label":{"isMath":true,"label":"(R_0^i Z)_\\El","pos":[800,144.8125],"zindex":-10000}},{"id":9,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[800,344.8125],"zindex":0}},{"id":10,"label":{"isMath":true,"label":"\\Hom(X)","pos":[500,500],"zindex":-10000}}],"sizeGrid":200,"title":"1"}]},"version":11} \ No newline at end of file diff --git a/Report/graphs/D2.json b/Report/graphs/D2.json new file mode 100644 index 0000000..111dc9d --- /dev/null +++ b/Report/graphs/D2.json @@ -0,0 +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":{"isPullshout":false,"label":"\\text{H3'}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":true,"head":"none","position":0.5,"tail":"none"},"zindex":-1},"to":1},{"from":2,"id":11,"label":{"isPullshout":false,"label":"\\inj_2^0","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":12,"label":{"isPullshout":false,"label":"\\text{H1r}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":true,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":4,"id":13,"label":{"isPullshout":false,"label":"R_0^i(g \\oplus L_0^{i-1}\\Hbar_\\bullet(g,h))_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":3,"id":14,"label":{"isPullshout":false,"label":"(R_0^i g \\oplus \\Hbar(g,h))_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":6,"id":15,"label":{"isPullshout":false,"label":"\\text{H1r}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":true,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":2,"id":16,"label":{"isPullshout":false,"label":"\\left[\\Hbar_\\bullet(g,h)\\right]_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":1,"id":17,"label":{"isPullshout":false,"label":"g \\circ \\dash","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":8},{"from":8,"id":18,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":true,"head":"none","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":0,"id":19,"label":{"isPullshout":false,"label":"(g \\oplus L_0^{i-1}\\Hbar_\\bullet(g,h)) \\circ \\dash","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":9},{"from":9,"id":20,"label":{"isPullshout":false,"label":"H3'","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":true,"head":"none","position":0.5,"tail":"none"},"zindex":0},"to":8},{"from":7,"id":21,"label":{"isPullshout":false,"label":"\\inj_2^0","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":1,"id":22,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":true,"head":"none","position":0.5,"tail":"none"},"zindex":0},"to":2}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,X \\oplus L_0^{i-1}\\Hbar_\\bullet(X,Y))","pos":[300,100],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,X)","pos":[700,100],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\left[\\Hbar_\\bullet(X,Y)\\right]_\\UU","pos":[900,100],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\left[R_0^{i-1} X \\oplus \\Hbar_\\bullet(X,Y)\\right]_\\UU","pos":[1300,100],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"R_0^{i-1}(X \\oplus L_0^{i-1} \\Hbar_\\bullet(X,Y))_\\UU","pos":[1700,100],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"R_0^{i-1}(X' \\oplus L_0^{i-1} \\Hbar_\\bullet(X',Y'))_\\UU","pos":[1700,300],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"\\left[R_0^{i-1} X' \\oplus \\Hbar_\\bullet(X',Y')\\right]_\\UU","pos":[1300,300],"zindex":-10000}},{"id":7,"label":{"isMath":true,"label":"\\left[\\Hbar_\\bullet(X',Y')\\right]_\\UU","pos":[900,300],"zindex":0}},{"id":8,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,X')","pos":[700,300],"zindex":0}},{"id":9,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,X' \\oplus L_0^{i-1}\\Hbar_\\bullet(X',Y'))","pos":[300,300],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":11} \ No newline at end of file diff --git a/Report/graphs/D3a.json b/Report/graphs/D3a.json new file mode 100644 index 0000000..97ad4fe --- /dev/null +++ b/Report/graphs/D3a.json @@ -0,0 +1 @@ +{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":4,"label":{"isPullshout":false,"label":"h","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":0,"id":5,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":6,"label":{"isPullshout":false,"label":"R_0^i(X)_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":1,"id":7,"label":{"isPullshout":false,"label":"\\Cstr^X_i","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","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":"\\Hom(G_{i-1}\\Gamma_i,R_{i-1}^i X)","pos":[100,317.8125],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"R_0^i(X)_\\El","pos":[300,117.8125],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"R_0^i(X)_\\UU","pos":[300,317.8125],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":11} \ No newline at end of file diff --git a/Report/graphs/D3b.json b/Report/graphs/D3b.json new file mode 100644 index 0000000..13e2ced --- /dev/null +++ b/Report/graphs/D3b.json @@ -0,0 +1 @@ +{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":8,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":9,"label":{"isPullshout":false,"label":"R_0^i(X)_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":10,"label":{"isPullshout":false,"label":"h","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":11,"label":{"isPullshout":false,"label":"\\Cstr^X_i","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":4,"id":12,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":5,"id":13,"label":{"isPullshout":false,"label":"R_0^i(X')_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":4,"id":14,"label":{"isPullshout":false,"label":"h'","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":7,"id":15,"label":{"isPullshout":false,"label":"\\Cstr^{X'}_i","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":0,"id":16,"label":{"isPullshout":false,"label":"!","style":{"alignment":"left","bend":0,"color":"black","dashed":true,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":1},"to":4},{"from":1,"id":17,"label":{"isPullshout":false,"label":"R_0^i(f)_\\El","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":3,"id":18,"label":{"isPullshout":false,"label":"\\dash \\circ R_{i-1}^i f","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.10000000000000003,"tail":"none"},"zindex":0},"to":7},{"from":2,"id":19,"label":{"isPullshout":false,"label":"R_0^i(f)_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.6,"tail":"none"},"zindex":0},"to":6},{"from":14,"id":20,"label":{"isPullshout":true,"label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"double":false,"head":"","position":0,"tail":""},"zindex":0},"to":12},{"from":10,"id":21,"label":{"isPullshout":true,"label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"double":false,"head":"","position":0,"tail":""},"zindex":0},"to":8}],"nodes":[{"id":0,"label":{"isMath":true,"label":"A","pos":[125,125],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"R_0^i(X)_\\El","pos":[375,125],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"R_0^i(X)_\\UU","pos":[375,375],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,R_{i-1}^i X)","pos":[125,375],"zindex":-10000}},{"id":4,"label":{"isMath":true,"label":"A'","pos":[243,200.8125],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"R_0^i(X')_\\El","pos":[493,200.8125],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"R_0^i(X')_\\UU","pos":[493,450.8125],"zindex":0}},{"id":7,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,R_{i-1}^i X')","pos":[243,450.8125],"zindex":-10000}}],"sizeGrid":250,"title":"1"}]},"version":11} \ No newline at end of file diff --git a/Report/graphs/D4.json b/Report/graphs/D4.json new file mode 100644 index 0000000..e877162 --- /dev/null +++ b/Report/graphs/D4.json @@ -0,0 +1 @@ +{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":6,"label":{"isPullshout":false,"label":"\\Cstr^X","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":7,"label":{"isPullshout":false,"label":"(R_0^{i-1} (\\inj_1^{i-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":8,"label":{"isPullshout":false,"label":"\\inj_1^{i-1} \\circ \\dash","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":4,"id":9,"label":{"isPullshout":false,"label":"R_0^{i-1}(\\inj_1^{i-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":3,"id":10,"label":{"isPullshout":false,"label":"(\\inj_1^{i-1} \\circ \\dash)^{-1}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.20000000000000004,"tail":"none"},"zindex":0},"to":5},{"from":5,"id":11,"label":{"isPullshout":false,"label":"\\Cstr^X","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":0,"id":12,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":true,"head":"none","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":4,"id":13,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":true,"head":"none","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":3,"id":14,"label":{"isPullshout":false,"label":"\\Cstr^{X \\oplus L_0^i Y}","style":{"alignment":"left","bend":0.1,"color":"green","dashed":true,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,R_{i-1}^i X)","pos":[220.5,73.5],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"(R_0^i X)_\\UU","pos":[951,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":[955.5,367.5],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,R_{i-1}^i X \\oplus_{i-1} L_0^{i-1} Y)","pos":[220.5,367.5],"zindex":-10000}},{"id":4,"label":{"isMath":true,"label":"(R_0^i X)_\\UU","pos":[718,301.8125],"zindex":-10000}},{"id":5,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,R_{i-1}^i X)","pos":[448,300.8125],"zindex":-10000}}],"sizeGrid":147,"title":"1"}]},"version":11} \ No newline at end of file diff --git a/Report/graphs/D5.json b/Report/graphs/D5.json new file mode 100644 index 0000000..89f2b1e --- /dev/null +++ b/Report/graphs/D5.json @@ -0,0 +1 @@ +{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":6,"label":{"isPullshout":false,"label":"(\\inj_1 \\circ \\dash)","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":true,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":7,"label":{"isPullshout":false,"label":"\\Cstr^X","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":8,"label":{"isPullshout":false,"label":"\\{\\varphi_1 ; \\varphi_2\\} \\circ \\dash","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":2,"id":9,"label":{"isPullshout":false,"label":"(R_0^{i-1} \\inj_1^{i-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"twoheads","position":0.30000000000000004,"tail":"none"},"zindex":0},"to":4},{"from":4,"id":10,"label":{"isPullshout":false,"label":"(R_0^i \\{\\varphi_1;\\varphi_2\\})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":3,"id":11,"label":{"isPullshout":false,"label":"\\Cstr^Z","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":1,"id":12,"label":{"isPullshout":false,"label":"R_{i-1}^i \\varphi_1 \\circ \\dash","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":2,"id":13,"label":{"isPullshout":false,"label":"(R_0^i \\varphi_1)_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":5}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,R_{i-1}^i X \\oplus L_0^{i-1} Y)","pos":[225,75],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,R_{i-1}^i X)","pos":[525,75],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i X)_\\UU","pos":[681,241.8125],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,R_{i-1}^i Z)","pos":[225,375],"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":[825,75],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[825,375],"zindex":0}}],"sizeGrid":150,"title":"1"}]},"version":11} \ No newline at end of file diff --git a/Report/graphs/D6.json b/Report/graphs/D6.json new file mode 100644 index 0000000..27fe43e --- /dev/null +++ b/Report/graphs/D6.json @@ -0,0 +1 @@ +{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":6,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":7,"label":{"isPullshout":false,"label":"(R_0^i Z)_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":8,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":9,"label":{"isPullshout":false,"label":"\\Cstr^Z","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":4,"id":10,"label":{"isPullshout":false,"label":"h","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":5,"id":11,"label":{"isPullshout":false,"label":"\\dash \\circ R_{i-1}^i f \\circ \\inj_1","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":4,"id":12,"label":{"isPullshout":false,"label":"\\left[R_{i-1}^i f \\circ \\inj_2\\right]_\\El","style":{"alignment":"left","bend":-0.2,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":4,"id":13,"label":{"isPullshout":false,"label":"\\phi_{XYZ}(f)_2","style":{"alignment":"left","bend":0,"color":"black","dashed":true,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":0}],"nodes":[{"id":0,"label":{"isMath":true,"label":"E(z)","pos":[300,300],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"(R_0^i Z)_\\El","pos":[500,300],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[500,500],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,R_{i-1}^i Z)","pos":[300,500],"zindex":-10000}},{"id":4,"label":{"isMath":true,"label":"A","pos":[100,100],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,X)","pos":[100,300],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":11} \ No newline at end of file diff --git a/Report/graphs/D7.json b/Report/graphs/D7.json new file mode 100644 index 0000000..1f97acc --- /dev/null +++ b/Report/graphs/D7.json @@ -0,0 +1 @@ +{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":6,"label":{"isPullshout":false,"label":"h","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":7,"label":{"isPullshout":false,"label":"\\pi_1","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":8,"label":{"isPullshout":false,"label":"(R_0^i Z)_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":1,"id":9,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":4,"id":10,"label":{"isPullshout":false,"label":"\\Cstr^Z","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":0,"id":11,"label":{"isPullshout":false,"label":"h","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":5,"id":12,"label":{"isPullshout":false,"label":"g \\circ \\dash","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":0,"id":13,"label":{"isPullshout":false,"label":"\\square_\\El","style":{"alignment":"left","bend":-0.10000000000000003,"color":"blue","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":5,"id":14,"label":{"isPullshout":false,"label":"\\square_\\UU","style":{"alignment":"right","bend":0.10000000000000003,"color":"blue","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":3}],"nodes":[{"id":0,"label":{"isMath":true,"label":"Y","pos":[130,130],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"E(Z)","pos":[390,130],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i Z)_\\El","pos":[650,130],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[650,390],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,R_{i-1}^i Z)","pos":[390,390],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,X)","pos":[130,390],"zindex":-10000}}],"sizeGrid":260,"title":"1"}]},"version":11} \ No newline at end of file diff --git a/Report/graphs/D8.json b/Report/graphs/D8.json new file mode 100644 index 0000000..4447ada --- /dev/null +++ b/Report/graphs/D8.json @@ -0,0 +1 @@ +{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":8,"label":{"isPullshout":false,"label":"\\text{H3'}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":true,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":9,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":true,"head":"none","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":10,"label":{"isPullshout":false,"label":"\\inj_2^0","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":11,"label":{"isPullshout":false,"label":"\\text{H1r}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":true,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":4,"id":12,"label":{"isPullshout":false,"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,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":2,"id":13,"label":{"isPullshout":false,"label":"(\\varepsilon_0^{i-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":6,"id":14,"label":{"isPullshout":false,"label":"(R_0^{i-1} \\inj_2^{i-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":6,"id":15,"label":{"isPullshout":false,"label":"R_0^{i-1}(\\eta_0^i \\circ L_0^{i-1} \\square)_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":2,"id":16,"label":{"isPullshout":false,"label":"\\square_\\UU \\circ \\Cstr^Z \\circ (g \\circ \\dash)","style":{"alignment":"right","bend":0.1,"color":"black","dashed":false,"double":false,"head":"default","position":0.20000000000000004,"tail":"none"},"zindex":0},"to":5},{"from":0,"id":17,"label":{"isPullshout":false,"label":"\\left\\{g;\\eta_0^i \\circ L_0^{i-1} \\square \\right\\} \\circ \\dash","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":7,"id":18,"label":{"isPullshout":false,"label":"\\Cstr^Z","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":1,"id":19,"label":{"isPullshout":false,"label":"g \\circ \\dash","style":{"alignment":"left","bend":0,"color":"red","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":7}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,X \\oplus L_0^{i-1}\\Hbar(X,Y))","pos":[210,70],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,X)","pos":[334,198.8125],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\Hbar(X,Y)_\\UU","pos":[426,70.8125],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\left[R_0^{i-1} X \\oplus \\Hbar(X,Y)\\right]_\\UU","pos":[620.9999999999999,67.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":[901,67.8125],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[901,347.8125],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"\\left[R_0^{i-1}L_0^{i-1}\\Hbar(X,Y)\\right]_\\UU","pos":[704,204.625],"zindex":0}},{"id":7,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,R_{i-1}^i Z)","pos":[210,350],"zindex":0}}],"sizeGrid":140,"title":"1"}]},"version":11} \ No newline at end of file diff --git a/Report/graphs/D9.json b/Report/graphs/D9.json new file mode 100644 index 0000000..9b4a2af --- /dev/null +++ b/Report/graphs/D9.json @@ -0,0 +1 @@ +{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":1,"id":6,"label":{"isPullshout":false,"label":"\\pi_1","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":7,"label":{"isPullshout":false,"label":"(R_0^i Z)_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":1,"id":8,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":4,"id":9,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":0,"id":10,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":5,"id":11,"label":{"isPullshout":false,"label":"\\dash \\circ g","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":0,"id":12,"label":{"isPullshout":false,"label":"(\\left\\{g;\\eta_0^i \\circ L_0^{i-1} \\square \\right\\} \\circ \\inj_2)_\\El","style":{"alignment":"left","bend":-0.30000000000000004,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":13,"label":{"isPullshout":false,"label":"h","style":{"alignment":"left","bend":0.2,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":0,"id":14,"label":{"isPullshout":false,"label":"\\phi_{XYZ}(\\phi^{-1}_{XYZ}(g,h))_2","style":{"alignment":"left","bend":-0.2,"color":"black","dashed":false,"double":false,"head":"default","position":0.7,"tail":"none"},"zindex":0},"to":1},{"from":8,"id":15,"label":{"isPullshout":true,"label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"double":false,"head":"","position":0,"tail":""},"zindex":0},"to":6}],"nodes":[{"id":0,"label":{"isMath":true,"label":"Y","pos":[300,100],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"E(Z)","pos":[500,300],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i Z)_\\El","pos":[700,300],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[700,500],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,R_{i-1}^i Z)","pos":[500,500],"zindex":-10000}},{"id":5,"label":{"isMath":true,"label":"\\Hom(G_{i-1}\\Gamma_i,X)","pos":[300,300],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":11} \ No newline at end of file diff --git a/Report/graphs/G0.json b/Report/graphs/G0.json new file mode 100644 index 0000000..943aa5c --- /dev/null +++ b/Report/graphs/G0.json @@ -0,0 +1 @@ +{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":1,"id":2,"label":{"isPullshout":false,"label":"p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":0}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\UU","pos":[100,300],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\El","pos":[100,100],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":11} \ No newline at end of file diff --git a/Report/graphs/G1.json b/Report/graphs/G1.json new file mode 100644 index 0000000..9784b62 --- /dev/null +++ b/Report/graphs/G1.json @@ -0,0 +1 @@ +{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":13,"label":{"isPullshout":false,"label":"F_i","style":{"alignment":"right","bend":0.20000000000000004,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":14,"label":{"isPullshout":false,"label":"G_i","style":{"alignment":"right","bend":0.20000000000000004,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":0,"id":15,"label":{"isPullshout":false,"label":"R_{i-1}^i","style":{"alignment":"right","bend":0.20000000000000004,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":16,"label":{"isPullshout":false,"label":"L_{i-1}^i","style":{"alignment":"right","bend":0.2,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":1,"id":17,"label":{"isPullshout":false,"label":"\\dash \\circ I_i","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":2,"id":18,"label":{"isPullshout":false,"label":"F_{i-1}","style":{"alignment":"right","bend":0.2,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":19,"label":{"isPullshout":false,"label":"G_{i-1}","style":{"alignment":"right","bend":0.2,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":3,"id":20,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":2,"id":21,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":0.2,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":5,"id":22,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":0.2,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":5,"id":23,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":0.2,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":6,"id":24,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":0.2,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":4,"id":25,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":6,"id":26,"label":{"isPullshout":false,"label":"L_0^i","style":{"alignment":"right","bend":-0.6,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":0,"id":27,"label":{"isPullshout":false,"label":"R_0^i","style":{"alignment":"right","bend":0.9999999999999999,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":6,"id":28,"label":{"isPullshout":false,"label":"\\lambda.\\star","style":{"alignment":"right","bend":0.20000000000000004,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":7,"id":29,"label":{"isPullshout":false,"label":"\\lambda.1","style":{"alignment":"right","bend":0.20000000000000004,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":6}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\BB_i","pos":[195,61],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\left[S_i,\\Set\\right]","pos":[474,61],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\BB_{i-1}","pos":[195,225],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\left[S_{i-1},\\Set\\right]","pos":[474,225],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"\\vdots","pos":[474,328],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"\\vdots","pos":[195,328],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"\\BB_0 = \\TSet","pos":[195,431],"zindex":0}},{"id":7,"label":{"isMath":true,"label":"\\left[\\emptyset,\\Set\\right] = 1","pos":[474,431],"zindex":0}},{"id":8,"label":{"isMath":true,"label":"\\vdash","pos":[33,245.8125],"zindex":0}},{"id":9,"label":{"isMath":true,"label":"\\vdash","pos":[195,160.8125],"zindex":0}},{"id":10,"label":{"isMath":true,"label":"\\bot","pos":[323,60.8125],"zindex":0}},{"id":11,"label":{"isMath":true,"label":"\\bot","pos":[327,223.8125],"zindex":0}},{"id":12,"label":{"isMath":true,"label":"\\bot","pos":[336,430.8125],"zindex":0}}],"sizeGrid":130,"title":"1"}]},"version":11} \ No newline at end of file diff --git a/Report/graphs/G2.json b/Report/graphs/G2.json new file mode 100644 index 0000000..59db84c --- /dev/null +++ b/Report/graphs/G2.json @@ -0,0 +1 @@ +{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":7,"label":{"isPullshout":false,"label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"double":true,"head":"none","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":8,"label":{"isPullshout":false,"label":"G_{i-1} \\times \\id","style":{"alignment":"right","bend":0.30000000000000004,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":9,"label":{"isPullshout":false,"label":"F_{i-1} \\times \\id","style":{"alignment":"right","bend":0.30000000000000004,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":2,"id":10,"label":{"isPullshout":false,"label":"W","style":{"alignment":"right","bend":0.30000000000000004,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":11,"label":{"isPullshout":false,"label":"E","style":{"alignment":"right","bend":0.30000000000000004,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":12,"label":{"isPullshout":false,"label":"G_i","style":{"alignment":"right","bend":0.5,"color":"black","dashed":false,"double":false,"head":"default","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":13,"label":{"isPullshout":false,"label":"F_i","style":{"alignment":"right","bend":-0.30000000000000004,"color":"black","dashed":false,"double":false,"head":"default","position":0.6,"tail":"none"},"zindex":0},"to":0}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\left[S_i,\\Set\\right]","pos":[176,99.8125],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\left(X : \\left[S_{i-1},\\Set\\right]\\right) \\times \\left.\\Set\\middle/\\Hom(\\Gamma_i,X)\\right.","pos":[500,100],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\left(X : \\BB_{i-1}\\right) \\times \\left.\\Set\\middle/\\Hom(G_{i-1}\\Gamma_i,X)\\right.","pos":[500,197.8125],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\BB_i","pos":[500,300],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"\\dashv","pos":[499,150.8125],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"\\dashv","pos":[500,251.8125],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"\\top","pos":[284,260.8125],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":11} \ No newline at end of file diff --git a/Report/header.tex b/Report/header.tex index 46d1fd8..81a7413 100644 --- a/Report/header.tex +++ b/Report/header.tex @@ -39,6 +39,7 @@ \usepackage{pdfpages} \usepackage{lipsum} \usepackage{newunicodechar} +\usepackage{yade} \usepackage[textheight=0.75\paperheight]{geometry} @@ -69,6 +70,7 @@ \newtheorem{theorem}{Théorème} \newtheorem{definition}{Definition} \newtheorem{property}{Propriété} +\newtheorem{remark}{Remark} \newcounter{rule} \addto\extrasfrench{% @@ -103,6 +105,9 @@ \newcommand\UU{{\ensuremath{\mathcal{U}}}} \newcommand\El{{\ensuremath{\operatorname{\mathcal{E}l}}}} \newcommand\ii{{\ensuremath{\mathbf{i}}}} +\newcommand\Con{{\ensuremath{\operatorname{Con}\;}}} +\newcommand\Ty{{\ensuremath{\operatorname{Ty}\;}}} +\newcommand\Tm{{\ensuremath{\operatorname{Tm}\;}}} \newcommand\Cstr{{\ensuremath{\operatorname{\mathcal{C}str}}}} \newcommand\Set{{\ensuremath{\operatorname{\mathcal{S}et}}}} \newcommand\Hom{{\ensuremath{\operatorname{\mathcal{H}om}}}} @@ -134,6 +139,14 @@ \right] }}} +\newcommand\simpleArrow[3]{ + \begin{tikzpicture} + \node (0) at (0,0) {$#1$}; + \node (1) at (6,0) {$#3$}; + \path[->] (0) edge["${\scriptstyle #2}$", pos=0.5, fore, black,=>, ] (1); + \end{tikzpicture} +} + \newcommand\diagram[1]{\begin{tcolorbox}\begin{center}\vspace{1.5cm}\Huge \texttt{\textbf{#1}}\vspace{1.5cm}\end{center}\end{tcolorbox}} \newcommand\todo[1]{\begin{tcolorbox}[colback=red!20!white,colframe=red!85!black,boxrule=4pt] #1 \end{tcolorbox}} diff --git a/Report/yade-preamble.tex b/Report/yade-preamble.tex new file mode 100644 index 0000000..306efba --- /dev/null +++ b/Report/yade-preamble.tex @@ -0,0 +1,15 @@ +\newcommand\ensuremath[1]{#1} +\newcommand\BB{{\ensuremath{\mathcal{B}}}} +\newcommand\TT{{\ensuremath{\mathcal{T}}}} +\newcommand\UU{{\ensuremath{\mathcal{U}}}} +\newcommand\El{{\ensuremath{\operatorname{\mathcal{E}l}}}} +\newcommand\ii{{\ensuremath{\mathbf{i}}}} +\newcommand\Cstr{{\ensuremath{\operatorname{\mathcal{C}str}}}} +\newcommand\Set{{\ensuremath{\operatorname{\mathcal{S}et}}}} +\newcommand\Hom{{\ensuremath{\operatorname{\mathcal{H}om}}}} +\newcommand\this{{\ensuremath{\operatorname{\texttt{this}}}}} +\newcommand\Hbar{{\ensuremath{\overline{H}}}} +\newcommand\dash{{\;\textrm{---}\;}} + +\newcommand\inj{\operatorname{inj}} +\newcommand\id{\operatorname{id}} \ No newline at end of file diff --git a/Report/yade.sty b/Report/yade.sty new file mode 100644 index 0000000..c887f07 --- /dev/null +++ b/Report/yade.sty @@ -0,0 +1,960 @@ +% Copyright 2022 by Tom Hirschowitz +% +% This file may be distributed and/or modified +% +% 1. under the LaTeX Project Public License and/or +% 2. under the GNU Public License. +% +\NeedsTeXFormat{LaTeX2e} +\ProvidesPackage{yade}[2022/06/07 v0.1 tikz categorical diagrams library] +\RequirePackage{tikz} +\RequirePackage{ifthen} +\RequirePackage{xparse} + + +\usetikzlibrary{shapes.geometric} +\usetikzlibrary{shapes.symbols} +\usetikzlibrary{shapes.arrows} +\usetikzlibrary{positioning} +\usetikzlibrary{matrix} +\usetikzlibrary{fit} +\usetikzlibrary{calc} +\usetikzlibrary{decorations} +\usetikzlibrary{decorations.markings} +\usetikzlibrary{decorations.pathreplacing} +\usetikzlibrary{decorations.pathmorphing} +\usetikzlibrary{arrows} +\usetikzlibrary{backgrounds} +\usetikzlibrary{quotes} +\pgfkeys{/pgf/.cd, + arity/.initial=4, +} + + + +\def\twocell{% + \@ifnextchar[{\twocell@i}{\twocell@i[.4]}% +} +\def\twocell@i[#1]{% + \@ifnextchar[{\twocell@ii[#1]}{\twocell@ii[#1][#1]}% +} +\def\twocell@ii[#1][#2]{% + \deuxcellule{#1}{#2}% +} + +% A TikZ style for curved arrows, inspired by AndréC's. +\tikzset{curve/.style={settings={#1},to path={ + let \p1 = ($(\tikztostart) - (\tikztotarget)$) in + (\tikztostart) +.. controls +($(\tikztostart)!\pv{pos}!(\tikztotarget)!{veclen(\x1,\y1)*\pv{ratio}*1pt}!270:(\tikztotarget)$) +and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!{veclen(\x1,\y1)*\pv{ratio}*1pt}!270:(\tikztotarget)$) +.. (\tikztotarget)\tikztonodes}}, +settings/.code={\tikzset{yade/.cd,#1} +\def\pv##1{\pgfkeysvalueof{/tikz/yade/##1}}}, +yade/.cd,pos/.initial=0.35,ratio/.initial=0} + +\newcommand{\deuxcellule}[8]{% + \node[coordinate] (a) at (#3) {} ; % + \node[coordinate] (b) at (#4) {} ; % + \node[coordinate] (c) at (#5) {} ; % + \node[coordinate] (d) at (#6) {} ; % + \path let + \p1= ($(b) - (a)$) , % + \p2= ($(d) - (c)$), % + \n1={veclen(\x1,\y1)}, % + \n2={veclen(\x2,\y2)}, % + \p3=($(\x1/\n1,\y1/\n1)$),% + \p4=($(\x2/\n2,\y2/\n2)$),% + \n3={#1 * \n1},% + \p5=($(\n3 * \x3, \n3 * \y3)$),% + \n3={#2 * \n2},% + \p6=($(\n3 * \x4, \n3 * \y4)$) in% + (a) ++ (\p5) node[coordinate] (x) {} %% + (c) ++ (\p6) node[coordinate] (y) {} %% + ; + \draw[#7] (x) -| (y) ; % +} + +% Old macros, for compatibility +\newcommand{\twocellleft}[5][.4]{\twocell[#1]{#2}{#3}{#4}{#5}{}{cell=0,bend left}} +\newcommand{\twocellright}[5][.4]{\twocell[#1]{#2}{#3}{#4}{#5}{}{cell=0,bend right}} + +\DeclareDocumentCommand{\twocelll}{O{.4} o D(){0} > { \SplitArgument { 1 } { , } } D<>{0.5,0.5} m m o m m}{% +\deuxcellule{#1}{\IfNoValueTF{#2}{#1}{#2}}{#5}{#6}{\IfNoValueTF{#7}{#5}{#7}}{#8}{}{bend right={#3},celllr=#4,label={[left]{$\scriptstyle #9$}}}} +\DeclareDocumentCommand{\twocellbr}{O{.4} o D(){30} > { \SplitArgument { 1 } { , } } D<>{0.5,0.5} m m o m m}{% +\deuxcellule{#1}{\IfNoValueTF{#2}{#1}{#2}}{#5}{#6}{\IfNoValueTF{#7}{#5}{#7}}{#8}{}{bend right={#3},celllr=#4,label={[below right]{$\scriptstyle #9$}}}} +\DeclareDocumentCommand{\twocellr}{O{.4} o D(){0} > { \SplitArgument { 1 } { , } } D<>{0.5,0.5} m m o m m}{% +\deuxcellule{#1}{\IfNoValueTF{#2}{#1}{#2}}{#5}{#6}{\IfNoValueTF{#7}{#5}{#7}}{#8}{}{bend right={#3},celllr=#4,label={[right]{$\scriptstyle #9$}}}} +\DeclareDocumentCommand{\twocellb}{O{.4} o D(){0} > { \SplitArgument { 1 } { , } } D<>{0.5,0.5} m m o m m}{% +\deuxcellule{#1}{\IfNoValueTF{#2}{#1}{#2}}{#5}{#6}{\IfNoValueTF{#7}{#5}{#7}}{#8}{}{bend right={#3},celllr=#4,label={[below]{$\scriptstyle #9$}}}} +\DeclareDocumentCommand{\twocella}{O{.4} o D(){0} > { \SplitArgument { 1 } { , } } D<>{0.5,0.5} m m o m m}{% +\deuxcellule{#1}{\IfNoValueTF{#2}{#1}{#2}}{#5}{#6}{\IfNoValueTF{#7}{#5}{#7}}{#8}{}{bend right={#3},celllr=#4,label={[above]{$\scriptstyle #9$}}}} +\DeclareDocumentCommand{\twocellal}{O{.4} o D(){30} > { \SplitArgument { 1 } { , } } D<>{0.5,0.5} m m o m m}{% +\deuxcellule{#1}{\IfNoValueTF{#2}{#1}{#2}}{#5}{#6}{\IfNoValueTF{#7}{#5}{#7}}{#8}{}{bend right={#3},celllr=#4,label={[above left]{$\scriptstyle #9$}}}} +\DeclareDocumentCommand{\twocellar}{O{.4} o D(){30} > { \SplitArgument { 1 } { , } } D<>{0.5,0.5} m m o m m}{% +\deuxcellule{#1}{\IfNoValueTF{#2}{#1}{#2}}{#5}{#6}{\IfNoValueTF{#7}{#5}{#7}}{#8}{}{bend left={#3},celllr=#4,label={[above right]{$\scriptstyle #9$}}}} +\DeclareDocumentCommand{\twocellbl}{O{.4} o D(){30} > { \SplitArgument { 1 } { , } } D<>{0.5,0.5} m m o m m}{% +\deuxcellule{#1}{\IfNoValueTF{#2}{#1}{#2}}{#5}{#6}{\IfNoValueTF{#7}{#5}{#7}}{#8}{}{bend right={#3},celllr=#4,label={[below left]{$\scriptstyle #9$}}}} + +% Two cell bent right + +\def\twocellrb{% + \@ifnextchar[{\twocellrb@i}{\twocellrb@i[.4]}% +} +\def\twocellrb@i[#1]{% + \@ifnextchar[{\twocellrb@ii[#1]}{\twocellrb@ii[#1][#1]}% +} +\def\twocellrb@ii[#1][#2]{% + \deuxcellulerb{#1}{#2}% +} +\newcommand{\deuxcellulerb}[6]{\twocell[#1][#2]{#3}{#4}{#5}{}{cell=0,bend right,labeld={#6}}} + +\def\twocellra{% + \@ifnextchar[{\twocellra@i}{\twocellra@i[.4]}% +} +\def\twocellra@i[#1]{% + \@ifnextchar[{\twocellra@ii[#1]}{\twocellra@ii[#1][#1]}% +} +\def\twocellra@ii[#1][#2]{% + \deuxcellulera{#1}{#2}% +} +\newcommand{\deuxcellulera}[6]{\twocell[#1][#2]{#3}{#4}{#5}{}{cell=0,bend right,labelu={#6}}} + +\def\twocellral{% + \@ifnextchar[{\twocellral@i}{\twocellral@i[.4]}% +} +\def\twocellral@i[#1]{% + \@ifnextchar[{\twocellral@ii[#1]}{\twocellral@ii[#1][#1]}% +} +\def\twocellral@ii[#1][#2]{% + \deuxcelluleral{#1}{#2}% +} +\newcommand{\deuxcelluleral}[6]{\twocell[#1][#2]{#3}{#4}{#5}{}{cell=0,bend right,labelal={#6}}} + +\def\twocellro{% + \@ifnextchar[{\twocellro@i}{\twocellro@i[.4]}% +} +\def\twocellro@i[#1]{% + \@ifnextchar[{\twocellro@ii[#1]}{\twocellro@ii[#1][#1]}% +} +\def\twocellro@ii[#1][#2]{% + \deuxcellulero{#1}{#2}% +} +\newcommand{\deuxcellulero}[6]{\twocell[#1][#2]{#3}{#4}{#5}{}{cell=0,bend right,labelo={#6}}} + +\def\twocellrl{% + \@ifnextchar[{\twocellrl@i}{\twocellrl@i[.4]}% +} +\def\twocellrl@i[#1]{% + \@ifnextchar[{\twocellrl@ii[#1]}{\twocellrl@ii[#1][#1]}% +} +\def\twocellrl@ii[#1][#2]{% + \deuxcellulerl{#1}{#2}% +} +\newcommand{\deuxcellulerl}[6]{\twocell[#1][#2]{#3}{#4}{#5}{}{cell=0,bend right,labell={#6}}} + +\def\twocellrr{% + \@ifnextchar[{\twocellrr@i}{\twocellrr@i[.4]}% +} +\def\twocellrr@i[#1]{% + \@ifnextchar[{\twocellrr@ii[#1]}{\twocellrr@ii[#1][#1]}% +} +\def\twocellrr@ii[#1][#2]{% + \deuxcellulerr{#1}{#2}% +} +\newcommand{\deuxcellulerr}[6]{\twocell[#1][#2]{#3}{#4}{#5}{}{cell=0,bend right,labelr={#6}}} + +\def\twocellrbr{% + \@ifnextchar[{\twocellrbr@i}{\twocellrbr@i[.4]}% +} +\def\twocellrbr@i[#1]{% + \@ifnextchar[{\twocellrbr@ii[#1]}{\twocellrbr@ii[#1][#1]}% +} +\def\twocellrbr@ii[#1][#2]{% + \deuxcellulerbr{#1}{#2}% +} +\newcommand{\deuxcellulerbr}[6]{\twocell[#1][#2]{#3}{#4}{#5}{}{cell=0,bend right,labelbr={#6}}} + +% Two cell bent left + +\def\twocelllb{% + \@ifnextchar[{\twocelllb@i}{\twocelllb@i[.4]}% +} +\def\twocelllb@i[#1]{% + \@ifnextchar[{\twocelllb@ii[#1]}{\twocelllb@ii[#1][#1]}% +} +\def\twocelllb@ii[#1][#2]{% + \deuxcellulelb{#1}{#2}% +} +\newcommand{\deuxcellulelb}[6]{\twocell[#1][#2]{#3}{#4}{#5}{}{cell=0,bend left,labeld={#6}}} + +\def\twocellla{% + \@ifnextchar[{\twocellla@i}{\twocellla@i[.4]}% +} +\def\twocellla@i[#1]{% + \@ifnextchar[{\twocellla@ii[#1]}{\twocellla@ii[#1][#1]}% +} +\def\twocellla@ii[#1][#2]{% + \deuxcellulela{#1}{#2}% +} +\newcommand{\deuxcellulela}[6]{\twocell[#1][#2]{#3}{#4}{#5}{}{cell=0,bend left,labelu={#6}}} + +\def\twocelllal{% + \@ifnextchar[{\twocelllal@i}{\twocelllal@i[.4]}% +} +\def\twocelllal@i[#1]{% + \@ifnextchar[{\twocelllal@ii[#1]}{\twocelllal@ii[#1][#1]}% +} +\def\twocelllal@ii[#1][#2]{% + \deuxcellulelal{#1}{#2}% +} +\newcommand{\deuxcellulelal}[6]{\twocell[#1][#2]{#3}{#4}{#5}{}{cell=0,bend left,labelal={#6}}} + +\def\twocelllo{% + \@ifnextchar[{\twocelllo@i}{\twocelllo@i[.4]}% +} +\def\twocelllo@i[#1]{% + \@ifnextchar[{\twocelllo@ii[#1]}{\twocelllo@ii[#1][#1]}% +} +\def\twocelllo@ii[#1][#2]{% + \deuxcellulelo{#1}{#2}% +} +\newcommand{\deuxcellulelo}[6]{\twocell[#1][#2]{#3}{#4}{#5}{}{cell=0,bend left,labelo={#6}}} + +\def\twocellll{% + \@ifnextchar[{\twocellll@i}{\twocellll@i[.4]}% +} +\def\twocellll@i[#1]{% + \@ifnextchar[{\twocellll@ii[#1]}{\twocellll@ii[#1][#1]}% +} +\def\twocellll@ii[#1][#2]{% + \deuxcellulell{#1}{#2}% +} +\newcommand{\deuxcellulell}[6]{\twocell[#1][#2]{#3}{#4}{#5}{}{cell=0,bend left,labell={#6}}} + +\def\twocelllr{% + \@ifnextchar[{\twocelllr@i}{\twocelllr@i[.4]}% +} +\def\twocelllr@i[#1]{% + \@ifnextchar[{\twocelllr@ii[#1]}{\twocelllr@ii[#1][#1]}% +} +\def\twocelllr@ii[#1][#2]{% + \deuxcellulelr{#1}{#2}% +} +\newcommand{\deuxcellulelr}[6]{\twocell[#1][#2]{#3}{#4}{#5}{}{cell=0,bend left,labelr={#6}}} + +\def\twocelllbr{% + \@ifnextchar[{\twocelllbr@i}{\twocelllbr@i[.4]}% +} +\def\twocelllbr@i[#1]{% + \@ifnextchar[{\twocelllbr@ii[#1]}{\twocelllbr@ii[#1][#1]}% +} +\def\twocelllbr@ii[#1][#2]{% + \deuxcellulelbr{#1}{#2}% +} +\newcommand{\deuxcellulelbr}[6]{\twocell[#1][#2]{#3}{#4}{#5}{}{cell=0,bend left,labelbr={#6}}} + + +\newbox\xrat@below +\newbox\xrat@above +\newcommand{\Xarrow}[3][]{% + \setbox\xrat@below=\hbox{\ensuremath{\scriptstyle #2}}% + \setbox\xrat@above=\hbox{\ensuremath{\scriptstyle #3}}% + \pgfmathsetlengthmacro{\xrat@len}{max(\wd\xrat@below,\wd\xrat@above)+.6em}% + \mathrel{\tikz [#1,baseline=-.75ex] + \draw (0,0) -- node[below=-2pt] {\box\xrat@below} + node[above=-2pt] {\box\xrat@above} + (\xrat@len,0) ;}} + +\newcommand{\xarrow}[2][]{% + \setbox\xrat@above=\hbox{\ensuremath{\scriptstyle #2\ }}% + \pgfmathsetlengthmacro{\xrat@len}{\wd\xrat@above+.8em}% + \mathrel{\tikz [baseline=-.75ex] + \draw (0,0) edge[#1] node[above=-2pt] {\box\xrat@above} + (\xrat@len,0) ;}} + + + + +\makeatother +\newenvironment{net}{\begin{tikzpicture}[baseline=(current bounding box.center),text depth=.2em,text height=.8em,inner sep=1pt]}{\end{tikzpicture}} + +\newcommand{\ssf}[2]{% +\inetatom(#1){#2}% +} + +\newcommand{\gimpll}{\ssf{Rien}{\impll}} +\newcommand{\gtens}{\ssf{Rien}{\tens}} +\newcommand{\gimpllof}[1]{\ssf{#1}{\impll}} +\newcommand{\gtensof}[1]{\ssf{#1}{\tens}} +\newcommand{\gun}[1]{\ssf{#1}{\un}} +\newcommand{\rpare}[1]{\node[text depth=.2em,text height=.8em,inner sep=0pt] (#1) {\ensuremath{)}};} +\newcommand{\lpare}[1]{\node[text depth=.2em,text height=.8em,inner sep=0pt] (#1) {\ensuremath{(}};} +\newcommand{\point}[1]{\node[right=0cm of #1] {.} ; } +\newcommand{\virgule}[1]{\node[right=0cm of #1] {,} ; } +\newcommand{\poing}{\ssf{}{.}} +\newcommand{\rieng}{\ssf{}{\,}} + + + +\pgfdeclaredecoration{single line}{initial}{ + \state{initial}[width=\pgfdecoratedpathlength-1sp]{\pgfpathmoveto{\pgfpointorigin}} + \state{final}{\pgfpathlineto{\pgfpointorigin}} +} + +\pgfdeclaredecoration{single line backwards}{initial}{ + \state{initial}[width=\pgfdecoratedpathlength-1sp]{\pgfpathmoveto{\pgfpointorigin}} + \state{final}{\pgfpathlineto{\pgfpointorigin}} +} + +\tikzset{ + raise line/.style={ + decoration={single line, raise=#1}, decorate + } +} + +\tikzset{ +mod/.style={postaction={ +decorate, +decoration={ +markings, +mark=at position .5 with { +\path[draw,-] (0,-3pt) -- (0,3pt); +}}}}} + +\tikzset{ +label/.style={postaction={ +decorate, +decoration={ +markings, +mark=at position .5 with {\node[inner sep=2pt,outer sep=0] #1 ;} +}}}} + +\tikzset{ +labelo/.style={postaction={ +decorate, +decoration={ +markings, +mark=at position .5 with {\node[circle,inner sep=0pt,fill=white] {$\scriptstyle #1$} ;} +}}}} + +\tikzset{ +labelon/.style={postaction={ +decorate, +decoration={ +markings, +mark=at position .5 with {\node[inner sep=1pt,fill=white] {$\scriptstyle #1$} ;} +}}}} + +\tikzset{ +labelonb/.style={postaction={ +decorate, +decoration={ +markings, +mark=at position .5 with {\node[inner sep=0pt,fill={bg}] {$\scriptstyle #1$} ;} +}}}} + +\tikzset{ +labelat/.style 2 args={postaction={ +decorate, +decoration={ +markings, +mark=at position #2 with {\node[inner sep=2pt] #1 ;} +}}}} + +\tikzset{ +labeloat/.style 2 args={postaction={ +decorate, +decoration={ +markings, +mark=at position #2 with {\node[inner sep=0.1pt,fill=white] {$\scriptstyle #1$} ;} +}}}} + +\tikzset{ +labelonat/.style 2 args={postaction={ +decorate, +decoration={ +markings, +mark=at position #2 with {\node[inner sep=0.1pt,fill=white] {$\scriptstyle #1$} ;} +}}}} + + + + +\tikzset{diagnode/.style={anchor=base,inner sep=5pt,outer sep=0pt}} +\tikzset{diag/.style 2 args=% + { +matrix of math nodes,ampersand replacement=\&, % +text height=1.2ex, text depth=0.25ex, % +row sep={#1 cm,between borders}, % +column sep={#2 cm,between borders}} +}% +\tikzset{diagorigins/.style 2 args=% +{matrix of math nodes,ampersand replacement=\&, % +row sep={#1 cm,between origins}, % +column sep={#2 cm,between origins}} +}% +\tikzset{stringdiag/.style 2 args=% +{nodes={inner sep=1pt,outer sep=0pt},% + ampersand replacement=\&,% + row sep={#1 cm,between origins}, % + column sep={#2 cm,between origins}% +}}% +\newcommand{\diaggrandhauteur}{1} +\newcommand{\diaggrandlargeur}{2} +\newcommand{\diagpetithauteur}{.5} +\newcommand{\diagpetitlargeur}{1.5} + +\tikzset{organigram/.style 2 args={matrix of nodes,ampersand replacement=\&, % +text height=1.7ex, text depth=0.25ex, % +row sep={#1 cm,between origins}, % +column sep={#2 cm,between origins} }} + +\tikzset{graphe/.style 2 args={matrix of math nodes,ampersand replacement=\&, % + row sep={#1 cm,between origins}, % + column sep={#2 cm,between origins}, % + inner sep=-.1ex}} % + +\tikzset{ +two/.style 2 args={postaction={ +decorate, +decoration={ +markings, +mark=at position .5 with \node (#1) [#2] {} ; +}}}} + +\tikzset{ +twocenter/.style={postaction={ +decorate, +decoration={ +markings, +mark=at position .5 with \node (#1) {} ; +}}}} + +\tikzset{ +twoon/.style 2 args={twocenter={#1},label={{$\scriptstyle #2$}}} +} +\tikzset{ +twoo/.style={two={on},label={{$\scriptstyle #1$}}} +} +\tikzset{ +twol/.style={two={l}{right},label={[left]{$\scriptstyle #1$}}} +} +\tikzset{ +twoleft/.style 2 args={two={#1}{right},label={[left]{$\scriptstyle #2$}}} +} +\tikzset{ +twor/.style={two={r}{left},label={[right]{$\scriptstyle #1$}}} +} +\tikzset{ +tworight/.style 2 args={two={#1}{left},label={[right]{$\scriptstyle #2$}}} +} +\tikzset{ +twou/.style={two={u}{below},label={[above]{$\scriptstyle #1$}}} +} +\tikzset{ +twoa/.style={two={a}{below},label={[above]{$\scriptstyle #1$}}} +} +\tikzset{ +twoup/.style 2 args={two={#1}{below},label={[above]{$\scriptstyle #2$}}} +} +\tikzset{ +twoabove/.style 2 args={two={#1}{below},label={[above]{$\scriptstyle #2$}}} +} +\tikzset{ +twod/.style={two={d}{above},label={[below]{$\scriptstyle #1$}}} +} +\tikzset{ +twob/.style={two={b}{above},label={[below]{$\scriptstyle #1$}}} +} +\tikzset{ +twodown/.style 2 args={two={#1}{above},label={[below]{$\scriptstyle #2$}}} +} +\tikzset{ +twobelow/.style 2 args={two={#1}{above},label={[below]{$\scriptstyle #2$}}} +} +\tikzset{ +twoal/.style={two={al}{right},label={[above left]{$\scriptstyle #1$}}} +} +\tikzset{ +twoaboveleft/.style 2 args={two={#1}{above},label={[above left]{$\scriptstyle #2$}}} +} +\tikzset{ +twoar/.style={two={ar}{left},label={[above right]{$\scriptstyle #1$}}} +} +\tikzset{ +twoaboveright/.style 2 args={two={#1}{above},label={[above right]{$\scriptstyle #2$}}} +} +\tikzset{ +twobr/.style={two={br}{left},label={[below right]{$\scriptstyle #1$}}} +} +\tikzset{ +twobelowright/.style 2 args={two={#1}{left},label={[below right]{$\scriptstyle #2$}}} +} +\tikzset{ +twobl/.style={two={bl}{right},label={[below left]{$\scriptstyle #1$}}} +} +\tikzset{ +twobelowleft/.style 2 args={two={#1}{right},label={[below left]{$\scriptstyle #2$}}} +} +\tikzset{ +twol/.style={two={l}{right},label={[left]{$\scriptstyle #1$}}} +} + +\tikzset{ +labell/.style={label={[left]{$\scriptstyle #1$}}} +} +\tikzset{ +labellat/.style 2 args={labelat={[left]{$\scriptstyle #1$}}{#2}} +} +\tikzset{ +labelr/.style={label={[right]{$\scriptstyle #1$}}} +} +\tikzset{ +labelrat/.style 2 args={labelat={[right]{$\scriptstyle #1$}}{#2}} +} +\tikzset{ +labelar/.style={label={[above right]{$\scriptstyle #1$}}} +} +\tikzset{ +labelarat/.style 2 args={labelat={[above right]{$\scriptstyle #1$}}{#2}} +} +\tikzset{ +labelbr/.style={label={[below right]{$\scriptstyle #1$}}} +} +\tikzset{ +labelbrat/.style 2 args={labelat={[below right]{$\scriptstyle #1$}}{#2}} +} +\tikzset{ +labelu/.style={label={[above]{$\scriptstyle #1$}}} +} +\tikzset{ +labeluat/.style 2 args={labelat={[above]{$\scriptstyle #1$}}{#2}} +} +\tikzset{ + labela/.style={label={[above]{$\scriptstyle #1$}}} +} +\tikzset{ +labelaat/.style 2 args={labelat={[above]{$\scriptstyle #1$}}{#2}} +} +\tikzset{ + loina/.style={label={[above=.5em]{$\scriptstyle #1$}}} +} +\tikzset{ +labeld/.style={label={[below]{$\scriptstyle #1$}}} +} +\tikzset{ +labelb/.style={label={[below]{$\scriptstyle #1$}}} +} +\tikzset{ +labelbat/.style 2 args={labelat={[below]{$\scriptstyle #1$}}{#2}} +} +\tikzset{ +loinb/.style={label={[below=.5em]{$\scriptstyle #1$}}} +} +\tikzset{ +labelal/.style={label={[above left]{$\scriptstyle #1$}}} +} +\tikzset{ +labelalat/.style 2 args={labelat={[above left]{$\scriptstyle #1$}}{#2}} +} +\tikzset{ +labelbl/.style={label={[below left]{$\scriptstyle #1$}}} +} +\tikzset{ +labelblat/.style 2 args={labelat={[below left]{$\scriptstyle #1$}}{#2}} +} +\tikzset{ +labellat/.style 2 args={labelat={[left]{$\scriptstyle #1$}}{#2}} +} + +\newcommand{\cs}[2][draw,->]{ % + \path[#1] (#2-1-1) -- (#2-1-2) ; % + \path[#1] (#2-1-3) -- (#2-1-2) ; % +} + +\newcommand{\cospan}{\cs{m}} + +\newcommand{\vdoublecs}[2][draw,->]{ + \foreach \i in {1,2,3} % + {% + \path[#1] (#2-1-\i) -- (#2-2-\i) ;% + \path[#1] (#2-3-\i) -- (#2-2-\i) ; % + } ; % +} + +\newcommand{\hdoublecs}[2][draw,->]{ + \foreach \i in {1,2,3} % + {% + \path[#1] (#2-\i-1) -- (#2-\i-2) ;% + \path[#1] (#2-\i-3) -- (#2-\i-2) ; % + } ; % +} + +\newcommand{\vdoubleisos}[1]{ + \foreach \i in {1,2,3} % + {% + \isopath{#1-1-\i}{#1-2-\i} % + \isopath{#1-2-\i}{#1-3-\i} % + } ; % +} + +\newcommand{\hdoubleisos}[1]{ + \foreach \i in {1,2,3} % + {% + \isopath{#1-\i-1}{#1-\i-2} % + \isopath{#1-\i-2}{#1-\i-3} % + } ; % +} + +\newcommand{\doublecs}[2][draw,->]{% + \vdoublecs[#1]{#2} % + \hdoublecs[#1]{#2} % +} + +\newcommand{\doublecospan}{\doublecs{m}} + +\newcommand{\sq}[4]{% + (m-1-1) edge[twou={#1}] (m-1-2) % + (m-1-1) edge[twol={#2}] (m-2-1) % + (m-1-2) edge[twor={#3}] (m-2-2) % + (m-2-1) edge[twod={#4}] (m-2-2) % +} + +\newcommand{\sqpath}[6]{ + \draw[->,#6,rounded corners] + (#1) -- +(#2:#3ex) -- node(#4) {} ($(#5) + (#2:#3ex)$) -- (#5) % + ; % + } + +\newcommand{\celltoangle}[5]{ + \path[draw] ($(#1)+(#2:#3ex)$) edge[celllr={0}{0},#5] ($(#1)+(#2:#4ex)$) ; % +} + +\newcommand{\pbkdefault}{1.4em} +\newcommand{\pbkmargin}{1pt} +\DeclareDocumentCommand{\pullbackk}{O{\pbkdefault} O{\pbkdefault} D(){2pt} m m m m}{% + \node[coordinate] (a) at (#4) {} ; % + \node[coordinate] (b) at (#5) {} ; % + \node[coordinate] (c) at (#6) {} ; % + \node[coordinate] (a') at ($(b)!#1!(a)$) {} ; % + \node[coordinate] (c') at ($(b)!#2!(c)$) {} ; % + \node[coordinate] (d) at (barycentric cs:a'=1,c'=1,b=-1) {} ; % + \node[coordinate] (aup) at ($(a')!#3!(d)$) {}; + \node[coordinate] (cup) at ($(c')!#3!(d)$) {}; + \path[#7] (aup) -- (d) -- (cup) ; % +} +\newcommand{\pullback}[5][\pbkdefault]{\pullbackk[#1][#1]{#2}{#3}{#4}{#5}} + +\newcommand{\pbk}[4][\pbkdefault]{% + \pullbackk[#1][#1]{#2}{#3}{#4}{draw,-} } +\newcommand{\stdpbk}{\pbk{m-2-1}{m-1-1}{m-1-2}} +\newcommand{\stdpo}{\pbk{m-2-1}{m-2-2}{m-1-2}} + +\newcommand{\onepbk}[4][\pbkdefault]{% + \pullback[#1]{#2}{#3}{#4}{draw,densely dotted} } +\newcommand{\ptwpbk}[4][\pbkdefault]{% + \pullback[#1]{#2}{#3}{#4}{draw,densely dotted} } + +\newcommand{\wpbk}[4][\pbkdefault]{% + \pullback[#1]{#2}{#3}{#4}{draw,dashed} } + +\newcommand{\pbkk}[4][\pbkdefault]{% + \pullback[#1]{#2}{#3}{#4}{cell=0} } + +\newcommand{\laxpbk}[4][\pbkdefault]{% + \pullback[#1]{#2}{#3}{#4}{draw,->,cell=0} } +\newcommand{\oplaxpbk}[4][\pbkdefault]{% + \pullback[#1]{#2}{#3}{#4}{draw,<-,cell=0} } + +\newcommand{\poleftg}[4][\pbkdefault]{% + \pullback[#1]{#2}{#3}{#4}{draw,open triangle 45-} } +\newcommand{\porightg}[4][\pbkdefault]{% + \pullback[#1]{#2}{#3}{#4}{draw,open triangle 45 reversed-} } + +\newcommand{\dpbk}[4][\pbkdefault]{% + \pullback[#1]{#2}{#3}{#4}{draw,-open triangle 45} } +\newcommand{\dpbkrev}[4][\pbkdefault]{% + \pullback[#1]{#2}{#3}{#4}{draw,-open triangle 45 reversed} } +\newcommand{\dpbkblack}[4][\pbkdefault]{% + \pullback[#1]{#2}{#3}{#4}{draw,-triangle 45} } +\newcommand{\dpbkblackrev}[4][\pbkdefault]{% + \pullback[#1]{#2}{#3}{#4}{draw,triangle 45-open triangle 45} } + + + + +\tikzset{shortenlr/.style 2 args={shorten <={#1 ex},shorten >={#2 ex}}} +\tikzset{ +back/.style={densely dotted} +} +\tikzset{ +fore/.style 2 args={preaction={draw={white},-,line width=4pt,shorten <=#1cm,shorten >=#2cm}}, +fore/.default={0.2}{0.2} +} +\tikzset{ +foretwo/.style={preaction={draw=white,-,line width=6pt}} +} + +\tikzset{twocell/.style = {double equal sign distance,double,-implies,shorten <= .15cm,shorten >=.15cm,draw}} +\tikzset{ +cell/.style = {double equal sign distance,double,-implies,shorten <= #1 cm,shorten >=#1 cm,draw} +} +\tikzset{celllr/.style 2 args = {double equal sign distance,double,-implies,shorten <= #1 ex,shorten >=#2 ex,draw}} +\tikzset{identity/.style = {double equal sign distance,double,-,draw}} +\tikzset{iso/.style = {label={[below=0em,sloped]{$\scriptstyle -$}},label={[above=-.2em,sloped]{$\scriptstyle \sim$}}}} +\tikzset{equi/.style = {label={[above=-.2em,sloped]{$\scriptstyle \sim$}}}} +\tikzset{isotwo/.style = postaction={ + decorate, + decoration={ + markings, + mark=at position .5 with {\node[inner sep=2pt,outer sep=0,above=-.2em,sloped] {$\scriptstyle \sim$} ;} + }}} +\tikzset{isor/.style = {labelr={\iso}}} +\tikzset{isol/.style = {labell={\iso}}} +\tikzset{isod/.style = {labeld={\iso}}} +\tikzset{isobr/.style = {labelbr={\iso}}} +\tikzset{baseline= (current bounding box.center)} +\tikzset{foreground/.style = {draw=white,very thick,double=black}} +\tikzset{background/.style = {draw=white,-,line width=3pt}} +\tikzset{diagram/.style = {column sep=1.5cm,row sep=1cm,nodes={minimum width=1cm}}} +\tikzset{nuage/.style = {cloud,draw,minimum width=2cm,minimum height=.6cm,cloud puffs=30,anchor=center}} +\tikzset{into/.style = {right hook->}} +\tikzset{otni/.style = {<-left hook}} +\tikzset{linto/.style = {left hook->}} +\tikzset{leadsto/.style = {->,decorate,decoration={snake,amplitude={#1 pt}}}} +\tikzset{leadsto/.default = {1.5}} +\tikzset{otsdael/.style = {<-,decorate,decoration={snake,amplitude=1.5pt}}} +\tikzset{onto/.style = {->>}} +\tikzset{mono/.style = {>->}} +\tikzset{fib/.style = {-latex}} +\tikzset{dfib/.style = {-Latex[open]}} +\tikzset{generic/.style = {-Triangle[]}} +\tikzset{free/.style = {-Triangle[open]}} +\tikzset{final/.style = {-]}} +\tikzset{epi/.style = {->>}} +\tikzset{adj/.style 2 args={text height={#1},text depth={#2}}} +\tikzset{adj/.default={.1cm}{0cm}} +\tikzset{iff/.style = {double equal sign distance,double,-implies,draw,shorten <= #1cm}} +\tikzset{ +mod/.style={postaction={ +decorate, +decoration={ +markings, +mark=at position .5 with {\draw[-] (0pt,-2pt) -- (0pt,2pt);} +}}}, +negate/.style={postaction={ +decorate, +decoration={ +markings, +mark=at position .5 with {\node[transform shape] (tempnode) {$/$};} +}}}, +mapsto/.style={|->}, +otspam/.style={<-|}, +pro/.style={postaction={ +decorate, +decoration={ +markings, +mark=at position #1 with {\draw[-,fill] (0pt,0pt) circle (1.5pt);} +}}}, +pro/.default={.5}, +glob/.style={postaction={ +decorate, +decoration={ +markings, +mark=at position .5 with {\draw[-,fill=white] (0pt,0pt) circle (1.5pt);} +}}} +} + +\newcommand{\idto}{\mathbin{\tikz[baseline] \draw[identity] (0pt,.5ex) -- (3ex,.5ex);}} +\newcommand{\idot}{\mathbin{\tikz[baseline] \draw[identity] (3ex,.5ex) -- (0pt,.5ex);}} +\newcommand{\fibto}[1]{\mathbin{\tikz[baseline] \draw (0pt,.5ex) edge[fib,labelu={\scriptstyle #1}] (3ex,.5ex);}} +\newcommand{\fibot}[1]{\mathbin{\tikz[baseline] \draw (3ex,.5ex) edge[fib,labelu={\scriptstyle #1}] (0pt,.5ex);}} +\newcommand{\dfibto}{ + \mathbin{\tikz[baseline] \draw (0pt,.5ex) edge[dfib] (3ex,.5ex);}} +\newcommand{\xdfibto}[1]{ + \mathbin{\tikz[baseline] \draw (0pt,.5ex) edge[dfib,labelu={\scriptstyle #1}] (3ex,.5ex);}} +\newcommand{\shortdfibto}{ + \mathbin{\tikz[baseline] \draw (0pt,.5ex) edge[dfib] (1.5ex,.5ex);}} +\newcommand{\shortdfibot}{ + \mathbin{\tikz[baseline] \draw (1.5ex,.5ex) edge[dfib] (0,.5ex);}} +\newcommand{\xxto}[2]{\mathbin{\tikz[baseline] \draw (0pt,.5ex) edge[->,labelu={\scriptstyle #1},labelb={\scriptstyle #2}] (3ex,.5ex);}} + +\newcommand{\dfibot}[1][]{ + \mathbin{\tikz[baseline] \draw (3ex,.5ex) edge[dfib,labelu={\scriptstyle #1}] (0pt,.5ex);}} +\newcommand{\modto}{\mathbin{\tikz[baseline] \draw[->,mod] (0pt,.5ex) -- (3ex,.5ex);}} +\newcommand{\proto}{\mathbin{\tikz[baseline] \draw[->,pro] (0pt,.5ex) -- (3ex,.5ex);}} +\newcommand{\shortproto}{\mathbin{\tikz[baseline] \draw[->,pro] (0pt,.5ex) -- (1.5ex,.5ex);}} +\newcommand{\finalto}{\mathbin{\tikz[baseline] \draw (0pt,.5ex) edge[final] (3ex,.5ex);}} +\newcommand{\xfinalto}[1]{\mathbin{\tikz[baseline] \draw (0pt,.5ex) edge[final,labelu={\scriptstyle #1}] (3ex,.5ex);}} +\newcommand{\finalot}{\mathbin{\tikz[baseline] \draw (3ex,.5ex) edge[final] (0pt,.5ex);}} +\newcommand{\xfinalot}[1]{\mathbin{\tikz[baseline] \draw (3ex,.5ex) edge[final,labelu={\scriptstyle #1}] (0pt,.5ex);}} +\newcommand{\shortinto}{\mathbin{\tikz[baseline] \draw[->,into] (0pt,.5ex) -- (2ex,.5ex);}} + + + +\newcommand{\cellule}[3][]{ % + \path (#3) +(#2:-.4cm) [twocell,#1] -- +(#2:.4cm) ; % +} + +\newcommand{\celluled}[2]{ % + \cellule[labell={#2}]{-90}{#1} % +} +\newcommand{\celluler}[2]{ % + \cellule[labelu={#2}]{0}{#1} % +} + +\newcommand{\isopath}[2]{% + \path % + (#1) -- node[sloped] {$\iso$} (#2) ; % +} + +\newcommand{\adjtemplate}[6][1]{% + \begin{tikzpicture}[baseline=(m-1-1.base)] % + \matrix (m) [diag={1}{#1}, + column sep={#1 cm,between borders}]{ % + |[adj]| #2 % + \& #6 % + \& |[adj]| #3 \\ + } ; % + \path[->] % + (m-1-1.north east) edge[labelu={#4},bend left=15] (m-1-3.north west) % + (m-1-3.base west) edge[labeld={#5},bend left=15] (m-1-1.base east) % + ; % + \end{tikzpicture} % +} + +\newcommand{\adj}[5][1]{\adjtemplate[#1]{#2}{#3}{#4}{#5}{\bot}} +\newcommand{\coadj}[5][1]{\adjtemplate[#1]{#2}{#3}{#4}{#5}{\top}} +\newcommand{\catequi}[5][1]{\adjtemplate[#1]{#2}{#3}{#4}{#5}{\simeq}} +\newcommand{\catiso}[5][1]{\adjtemplate[#1]{#2}{#3}{#4}{#5}{\cong}} + +\newcommand{\adjunction}[4]{% + \path[->] % + (#1) edge[twou={#3},bend left=15] (#2) % + (#2) edge[twod={#4},bend left=15] (#1) % + ; % + \path (u) -- node[pos=.5,sloped] {$\dashv$} (d) ; % + } + +\newcommand{\ladjunction}[4]{% + \path[->] % + (#1) edge[twou={#3},bend left=15] (#2) % + (#2) edge[twod={#4},bend left=15] (#1) % + ; % + \path (u) -- node[pos=.5,sloped] {$\vdash$} (d) ; % + } + +\newcommand{\adjs}[8][1]{% + \begin{tikzpicture} % + \matrix (m) [diag={1}{#1},column sep={#1 cm,between borders}]{ % + |[adj]| #2 % + \& \bot % + \& |[adj]| #3 + \& \bot % + \& |[adj]| #6 \\ + } ; % + \path[->] % + (m-1-1.north east) edge[labelu={#4},bend left=15] (m-1-3.north west) % + (m-1-3.south west) edge[labeld={#5},bend left=15] (m-1-1.south east) % + (m-1-3.north east) edge[labelu={#7},bend left=15] (m-1-5.north west) % + (m-1-5.south west) edge[labeld={#8},bend left=15] (m-1-3.south east) % + ; % + \end{tikzpicture} % +} +\newcommand{\coadjs}[8][1]{% + \begin{tikzpicture} % + \matrix (m) [diag={1}{#1},column sep={#1 cm,between borders}]{ % + |[adj]| #2 % + \& \top % + \& |[adj]| #3 + \& \top % + \& |[adj]| #6 \\ + } ; % + \path[->] % + (m-1-1.north east) edge[labelu={#4},bend left=15] (m-1-3.north west) % + (m-1-3.south west) edge[labeld={#5},bend left=15] (m-1-1.south east) % + (m-1-3.north east) edge[labelu={#7},bend left=15] (m-1-5.north west) % + (m-1-5.south west) edge[labeld={#8},bend left=15] (m-1-3.south east) % + ; % + \end{tikzpicture} % +} + +\newcommand{\retr}[5][1]{% + \begin{tikzpicture} % + \matrix (m) [diag={1}{#1},column sep={#1 cm,between borders}]{ % + |[anchor=east,text height=.1cm,text depth=-.1cm]| #2 % + \& |[anchor=center]| \triangleleft % + \& |[anchor=west,text height=.1cm,text depth=-.1cm]| #3 \\ + } ; % + \path[->] % + (m-1-1.north east) edge[labelu={#4},bend left=15] (m-1-3.north west) % + (m-1-3.south west) edge[labeld={#5},bend left=15] (m-1-1.south east) % + ; % + \end{tikzpicture} % +} + +\newcommand{\doublecell}[9]{ + \diag{% + |(X)| {#1} \& |(Y)| {#2} \\ % + |(U)| {#3} \& |(V)| {#4} % + }{% + (X) edge[labelu={#5}] (Y) % + edge[pro,twol={#6}] (U) % + (Y) edge[pro,twor={#7}] (V) % + (U) edge[labeld={#8}] (V) % + (l) edge[cell=.4,labelu={\scriptstyle #9}] (r) % + } +} + +\newcommand{\doublecellpro}[9]{ + \diag{% + |(X)| {#1} \& |(Y)| {#2} \\ % + |(U)| {#3} \& |(V)| {#4} % + }{% + (X) edge[labelu={#5}] (Y) % + edge[pro,twol={#6}] (U) % + (Y) edge[pro,twor={#7}] (V) % + (U) edge[labeld={#8}] (V) % + (l) edge[cell=.4,labelu={\scriptstyle #9}] (r) % + } +} + +\newcommand{\vdoublecell}[9]{ + \diag{% + |(X)| {#1} \& |(Y)| {#2} \\ % + |(U)| {#3} \& |(V)| {#4} % + }{% + (X) edge[twou={#5}] (Y) % + edge[labell={#6}] (U) % + (Y) edge[labelr={#7}] (V) % + (U) edge[twod={#8}] (V) % + (u) edge[cell=.4,labelr={\scriptstyle #9}] (d) % + } +} + +\newcommand{\Vdots}{|[anchor=center,text height=.1cm]| \vdots} + +\newcommand{\relate}[3]{\path (#1) -- node[anchor=mid] {$#2$} (#3) ;} +\newcommand{\justify}[4][0.5]{\path (#2) -- node[anchor=mid,pos=#1] {\tiny (#3)} (#4) ;} + + + +\newcommand{\mkdots}[2]{ \path + (#1) -- + node[pos=.4] {.} + node[pos=.5] {.} + node[pos=.6] {.} + (#2) + ;} + +\newcommand{\mkdotsshrink}[2]{ \path + (#1) -- + node[pos=.3] {.} + node[pos=.5] {.} + node[pos=.7] {.} + (#2) + ;} + +\endinput