Mysaa/M2Internship
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Adapt the construction of the adjunction

Browse Source
This commit is contained in:
Samy Avrillon 2024-07-18 03:46:43 +02:00
parent b27dcbd2ca
commit e9da8a9107
Signed by: Mysaa
GPG Key ID: 0220AC4A3D6A328B
9 changed files with 69 additions and 51 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

107
Report/M2Report.tex
View File

@ -234,49 +234,41 @@
\end{remark}
\subsection{Constructing the adjunction}
We will now construct the adjunction $F_i \vdash G_i$ at the step $i$.
\subsection{Some Hypotheses}
\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$.
In order to build and prove the adjunction, we will state some recurrence invariants that we will prove after having built objects.
\begin{property}[H1]
\[
\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}
is an isomorphism.
\begin{property}[H1r]
Its recursive version is the following isomorphism
\[
\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)}
\simpleArrow{ R_{0}^i X \oplus_0 Y}{\left\{R_0^i \inj_1^i ; R_0^i \inj_2^i \circ \eta_0^i\right\}}{R_0^i(X \oplus_i L_0^i Y)}
\]
is an equivalence.
This property is proven easily by recursion over previous property H1.
\end{property}
\begin{property}[H3]
\[
\simpleArrow{F_i X}{F(\inj_1^i)}{F_i(X \oplus L_0^i Y)}
\]
is an equivalence.
is an isomorphism.
We will often this equality along with the $F_i \vdash G_i$ adjunction (for an object $O$ in $\CC_i$)
\[
\Hom(G_i O, X) \cong \Hom(O, F_i X) \cong \Hom(O, F_i(X \oplus L_0^i Y)) \cong \Hom(G_i O, X \oplus L_0^i Y)
\]
This new isomorphism is the following:
\[
\simpleArrow{\Hom(G_i O, X)}{(inj_1^i \circ \dash)}{\Hom(G_i O,X \oplus L_0^i Y)}
\]
\end{property}
\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}
\subsubsection{Decomposing the proof}
\subsection{Constructing the functors}
In order to use all the power of the recurrence, we will build the $F_i \vdash G_i$ adjunction using the $F_{i-1} \vdash G_{i-1}$ adjunction, following the diagram below.
@ -287,25 +279,30 @@
% 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.
The first part $G_{i-1} \times \id \dashv F_{i-1} \times \id$ is proven and defined as an adjunction from the previous step of the recurrence.
\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}$
We define a functor $W : \left(X : \BB_{i-1}\right) \times \Set/\Hom_{\BB_{i-1}}(G_{i-1}O_i,X) \to \BB_{i}$
The action on objects is as follows:
\[
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}O_i,\dash)}(X,Y), \widetilde{\inj_2} \right)
\]
With $\widetilde{\inj_2}$ being defined by
Where $\Hbar_A(X,Y)$ is a functor $(X:C) \times (\Set/A(X)) \to \TSet$ with
\[\begin{array}{c}
\Hbar_A(X,Y)_\UU = A(X)\\
\Hbar_A(X,Y)_\El = Y
\end{array}\]
\todo{Réference de comment on crée le foncteur, pourquoi c'en est un, si c'est utile ...}
With $\widetilde{\inj_2}$ being defined by \inlinetodo{Changer les noms des hypothèses H3' et H1r}
\[
\begin{array}{lcl}
\Hom(G_{i-1}\Gamma_i,X \oplus L_0^{i-1} \Hbar_\bullet(X,Y)) & \to^{\text{H3'}} & \Hom(G_{i-1}\Gamma_i,X)\\
\Hom(G_{i-1}O_i,X \oplus L_0^{i-1} \Hbar_\bullet(X,Y)) & \to^{\text{H3'}} & \Hom(G_{i-1}O_i,X)\\
& = & \Hbar_\bullet(X,Y)_\UU \\
& \to^{\inj_2^0} & \left(R_0^{i-1}X \oplus \Hbar_\bullet(X,Y)\right)_\UU \\
& \to^{\text{H1r}} & \left(R_0^{i-1}(X \oplus L_0^{i-1}\Hbar_\bullet(X,Y))\right)_\UU
@ -314,7 +311,7 @@
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}O_i,\dash)}(g,h)\right)
\]
It is indeed a morphism from $\BB_{i}$ as it makes the following diagram commute.
@ -328,8 +325,9 @@
\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))$
We define $E : \BB_{i} \to \left(X : \BB_{i-1}\right) \times (\Set/\Hom_{\BB_{i-1}}(G_{i-1}O_i,X))$
The action on objects is
\[
E(X) = (R_{i-1}^i X, (A,h))
\]
@ -352,11 +350,11 @@
\end{center}
\subsubsection{Proof of the adjunction}
\subsection{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}$.
We want to construct for each $(X,Y)$ in $\displaystyle\prod_{X : \BB_{i-1}} (\Set/\Hom_{\BB_{i-1}}(G_{i-1}O_i,X))$ and $Z$ in $\BB_i$, an isomorphism $\phi_{XYZ}$.
\[
\phi_{XYZ} : \Hom(W(X,Y),Z) \to \Hom((X,Y),E(Z))
@ -364,7 +362,7 @@
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}$}
\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)$.
@ -380,7 +378,7 @@
% END OF GENERATED LATEX
\end{center}
\paragraph{Constructing $\phi^{-1}_{XYZ}$}
\subsubsection{Constructing $\phi^{-1}_{XYZ}$}
Now, we take $(g,h)$ a morphism from $(X,Y)$ to $E(Z)$.
@ -389,7 +387,7 @@
\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:
Where $\square$ is a morphism $\Hbar (X,Y) \to R_0^i Z$ in $\TSet$ defined by the following diagram:
\begin{center}
% YADE DIAGRAM D7.json
@ -411,9 +409,15 @@
\subsection{$F \vdash G$ make a reflection}
\subsubsection{Properties of the adjunction}
We have proven that $F_i \vdash G_i$ make a reflection, i.e. that $F_iG_i \cong \Id_{\CC_i}$.
\subsection{Proof of H1 - Sum definition}
The proof is given in \autoref{apx:FG-refl}.
\subsection{Proof of the hypotheses}
\subsubsection{Proof of H1}
\todo{Relire + réeexpliquer pourquoi ça prouve}
We will define the sums of the form $X \oplus_i L_0^i Y$ in $\BB_i$.
@ -467,7 +471,7 @@
\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}
\subsubsection{Proof of H3}
\section{Misc}
@ -731,8 +735,21 @@
As the diagram commutes and by pullback property, we get the equality.
\section{$F_i \vdash G_i$ reflection}
\label{apx:FG-refl}
\todo{La preuve :/}
\end{document}

