Une relecture de plus ne fait jamais de mal
This commit is contained in:
parent
c22581c3a0
commit
1bfa214cde
GPG Key ID:
0220AC4A3D6A328B
@ -28,7 +28,7 @@
|
||||
|
||||
\subsection*{General Context}
|
||||
|
||||
Generalized Algebraic Theories a.k.a. GATs are syntactic objects introduced in 1986 by Cartmell \cite{CartmellGATs}. They enable us to describe algebraic structures that we can see as a generalization of Type Theory's inductive types. For example, we can describe the models of some type theory using a GAT.
|
||||
Generalized Algebraic Theories a.k.a. GATs are syntactic objects introduced in 1986 by Cartmell \cite{CartmellGATs}. We can see them as a generalization of Type Theory's inductive types as they enable us to describe algebraic structures. For example, we can describe the models of first order logic using a GAT.
|
||||
|
||||
A GAT is made of a list of \enquote{sorts} called a \enquote{sort specification} that describes sets, usually followed by a list of \enquote{constructors}.
|
||||
|
||||
@ -121,9 +121,9 @@
|
||||
$\Con : \mathcal{O}$ & One sort object is called \enquote{$\Con$} \\
|
||||
$\Ty : (\Gamma : \underline{\Con}) \to \mathcal{O}$ &
|
||||
For each object $\Gamma$ corresponding to the sort object $\Con$, another sort object called \enquote{$\Ty\;\Gamma$} \\
|
||||
$\Tm : (\Gamma : \underline{\Con}) \to (A : \underline{\Ty\;\Delta}) \to \mathcal{O}$ &
|
||||
For each object $\Gamma$ corresponding to the sort object $\Con$,
|
||||
and for every object $A$ corresponding to the sort object $\Ty\;\Gamma$, another sort object called \enquote{$\Tm\;\Gamma\;A$}\\
|
||||
$\Tm : (\Delta : \underline{\Con}) \to (A : \underline{\Ty\;\Delta}) \to \mathcal{O}$ &
|
||||
For each object $\Delta$ corresponding to the sort object $\Con$,
|
||||
and for every object $A$ corresponding to the sort object $\Ty\;\Delta$, another sort object called \enquote{$\Tm\;\Delta\;A$}\\
|
||||
$\operatorname{unit} : (\Gamma : \underline{\Con}) \to \underline{\Ty\;\Gamma}$ &
|
||||
For each object $\Gamma$ corresponding to the sort object $\Con$, an object called "$\operatorname{unit} \Gamma$" corresponding to the sort object $\Ty\;\Gamma$\\
|
||||
$\operatorname{tt}: (\Gamma : \underline{\Con}) \to \underline{\Tm\;(\operatorname{unit}\;\Gamma)}$ &
|
||||
@ -243,7 +243,7 @@
|
||||
|
||||
\subsection{Type theory example}
|
||||
|
||||
We will take as a first example the sort specification of type theory presented in the introduction. The sort specification and its transformation are as follows:
|
||||
Our next example is the sort specification of type theory presented in the introduction. We recall that the sort specification and its transformation are as follows:
|
||||
|
||||
\vspace{1ex}
|
||||
\begin{center}
|
||||
@ -279,7 +279,7 @@
|
||||
|
||||
We have seen in the introduction a description of a model of the type theory sort specification. We will rebuild the category of those models inductively, adding one sort at a time.
|
||||
|
||||
To construct those categories generically, we will define functors $H_X : \CC_{X-1} \to \Set$ that will describe the \enquote{parameters} of the sort declaration.
|
||||
To construct those categories generically, we will define functors $H_i : \CC_{i-1} \to \Set$ that will describe the \enquote{parameters} of the sort declaration.
|
||||
|
||||
\[
|
||||
\boxed{\Con : \Set}
|
||||
@ -550,7 +550,7 @@
|
||||
\[
|
||||
R_0^i := R^1_0 \circ \dots \circ R_{i-1}^i
|
||||
\]
|
||||
\item An operator $\tl^i : \BB_i \times \BB_0 \to \BB_i$ along with two morphism $\inj_1^i : X \to X \tl^i Y$ and $\inj_2^i : Y \to R_0^i(X \tl^i Y)$ for every $X,Y$ in $\BB_i \times \BB_0$. This operation follows a specific universal property: For every morphism $g : X \to Z$ and $h : Y \to R_0^iZ$, there is a unique morphism $\{g;h\}$ such that the following two diagrams respectively in $\BB_i$ and $\BB_0$ commute:
|
||||
\item An operator $\tl^i : \BB_i \times \BB_0 \to \BB_i$ along with two morphisms $\inj_1^i : X \to X \tl^i Y$ and $\inj_2^i : Y \to R_0^i(X \tl^i Y)$ for every $X,Y$ in $\BB_i \times \BB_0$. This operation follows a specific universal property: For every morphism $g : X \to Z$ and $h : Y \to R_0^iZ$, there is a unique morphism $\{g;h\}$ such that the following two diagrams respectively in $\BB_i$ and $\BB_0$ commute:
|
||||
\label{sec:tlUniversalProperty}
|
||||
|
||||
\begin{center}
|
||||
@ -658,7 +658,7 @@
|
||||
\end{remark}
|
||||
|
||||
\subsection{Initialization}
|
||||
In this subsection, we will recall objects built in \autoref{sec:EmptySortSpec}, and build some other objects corresponding to the empty sort specification i.e. the first step of our induction.
|
||||
In this subsection, we will recall objects built in the example of \nameref{sec:EmptySortSpec}, and build some other objects corresponding to the empty sort specification i.e. the first step of our induction.
|
||||
|
||||
\begin{itemize}
|
||||
\setlength\itemsep{-1ex}
|
||||
@ -668,11 +668,11 @@
|
||||
\item $F_0 : \TSet \to \one$ is the terminal functor of $\Cat$
|
||||
\item $G_0 : \one \to \TSet$ is the functor that sends the only object of $\one$ to the initial object of $\TSet$: $0_\TSet$
|
||||
\item For $X$ an object of $\TSet$, we have
|
||||
\[\Hom(G_0 \star,X) = \Hom(0_\TSet,X) \cong \one \cong \Hom(\star,F_0 X)\]
|
||||
\[\Hom(G_0 \star,X) = \Hom(0_\TSet,X) \cong 1_\Set \cong \Hom(\star,F_0 X)\]
|
||||
(reminder: $\star$ is the only object of $\one$)
|
||||
Therefore, we have that $F_0 \vdash G_0$.
|
||||
\item $F_0G_0 : \one \to \one$ so $F_0G_0 = \Id_\one$ as $\one$ is terminal in $\Cat$
|
||||
\item $F_i\inj_1 = \id_\star$ which is an isomorphism
|
||||
\item $F_i\inj^0_1 = \id_\star$ which is an isomorphism
|
||||
\end{itemize}
|
||||
|
||||
|
||||
@ -865,7 +865,7 @@
|
||||
\]
|
||||
|
||||
\paragraph{Universal Property}
|
||||
We will now show that the universal property stated in \autoref{sec:tlUniversalProperty} holds.
|
||||
We will now show that the universal property stated in the introduction of this section holds.
|
||||
To that end, we take two objects $X$ and $Z$ in $\BB_i$, $Y$ in $\BB_0$, a morphism $g : X \to Z$ in $\BB_i$ and a morphism $h : Y \to R_0^iZ$ in $\BB_0$. We want to build a morphism $\{g,h\}$ of $\BB_i$ such that the following diagrams of $\BB_i$ and $\BB_0$ commute.
|
||||
|
||||
\begin{center}
|
||||
@ -883,29 +883,18 @@
|
||||
|
||||
\paragraph{Building morphisms}
|
||||
|
||||
For any two morphisms $g : X \to X'$ of $\BB_i$ and $h : Y \to Y'$ of $\BB_0$, we will create a morphism $X \tl^i Y \to X' \tl^i Y'$ as follows:
|
||||
For any two morphisms $g : X \to X'$ of $\BB_i$ and $h : Y \to Y'$ of $\BB_0$, we check that the morphism $R_{i-1}^ig \tl^{i-1} h$ verifies the morphism property of $\BB_i$ in Appendix \ref{apx:tlMorphismOfBi}, so that we can define a morphism $g\tl^ih : X \tl^i Y \to X' \tl^i Y'$ such that
|
||||
\[
|
||||
g\tl^ih := R_{i-1}^ig \tl^{i-1} h
|
||||
R_{i-1}^i\left(g\tl^ih\right) = \left(R_{i-1}^ig\right) \tl^{i-1} h
|
||||
\]
|
||||
|
||||
This is indeed a morphism of $\BB_i$ as it makes the following diagram commute:
|
||||
|
||||
\begin{center}
|
||||
\begin{scaletikzpicturetowidth}{.9\textwidth}
|
||||
% YADE DIAGRAM TlDefOnMorphisms.json
|
||||
% GENERATED LATEX
|
||||
\input{graphs/TlDefOnMorphisms.tex}
|
||||
% END OF GENERATED LATEX
|
||||
\end{scaletikzpicturetowidth}
|
||||
\end{center}
|
||||
|
||||
\paragraph{Composition with $F_i$}
|
||||
We finally need to prove, for any objects $X$ in $\BB_i$ and $Y$ in $\TSet$, that the morphism
|
||||
$F_i(\inj_1^i) : F_iX \to F_i(X \tl^i Y)$ is an isomorphism.
|
||||
|
||||
Morphisms $\BB_{i}$ are morphisms of $\BB_{i-1}$ that follow some equations, and composition is the same. Moreover, we know from the definition above that $R_{i-1^i} \inj_1^i := \inj_1^{i-1}$.
|
||||
Morphisms $\BB_{i}$ are morphisms of $\BB_{i-1}$ that follow some equations, and composition is the same. Moreover, we know from the definition above that $R_{i-1}^i \inj_1^i = \inj_1^{i-1}$.
|
||||
|
||||
So, we just need to know that $R_{i-1}^i(F_{i-1}\inj_1^i)$ is an isomorphism.
|
||||
So, we just need to prove that $R_{i-1}^i(F_{i-1}\inj_1^i)$ is an isomorphism.
|
||||
|
||||
\[
|
||||
R_{i-1}^iF_i\inj_1^i = \left[(F_{i-1} \times \id) (E(\inj_1^i))\right]_1 = \left[(F_{i-1} \times \id) (R_{i-1}^i \inj_1^i,!)\right]_1 = F_{i-1} \inj_1^{i-1}
|
||||
@ -928,7 +917,7 @@
|
||||
|
||||
The input data describing the GAT will be a sequence of finite functors $\Gamma_i : S_{i-1} \to \Set$.
|
||||
|
||||
We will then construct the category $S_i$ by adding a single object $\alpha_i$ to the category $S_{i-1}$, along with morphisms $f : \alpha_j \to \alpha_{i+1}$ for $f \in \Gamma_{i+1}(\alpha_j)$ and $j \leq i$. The morphisms follow the composition condition, describing that every pair of morphisms $f : \alpha_j \to \alpha_{i+1}$ and $g : \alpha_k \to \alpha_{i+1}$ (i.e. $f\in\Gamma_{i+1}(\alpha_k)$ and $g\in\Gamma_{i+1}(\alpha_j)$) and for every morphism of $S_{i}$ $h : \alpha_j \to \alpha_k$, we have $\Gamma_{i+1}(h)(f) \circ f = g$.
|
||||
We will then construct the category $S_i$ by adding a single object $\alpha_i$ to the category $S_{i-1}$, along with morphisms $f : \alpha_j \to \alpha_{i+1}$ for $f \in \Gamma_{i+1}(\alpha_j)$ and $j \leq i$. The morphisms follow the composition condition, describing that every pair of morphisms $f : \alpha_j \to \alpha_{i+1}$ and $g : \alpha_k \to \alpha_{i+1}$ (i.e. $f\in\Gamma_{i+1}(\alpha_k)$ and $g\in\Gamma_{i+1}(\alpha_j)$) and for every morphism $h : \alpha_j \to \alpha_k$ of $S_{i}$, we have $\Gamma_{i+1}(h)(f) \circ f = g$.
|
||||
|
||||
The final category is simply $S = \bigcup S_i$.
|
||||
|
||||
@ -1100,7 +1089,7 @@
|
||||
\subsection{$W(g,h)$ morphism of $\BB_i$}
|
||||
\label{apx:wdefsound}
|
||||
|
||||
The morphism $W(g,h) = g \tl_{i-1} K_{H_iF_{i-1}}(g,h)$ is a morphism of $\BB_i$ as it makes the following diagram commute:
|
||||
The morphism $R_{i-1}^iW(g,h) = g \tl_{i-1} K_{H_iF_{i-1}}(g,h)$ is a morphism of $\BB_i$ as it makes the following diagram commute:
|
||||
\begin{center}
|
||||
% YADE DIAGRAM WghMorphismOfBi.json
|
||||
% GENERATED LATEX
|
||||
@ -1111,7 +1100,7 @@
|
||||
\subsection{$\inj_1^i$ morphism of $\BB_i$}
|
||||
\label{apx:inj1morphism}
|
||||
|
||||
The morphism $\inj_1^i := \inj_1^{i-1}$ is a morphism of $\BB_i$ as it makes the following diagram commute:
|
||||
The morphism $R_{i-1}^i \inj_1^i = \inj_1^{i-1}$ is a morphism of $\BB_i$ as it makes the following diagram commute:
|
||||
\begin{center}
|
||||
% YADE DIAGRAM TlInj1MorphismOfBi.json
|
||||
% GENERATED LATEX
|
||||
@ -1120,10 +1109,9 @@
|
||||
\end{center}
|
||||
|
||||
\subsection{$\{g,h\}_i$ morphism of $\BB_i$}
|
||||
\label{apx:universalpropertymorphismIsMorphism}ç
|
||||
|
||||
$\{g,h\}_i := \{R_{i-1}^ig,h\}_{i-1}$ is a morphism of $\BB_i$ as it makes the following diagram commute:
|
||||
\label{apx:universalpropertymorphismIsMorphism}
|
||||
|
||||
$R_{i-1}^i\{g,h\}_i := \{R_{i-1}^ig,h\}_{i-1}$ is a morphism of $\BB_i$ as it makes the following diagram commute:
|
||||
\begin{center}
|
||||
% YADE DIAGRAM TlUniversalMorphismIsOfBi.json
|
||||
% GENERATED LATEX
|
||||
@ -1131,6 +1119,19 @@
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
|
||||
\subsection{$g \tl_i h$ morphism of $\BB_i$}
|
||||
|
||||
\label{apx:tlMorphismOfBi}
|
||||
|
||||
$(R_{i-1}^ig)\tl_{i-1}h$ is a morphism of $\BB_i$ as it makes the following diagram commute:
|
||||
\begin{center}
|
||||
\begin{scaletikzpicturetowidth}{.9\textwidth}
|
||||
% YADE DIAGRAM TlDefOnMorphisms.json
|
||||
% GENERATED LATEX
|
||||
\input{graphs/TlDefOnMorphisms.tex}
|
||||
% END OF GENERATED LATEX
|
||||
\end{scaletikzpicturetowidth}
|
||||
\end{center}
|
||||
|
||||
\section{$W \dashv E$ adjunction}
|
||||
\label{apx:adjunction}
|
||||
@ -1200,13 +1201,7 @@
|
||||
% GENERATED LATEX
|
||||
\input{graphs/CompositionSecondComponent.tex}
|
||||
% END OF GENERATED LATEX
|
||||
|
||||
\end{center}
|
||||
|
||||
|
||||
\todo{Justifier que la partie du haut commute, i.e. que \[
|
||||
(R_0^{i-1}\{g,\square\})_\El \circ (\inj^{i-1}_2)_\El = \square_\El
|
||||
\]}
|
||||
|
||||
The diagram commutes, and so we can deduce that the second component of $\phi_{XYZ}(f)$ is $h$, by property of the pullback $E(Z)$
|
||||
|
||||
@ -1215,7 +1210,7 @@
|
||||
Now, the converse composition is
|
||||
|
||||
\[
|
||||
\phi_{XYZ}^{-1} (\phi_{XYZ}(f)) = \left\{R_{i-1}^i f \circ \inj_1^{i-1} ; \square \right\}
|
||||
\phi_{XYZ}^{-1} (\phi_{XYZ}(f)) = \left\{R_{i-1}^i f \circ \inj_1^{i-1} ; \square \right\}_{i-1}
|
||||
\]
|
||||
where $\square$ follows the following diagram
|
||||
|
||||
@ -1258,6 +1253,8 @@
|
||||
&=& \left[E(f) \circ \phi_{XYZ}(\ii) \circ (g,h)\right]_1
|
||||
\end{array}\]
|
||||
|
||||
The notation $k^+$ denotes the morphism of $\BB_i$ such that $R_{i-1}^i(k^+) = k$ when the morphism property has already been proven.
|
||||
|
||||
The second components are defined by the pullback properties of $E(Z)$ and $E(Z')$. The two sides that define each morphism are given separately in the two following diagrams.
|
||||
|
||||
\begin{center}
|
||||
@ -1313,9 +1310,7 @@
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
|
||||
\todo{Il manque l'info $\inj_2^{i-1} \circ \en_0^{i-1} = \inj_2^0$ OU ALORS que $\inj_2^{i-1}$ se transpose dans les pullbacks aussi.}
|
||||
|
||||
The first component of the isomorphism is the following isomorphism, where $\eta_{i-1}^{FG}$ if the counit of the adjunction $F_{i-1} \vdash G_{i-1}$, which we know to be an isomorphism from the induction hypothesis.
|
||||
The first component of the isomorphism is the following isomorphism, where $\eta_{i-1}$ if the counit of the adjunction $F_{i-1} \vdash G_{i-1}$, which we know to be an isomorphism from the induction hypothesis.
|
||||
|
||||
\begin{center}
|
||||
% YADE DIAGRAM ReflectionFGIsomorphismFirst.json
|
||||
@ -1342,7 +1337,7 @@
|
||||
% \begin{center}
|
||||
% % YADE DIAGRAM BiMorphismDiagram.json
|
||||
% GENERATED LATEX
|
||||
\input{graphs/BiMorphismDiagram.tex}
|
||||
%\input{graphs/BiMorphismDiagram.tex}
|
||||
% END OF GENERATED LATEX
|
||||
% % GENERATED LATEX
|
||||
% \input{graphs/BiMorphismDiagram.tex}
|
||||
@ -1381,3 +1376,10 @@
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
@ -1 +1 @@
|
||||
{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":9,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":10,"label":{"kind":"normal","label":"(R_0^i Z)_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":11,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":12,"label":{"kind":"normal","label":"\\Cstr^Z","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":4,"id":13,"label":{"kind":"normal","label":"y","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":4,"id":14,"label":{"kind":"normal","label":"\\phi_{XYZ}(f)_2","style":{"alignment":"left","bend":0.1,"color":"black","dashed":true,"head":"default","kind":"normal","position":0.6,"tail":"none"},"zindex":0},"to":0},{"from":4,"id":15,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":7,"id":16,"label":{"kind":"normal","label":"(R_0^{i-1}\\left\\{g,\\square\\right\\})_\\El","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":5,"id":17,"label":{"kind":"normal","label":"H_iF_{i-1}\\inj_1^{i-1}","style":{"alignment":"left","bend":0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.6,"tail":"none"},"zindex":6},"to":8},{"from":8,"id":18,"label":{"kind":"normal","label":"H_iF_{i-1}R_{i-1}^i\\left\\{g,\\square\\right\\}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":5,"id":19,"label":{"kind":"normal","label":"H_iF_{i-1}g","style":{"alignment":"left","bend":-0.1,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":4,"id":20,"label":{"kind":"normal","label":"h","style":{"alignment":"left","bend":-0.1,"color":"black","dashed":true,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":4,"id":21,"label":{"kind":"normal","label":"\\square_\\El","style":{"alignment":"left","bend":-0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":6,"id":22,"label":{"kind":"normal","label":"(\\inj_2^{i-1})_\\El","style":{"alignment":"left","bend":-0.1,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":11,"id":23,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":9}],"nodes":[{"id":0,"label":{"isMath":true,"label":"E(Z)","pos":[473,329.8125],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"(R_0^i Z)_\\El","pos":[632,329.8125],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[632,459.8125],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i Z","pos":[473,459.8125],"zindex":-10000}},{"id":4,"label":{"isMath":true,"label":"Y","pos":[108,167.8125],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"H_iF_{i-1}X","pos":[108,329.8125],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"(K_{H_iF_{i-1}}(X,Y))_\\El","pos":[108,87.8125],"zindex":0}},{"id":7,"label":{"isMath":true,"label":"R_0^{i-1}(X \\tl^{i-1} K_{H_iF_{i-1}}(X,Y))_\\El","pos":[632,167.8125],"zindex":0}},{"id":8,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i(W(X,Y))","pos":[182,459.8125],"zindex":-10000}}],"sizeGrid":200,"title":"1"}]},"version":12}
|
||||
{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":9,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":10,"label":{"kind":"normal","label":"(R_0^i Z)_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":11,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":12,"label":{"kind":"normal","label":"\\Cstr^Z","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":4,"id":13,"label":{"kind":"normal","label":"y","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":4,"id":14,"label":{"kind":"normal","label":"\\phi_{XYZ}(f)_2","style":{"alignment":"right","bend":0.1,"color":"black","dashed":true,"head":"default","kind":"normal","position":0.4,"tail":"none"},"zindex":0},"to":0},{"from":4,"id":15,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":7,"id":16,"label":{"kind":"normal","label":"(R_0^{i-1}\\left\\{g,\\square\\right\\})_\\El","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":5,"id":17,"label":{"kind":"normal","label":"H_iF_{i-1}\\inj_1^{i-1}","style":{"alignment":"left","bend":0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.6,"tail":"none"},"zindex":6},"to":8},{"from":8,"id":18,"label":{"kind":"normal","label":"H_iF_{i-1}R_{i-1}^i\\left\\{g,\\square\\right\\}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":5,"id":19,"label":{"kind":"normal","label":"H_iF_{i-1}g","style":{"alignment":"left","bend":-0.1,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":4,"id":20,"label":{"kind":"normal","label":"h","style":{"alignment":"left","bend":-0.1,"color":"black","dashed":true,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":4,"id":21,"label":{"kind":"normal","label":"\\square_\\El","style":{"alignment":"left","bend":-0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":6,"id":22,"label":{"kind":"normal","label":"(\\inj_2^{i-1})_\\El","style":{"alignment":"left","bend":-0.1,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":11,"id":23,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":9}],"nodes":[{"id":0,"label":{"isMath":true,"label":"E(Z)","pos":[473,329.8125],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"(R_0^i Z)_\\El","pos":[632,329.8125],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[632,459.8125],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i Z","pos":[473,459.8125],"zindex":-10000}},{"id":4,"label":{"isMath":true,"label":"Y","pos":[108,167.8125],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"H_iF_{i-1}X","pos":[108,329.8125],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"(K_{H_iF_{i-1}}(X,Y))_\\El","pos":[108,87.8125],"zindex":0}},{"id":7,"label":{"isMath":true,"label":"R_0^{i-1}(X \\tl^{i-1} K_{H_iF_{i-1}}(X,Y))_\\El","pos":[632,167.8125],"zindex":0}},{"id":8,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i(W(X,Y))","pos":[182,459.8125],"zindex":-10000}}],"sizeGrid":200,"title":"1"}]},"version":12}
|
||||
@ -1 +1 @@
|
||||
{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":9,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":10,"label":{"kind":"normal","label":"(R_0^i Z)_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":11,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":12,"label":{"kind":"normal","label":"\\Cstr^Z","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":4,"id":13,"label":{"kind":"normal","label":"y","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":4,"id":14,"label":{"kind":"normal","label":"\\phi_{XYZ}(f)_2","style":{"alignment":"left","bend":0,"color":"black","dashed":true,"head":"default","kind":"normal","position":0.6,"tail":"none"},"zindex":0},"to":0},{"from":4,"id":15,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":7,"id":16,"label":{"kind":"normal","label":"(R_0^{i-1}f)_\\El","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":5,"id":17,"label":{"kind":"normal","label":"H_iF_{i-1}\\inj_0^{i-1}","style":{"alignment":"left","bend":0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.6,"tail":"none"},"zindex":6},"to":8},{"from":8,"id":18,"label":{"kind":"normal","label":"H_iF_{i-1}R_{i-1}^if","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":6,"id":19,"label":{"kind":"normal","label":"\\inj_2^{i-1}","style":{"alignment":"left","bend":-0.1,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":11,"id":20,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":9}],"nodes":[{"id":0,"label":{"isMath":true,"label":"E(Z)","pos":[440,222],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"(R_0^i Z)_\\El","pos":[600,222],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[600,382],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i Z","pos":[440,382],"zindex":-10000}},{"id":4,"label":{"isMath":true,"label":"Y","pos":[40,121],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"H_iF_{i-1}X","pos":[40,222],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"(K_{H_iF_{i-1}}(X,Y))_\\El","pos":[40,40],"zindex":0}},{"id":7,"label":{"isMath":true,"label":"R_0^{i-1}(X \\tl^{i-1} K_{H_iF_{i-1}}(X,Y))_\\El","pos":[600,132],"zindex":0}},{"id":8,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i(W(X,Y))","pos":[200,382],"zindex":-10000}}],"sizeGrid":80,"title":"1"}]},"version":12}
|
||||
{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":9,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":10,"label":{"kind":"normal","label":"(R_0^i Z)_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":11,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":12,"label":{"kind":"normal","label":"\\Cstr^Z","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":4,"id":13,"label":{"kind":"normal","label":"y","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":4,"id":14,"label":{"kind":"normal","label":"\\phi_{XYZ}(f)_2","style":{"alignment":"left","bend":0,"color":"black","dashed":true,"head":"default","kind":"normal","position":0.6,"tail":"none"},"zindex":0},"to":0},{"from":4,"id":15,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":7,"id":16,"label":{"kind":"normal","label":"(R_0^{i-1}f)_\\El","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":5,"id":17,"label":{"kind":"normal","label":"H_iF_{i-1}\\inj_1^{i-1}","style":{"alignment":"left","bend":0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.6,"tail":"none"},"zindex":6},"to":8},{"from":8,"id":18,"label":{"kind":"normal","label":"H_iF_{i-1}R_{i-1}^if","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":6,"id":19,"label":{"kind":"normal","label":"\\inj_2^{i-1}","style":{"alignment":"left","bend":-0.1,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":11,"id":20,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":9}],"nodes":[{"id":0,"label":{"isMath":true,"label":"E(Z)","pos":[409,222],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"(R_0^i Z)_\\El","pos":[569,222],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[569,375],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i Z","pos":[409,375],"zindex":-10000}},{"id":4,"label":{"isMath":true,"label":"Y","pos":[40,121],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"H_iF_{i-1}X","pos":[40,222],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"(K_{H_iF_{i-1}}(X,Y))_\\El","pos":[40,40],"zindex":0}},{"id":7,"label":{"isMath":true,"label":"R_0^{i-1}(X \\tl^{i-1} K_{H_iF_{i-1}}(X,Y))_\\El","pos":[569,132],"zindex":0}},{"id":8,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i(W(X,Y))","pos":[125,375],"zindex":-10000}}],"sizeGrid":80,"title":"1"}]},"version":12}
|
||||
@ -1 +1 @@
|
||||
{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\CC{{\\ensuremath{\\mathcal{C}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":3,"label":{"kind":"normal","label":"\\eta^{FG}_{i-1}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":4,"label":{"kind":"normal","label":"F_{i-1}(\\inj_1^{i-1})","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":5,"label":{"kind":"normal","label":"\\simeq","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":6,"label":{"kind":"normal","label":"\\simeq","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2}],"nodes":[{"id":0,"label":{"isMath":true,"label":"X","pos":[100,100],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"F_{i-1}G_{i-1}X","pos":[300,100],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"F_{i-1}(G_{i-1}X \\tl^{i-1}K_\\bullet(G_{i-1}X,(B,H_i\\eta_{i-1}\\circ g)))","pos":[626,100],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12}
|
||||
{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\CC{{\\ensuremath{\\mathcal{C}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":3,"label":{"kind":"normal","label":"\\eta_{i-1}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":4,"label":{"kind":"normal","label":"F_{i-1}(\\inj_1^{i-1})","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":5,"label":{"kind":"normal","label":"\\simeq","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":6,"label":{"kind":"normal","label":"\\simeq","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2}],"nodes":[{"id":0,"label":{"isMath":true,"label":"X","pos":[100,100],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"F_{i-1}G_{i-1}X","pos":[300,100],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"F_{i-1}(G_{i-1}X \\tl^{i-1}K_\\bullet(G_{i-1}X,(B,H_i\\eta_{i-1}\\circ g)))","pos":[626,100],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12}
|
||||
@ -1 +1 @@
|
||||
{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\CC{{\\ensuremath{\\mathcal{C}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":6,"label":{"kind":"normal","label":"\\id_B","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":7,"label":{"kind":"normal","label":"\\simeq","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":8,"label":{"kind":"normal","label":"h","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":1,"id":9,"label":{"kind":"normal","label":"H_i\\eta^{FG}_{i-1} \\circ g","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":4,"id":10,"label":{"kind":"normal","label":"H_iF_{i-1}\\inj_1^{i-1}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":0,"id":11,"label":{"kind":"normal","label":"g","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":5,"id":12,"label":{"kind":"normal","label":"H_i\\eta_{i-1}^{FG}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":0,"id":13,"label":{"kind":"normal","label":"\\simeq","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":5,"id":14,"label":{"kind":"normal","label":"\\simeq","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":4,"id":15,"label":{"kind":"normal","label":"\\simeq","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3}],"nodes":[{"id":0,"label":{"isMath":true,"label":"B","pos":[100,100],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"B","pos":[300,100],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"A","pos":[678,100],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}(G_{i-1}X \\tl^{i-1}K_\\bullet(G_{i-1}X,(B,H_i\\eta_{i-1}\\circ g)))","pos":[678,211],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"H_iF_{i-1}G_{i-1}X","pos":[300,211],"zindex":-10000}},{"id":5,"label":{"isMath":true,"label":"H_iX","pos":[100,211],"zindex":-10000}}],"sizeGrid":200,"title":"1"}]},"version":12}
|
||||
{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\CC{{\\ensuremath{\\mathcal{C}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":6,"label":{"kind":"normal","label":"\\id_B","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":7,"label":{"kind":"normal","label":"\\simeq","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":8,"label":{"kind":"normal","label":"h","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":1,"id":9,"label":{"kind":"normal","label":"H_i\\eta_{i-1} \\circ g","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":4,"id":10,"label":{"kind":"normal","label":"H_iF_{i-1}\\inj_1^{i-1}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":0,"id":11,"label":{"kind":"normal","label":"g","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":5,"id":12,"label":{"kind":"normal","label":"H_i\\eta_{i-1}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":0,"id":13,"label":{"kind":"normal","label":"\\simeq","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":5,"id":14,"label":{"kind":"normal","label":"\\simeq","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":4,"id":15,"label":{"kind":"normal","label":"\\simeq","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3}],"nodes":[{"id":0,"label":{"isMath":true,"label":"B","pos":[100,100],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"B","pos":[300,100],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"A","pos":[678,100],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}(G_{i-1}X \\tl^{i-1}K_\\bullet(G_{i-1}X,(B,H_i\\eta_{i-1}\\circ g)))","pos":[678,211],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"H_iF_{i-1}G_{i-1}X","pos":[300,211],"zindex":-10000}},{"id":5,"label":{"isMath":true,"label":"H_iX","pos":[100,211],"zindex":-10000}}],"sizeGrid":200,"title":"1"}]},"version":12}
|
||||
@ -1 +1 @@
|
||||
{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\CC{{\\ensuremath{\\mathcal{C}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":4,"label":{"kind":"normal","label":"(H_i(F_{i-1}\\inj_\\tl^{i-1})^{-1})","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":5,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":6,"label":{"kind":"normal","label":"\\simeq","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":2,"id":7,"label":{"kind":"normal","label":"\\inj_2^{i-1}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3}],"nodes":[{"id":0,"label":{"isMath":true,"label":"H_iF_{i-1}(X \\tl^{i-1} K_{H_iF_{i-1}}(X,Y))) ","pos":[230,46],"zindex":0}},{"id":1,"label":{"isMath":true,"label":" H_iF_{i-1}X","pos":[230,138],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\left(K_{H_iF_{i-1}}(X,Y)\\right)_\\UU","pos":[230,204],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"R_0^{i-1}\\left(X \\tl^{i-1}K_{H_iF_{i-1}}(X,Y)\\right)_\\UU","pos":[230,300],"zindex":0}}],"sizeGrid":92,"title":"1"}]},"version":12}
|
||||
{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\CC{{\\ensuremath{\\mathcal{C}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":4,"label":{"kind":"normal","label":"H_i(F_{i-1}\\inj_\\tl^{i-1})^{-1}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":5,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":6,"label":{"kind":"normal","label":"\\simeq","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":2,"id":7,"label":{"kind":"normal","label":"\\inj_2^{i-1}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3}],"nodes":[{"id":0,"label":{"isMath":true,"label":"H_iF_{i-1}(X \\tl^{i-1} K_{H_iF_{i-1}}(X,Y))) ","pos":[230,46],"zindex":0}},{"id":1,"label":{"isMath":true,"label":" H_iF_{i-1}X","pos":[230,138],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\left(K_{H_iF_{i-1}}(X,Y)\\right)_\\UU","pos":[230,204],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"R_0^{i-1}\\left(X \\tl^{i-1}K_{H_iF_{i-1}}(X,Y)\\right)_\\UU","pos":[230,300],"zindex":0}}],"sizeGrid":92,"title":"1"}]},"version":12}
|
||||
Loading…
x
Reference in New Issue
Block a user