2
Report/graphs/D2.json
View File

File diff suppressed because one or more lines are too long

2
Report/graphs/D3a.json
View File

@ -1 +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}
{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":4,"label":{"kind":"normal","label":"h","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":0,"id":5,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":6,"label":{"kind":"normal","label":"R_0^i(X)_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":1,"id":7,"label":{"kind":"normal","label":"\\Cstr^X_i","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3}],"nodes":[{"id":0,"label":{"isMath":true,"label":"A","pos":[100,117.8125],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\Hom(G_{i-1}O_i,R_{i-1}^i X)","pos":[100,195.8125],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"R_0^i(X)_\\El","pos":[358,117.8125],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"R_0^i(X)_\\UU","pos":[358,195.8125],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12}

2
Report/graphs/D3b.json
View File

@ -1 +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}
{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":8,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":9,"label":{"kind":"normal","label":"R_0^i(X)_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":10,"label":{"kind":"normal","label":"h","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.30000000000000004,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":11,"label":{"kind":"normal","label":"\\Cstr^X_i","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":4,"id":12,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":5,"id":13,"label":{"kind":"normal","label":"R_0^i(X')_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":4,"id":14,"label":{"kind":"normal","label":"h'","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.30000000000000004,"tail":"none"},"zindex":0},"to":7},{"from":7,"id":15,"label":{"kind":"normal","label":"\\Cstr^{X'}_i","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":0,"id":16,"label":{"kind":"normal","label":"!","style":{"alignment":"left","bend":0,"color":"black","dashed":true,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":1},"to":4},{"from":1,"id":17,"label":{"kind":"normal","label":"R_0^i(f)_\\El","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":3,"id":18,"label":{"kind":"normal","label":"\\dash \\circ R_{i-1}^i f","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.10000000000000003,"tail":"none"},"zindex":0},"to":7},{"from":2,"id":19,"label":{"kind":"normal","label":"R_0^i(f)_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.6,"tail":"none"},"zindex":0},"to":6},{"from":14,"id":20,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":12},{"from":10,"id":21,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":8}],"nodes":[{"id":0,"label":{"isMath":true,"label":"A","pos":[125,115],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"R_0^i(X)_\\El","pos":[403,115],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"R_0^i(X)_\\UU","pos":[403,297],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\Hom(G_{i-1}O_i,R_{i-1}^i X)","pos":[125,297],"zindex":-10000}},{"id":4,"label":{"isMath":true,"label":"A'","pos":[249,190.8125],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"R_0^i(X')_\\El","pos":[521,190.8125],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"R_0^i(X')_\\UU","pos":[521,372.8125],"zindex":0}},{"id":7,"label":{"isMath":true,"label":"\\Hom(G_{i-1}O_i,R_{i-1}^i X')","pos":[249,372.8125],"zindex":-10000}}],"sizeGrid":250,"title":"1"}]},"version":12}

2
Report/graphs/D6.json
View File

@ -1 +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}
{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":6,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":7,"label":{"kind":"normal","label":"(R_0^i Z)_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":8,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":9,"label":{"kind":"normal","label":"\\Cstr^Z","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":4,"id":10,"label":{"kind":"normal","label":"h","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":5,"id":11,"label":{"kind":"normal","label":"\\dash \\circ R_{i-1}^i f \\circ \\inj_1","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.10000000000000003,"tail":"hook"},"zindex":8},"to":3},{"from":4,"id":12,"label":{"kind":"normal","label":"\\left[R_{i-1}^i f \\circ \\inj_2\\right]_\\El","style":{"alignment":"left","bend":-0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":4,"id":13,"label":{"kind":"normal","label":"\\phi_{XYZ}(f)_2","style":{"alignment":"left","bend":0,"color":"black","dashed":true,"head":"default","kind":"normal","position":0.6,"tail":"none"},"zindex":0},"to":0}],"nodes":[{"id":0,"label":{"isMath":true,"label":"E(z)","pos":[292,174],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"(R_0^i Z)_\\El","pos":[492,174],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[492,304],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\Hom(G_{i-1}O_i,R_{i-1}^i Z)","pos":[292,304],"zindex":-10000}},{"id":4,"label":{"isMath":true,"label":"A","pos":[100,100],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"\\Hom(G_{i-1}O_i,X)","pos":[101,224.8125],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12}

2
Report/graphs/D7.json
View File

@ -1 +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}
{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":6,"label":{"kind":"normal","label":"h","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":7,"label":{"kind":"normal","label":"\\pi_1","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":8,"label":{"kind":"normal","label":"(R_0^i Z)_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":1,"id":9,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":4,"id":10,"label":{"kind":"normal","label":"\\Cstr^Z","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":0,"id":11,"label":{"kind":"normal","label":"h","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":5,"id":12,"label":{"kind":"normal","label":"g \\circ \\dash","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":0,"id":13,"label":{"kind":"normal","label":"\\square_\\El","style":{"alignment":"left","bend":-0.2,"color":"blue","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":5,"id":14,"label":{"kind":"normal","label":"\\square_\\UU","style":{"alignment":"right","bend":0.10000000000000003,"color":"blue","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":9,"id":15,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":7}],"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":[608,130],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[608,234],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"\\Hom(G_{i-1}O_i,R_{i-1}^i Z)","pos":[390,234],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"\\Hom(G_{i-1}O_i,X)","pos":[130,234],"zindex":-10000}}],"sizeGrid":260,"title":"1"}]},"version":12}

2
Report/graphs/D8.json
View File

@ -1 +1 @@
{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":8,"label":{"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}
{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":8,"label":{"kind":"normal","label":"\\text{H3'}","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.30000000000000004,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":9,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":10,"label":{"kind":"normal","label":"\\inj_2^0","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":11,"label":{"kind":"normal","label":"\\text{H1r}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":4,"id":12,"label":{"kind":"normal","label":"R_0^{i-1}\\left\\{g;\\eta_0^i \\circ L_0^{i-1} \\square \\right\\}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":2,"id":13,"label":{"kind":"normal","label":"(\\varepsilon_0^{i-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":6,"id":14,"label":{"kind":"normal","label":"(R_0^{i-1} \\inj_2^{i-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":6,"id":15,"label":{"kind":"normal","label":"R_0^{i-1}(\\eta_0^i \\circ L_0^{i-1} \\square)_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.7,"tail":"none"},"zindex":0},"to":5},{"from":2,"id":16,"label":{"kind":"normal","label":"\\square_\\UU \\circ \\Cstr^Z \\circ (g \\circ \\dash)","style":{"alignment":"right","bend":0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.30000000000000004,"tail":"none"},"zindex":0},"to":5},{"from":0,"id":17,"label":{"kind":"normal","label":"\\left\\{g;\\eta_0^i \\circ L_0^{i-1} \\square \\right\\} \\circ \\dash","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":7,"id":18,"label":{"kind":"normal","label":"\\Cstr^Z","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":1,"id":19,"label":{"kind":"normal","label":"g \\circ \\dash","style":{"alignment":"left","bend":0,"color":"red","dashed":false,"head":"default","kind":"normal","position":0.4,"tail":"none"},"zindex":0},"to":7}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\Hom(G_{i-1}O_i,X \\oplus L_0^{i-1}\\Hbar(X,Y))","pos":[210,64],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\Hom(G_{i-1}O_i,X)","pos":[329,129.8125],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\Hbar(X,Y)_\\UU","pos":[410,64.8125],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\left[R_0^{i-1} X \\oplus \\Hbar(X,Y)\\right]_\\UU","pos":[604.9999999999999,61.8125],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"R_0^{i-1}\\left(X \\oplus L_0^{i-1}\\Hbar(X,Y)\\right)","pos":[853,61.8125],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[853,303.8125],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"\\left[R_0^{i-1}L_0^{i-1}\\Hbar(X,Y)\\right]_\\UU","pos":[688,198.625],"zindex":0}},{"id":7,"label":{"isMath":true,"label":"\\Hom(G_{i-1}O_i,R_{i-1}^i Z)","pos":[210,306],"zindex":0}}],"sizeGrid":140,"title":"1"}]},"version":12}

2
Report/graphs/G2.json
View File

@ -1 +1 @@
{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":7,"label":{"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}
{"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":4,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":5,"label":{"kind":"normal","label":"G_{i-1} \\times \\id","style":{"alignment":"right","bend":0.30000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":6,"label":{"kind":"normal","label":"F_{i-1} \\times \\id","style":{"alignment":"right","bend":0.30000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":2,"id":7,"label":{"kind":"normal","label":"W","style":{"alignment":"right","bend":0.30000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":8,"label":{"kind":"normal","label":"E","style":{"alignment":"right","bend":0.30000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":9,"label":{"kind":"normal","label":"G_i","style":{"alignment":"right","bend":0.6,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":10,"label":{"kind":"normal","label":"F_i","style":{"alignment":"right","bend":-0.4,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":6,"id":11,"label":{"kind":"adjunction","label":"\\vdash","style":{"alignment":"over","bend":0,"color":"black","dashed":false,"head":"none","kind":"none","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":8,"id":12,"label":{"kind":"adjunction","label":"\\vdash","style":{"alignment":"over","bend":0,"color":"black","dashed":false,"head":"none","kind":"none","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":10,"id":13,"label":{"kind":"adjunction","label":"\\vdash","style":{"alignment":"over","bend":0,"color":"black","dashed":false,"head":"none","kind":"none","position":0.5,"tail":"none"},"zindex":0},"to":9}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\CC_i","pos":[176,73.8125],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\left(X : \\CC_{i-1}\\right) \\times \\left.\\Set\\middle/\\Hom(O_i,X)\\right.","pos":[386,74],"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":[386,171.8125],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\BB_i","pos":[386,274],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12}

1
Report/header.tex
View File

@ -118,6 +118,7 @@
\DeclareMathOperator{\inj}{inj}
\DeclareMathOperator{\id}{id}
\DeclareMathOperator{\Id}{\mathcal{I}d}
\newcommand\TSet{{\ensuremath{\left[\TT,\Set\right]}}}
\newcommand\TSetObject[3]{{\ensuremath{