Compare commits
2 Commits
a779d3ed7f
...
f0c9453836
| Author | SHA1 | Date | |
|---|---|---|---|
f0c9453836
|
|||
|
a4596781d3
|
@ -23,10 +23,10 @@
|
||||
|
||||
\newpage
|
||||
|
||||
\section{Sort specification}
|
||||
\section{Introduction}
|
||||
|
||||
A Generalized Algebraic Theory (or GAT), first introduced by Cartmell \cite{CartmellGATs}, is a syntactic specification of an algebraic structure. From a GAT, one can define a category of models describing the models of the algebraic structure.
|
||||
A GAT starts with a sort specification i.e. a list of sort declarations, eventually followed by a list of constructors.
|
||||
A GAT typically starts with a sort specification i.e. a list of sort declarations, eventually followed by a list of constructors.
|
||||
In this document, we will not ask ourselves about the specific syntax of GATs, a \enquote{vague} definition is enough.
|
||||
|
||||
\paragraph{Sort specification}
|
||||
@ -46,9 +46,9 @@
|
||||
|
||||
A model of this category is a triple
|
||||
\begin{itemize}
|
||||
\item A set $X_\Con : \Set$
|
||||
\item A family of sets $\left(X_\Ty\left(\Gamma\right)\right)_{\Gamma \in _\Con}$
|
||||
\item A family of sets $\left(X_\Tm\left(\Delta,A\right)\right)_{\Delta\in X_\Con,\: A \in X_\Ty\left(\Delta\right)}$
|
||||
\item A set $X_\Con$ of contexts
|
||||
\item A family of sets $\left(X_\Ty\left(\Gamma\right)\right)_{\Gamma \in _\Con}$ of types, indexed by contexts
|
||||
\item A family of sets $\left(X_\Tm\left(\Delta,A\right)\right)_{\Delta\in X_\Con,\: A \in X_\Ty\left(\Delta\right)}$ of terms, indexed by contexts and types.
|
||||
\end{itemize}
|
||||
|
||||
\paragraph{Constructor specification}
|
||||
@ -58,87 +58,62 @@
|
||||
\vspace{1em}
|
||||
\renewcommand\arraystretch{1.5}
|
||||
\begin{tabular}{p{.37\textwidth}|p{.6\textwidth}}
|
||||
$\operatorname{unit} : (\Gamma : \Con) \to \Ty\;\Gamma$ & In any context $\Gamma$, a type of $\Ty\;\Gamma$ called unit.\\
|
||||
$\operatorname{unit} : (\Gamma : \Con) \to \Ty\;\Gamma$ & In any context $\Gamma$, a type of $\Ty\;\Gamma$ called unit.\\
|
||||
|
||||
$\operatorname{eq}: (\Gamma : \Con) \to (A : \Ty\;\Gamma) \to$
|
||||
|
||||
$\qquad\Tm\;\Gamma A \to \Tm\;\Gamma A \to \Ty\;\Gamma$ & In any context $\Gamma$ and type $A$ in this context, for every terms $t$,$u$ of the type $A$, we have a type $\operatorname{eq} \Gamma A t u$ describing the equality of the terms.
|
||||
$\operatorname{tt}: (\Gamma : \Con) \to \Tm\;\Gamma\;(\operatorname{unit}\;\Gamma)$ & In any context $\Gamma$, we have a term whose type is the $\operatorname{unit}$ of this context ($\operatorname{unit}\;\Gamma$).
|
||||
\end{tabular}
|
||||
\vspace{1em}
|
||||
|
||||
This adds to the previous model two functions that \enquote{points} one element of the sets
|
||||
\begin{itemize}
|
||||
\item For each $\Gamma \in X_\Con$, an element $\operatorname{unit}\;\Gamma \in X_\Ty(\Gamma)$
|
||||
\item For each $\Gamma \in X_\Con$, for each $A \in X_\Ty(\Gamma)$, for each elements $u,v \in X_\Tm(\Gamma,A)$, an element $\operatorname{eq}\;\Gamma\;A\;u\;v \in X_\Ty(\Gamma)$
|
||||
\item For each $\Gamma \in X_\Con$, an element $\operatorname{tt}\;\Gamma \in X_\Tm(\Gamma,\operatorname{unit}\;\Gamma)$
|
||||
\end{itemize}
|
||||
|
||||
Sort declarations describe the sets that the model contains, whereas the constructors describe elements of these sets.
|
||||
|
||||
\paragraph{Two-sortification}
|
||||
|
||||
There is a process that allows us to transform a GAT into a GAT with only two sorts. This process is used by Philippo Sestini in his thesis \cite{SestiniPhD} refering the work of Zongpu Szumi Xie \cite{AmbrusSzumiXie2sort}:
|
||||
There is a process that allows us to transform a GAT into a GAT with only two sorts.
|
||||
The sort specification of the transformed GAT is always the same, and contains these two sort declarations:
|
||||
|
||||
\vspace{1em}
|
||||
\begin{tabular}{p{0.37\textwidth}|p{0.5\textwidth}}
|
||||
$\UU : \Set$ & The set of sorts \\
|
||||
$\El : \mathcal{O} \to \Set$ & For every sort object $o$ in the set of sorts, a set called $\El(o)$ of objects corresponding to the sort object. We will write this set $\underline{o}$ rather than $\El(o)$.
|
||||
\end{tabular}
|
||||
\vspace{1em}
|
||||
|
||||
Then, we replace all occurrences of $\Set$ to $\mathcal{O}$, and we apply $\El$ to every parameter. For example, the Type Theory GAT presented above becomes that which follows:
|
||||
|
||||
\begin{tabular}{p{0.4\textwidth}|p{0.5\textwidth}}
|
||||
$\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 "$\Tm\;\Gamma\;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)}$ &
|
||||
$\dots$
|
||||
\end{tabular}
|
||||
|
||||
This process has been observed by Zongpu Szumi Xie \cite{AmbrusSzumiXie2sort}, and Philippo Sestini used it in his thesis \cite{SestiniPhD}:
|
||||
|
||||
\begin{quote}
|
||||
Many instances of multi-sorted IITs [IITs are another type of GATs] can be reduced to equivalent two-sorted IITs, via a systematic reduction method originally observed by Zongpu (Szumi) Xie. We are not aware of a formal proof of this construction for arbitrary IITs, but we conjecture that it does apply to all instances of induction-induction and consequently that it shows two-sorted IITs are enough to represent any specifiable IIT.
|
||||
\end{quote}
|
||||
|
||||
The goal of this document is to prove semantically that this transformation makes sense. More specifically, we prove that this transformation is a left adjunct functor of a coreflection. This is enough to prove what Sestini conjectured, i.e. that the initial object in the 2-sort category creates back the initial object of the primary category \cite[5. General]{nlab:reflective_subcategory}.
|
||||
|
||||
We will now present this transformation. The sort specification of the transformed GAT is always the same, and contains two sort declarations (as planned):
|
||||
|
||||
\vspace{1em}
|
||||
\begin{tabular}{p{0.37\textwidth}|p{0.5\textwidth}}
|
||||
$\mathcal{O} : \Set$ & The set of sorts \\
|
||||
$\underline{\;\bullet\;} : \mathcal{O} \to \Set$ & For every sort object $o$ in the set of sorts, a set called $\underline{o}$ of objects corresponding to the sort object.
|
||||
\end{tabular}
|
||||
\vspace{1em}
|
||||
|
||||
Category of models of this two-sort specification are intuitively the category of families of set $\FamSet$, composed of pairs $\left(X_0:\Set,X_1: X_0 \to \Set\right)$.
|
||||
|
||||
Then, we replace all occurrences of $\Set$ to $\mathcal{O}$, and we apply underline to every parameter. For example, the Type Theory GAT presented above becomes that which follows:
|
||||
|
||||
\begin{tabular}{p{0.4\textwidth}|p{0.5\textwidth}}
|
||||
$\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$}\\
|
||||
$\operatorname{unit} : (\Gamma : \underline{\Con}) \to \underline{\Ty\;\Gamma}$ &
|
||||
For each object $\Gamma$ corresponding to the sort object $\Con$, an object called \enquote{$\operatorname{unit} \Gamma$} corresponding to the sort object $\Ty\;\Gamma$\\
|
||||
$\operatorname{eq}: (\Gamma : \underline{\Con}) \to (A : \underline{\Ty\;\Gamma}) \to$ \newline
|
||||
$\qquad\underline{\Tm\;\Gamma A} \to \underline{\Tm\;\Gamma A} \to \underline{\Ty\;\Gamma}$ &
|
||||
$\dots$
|
||||
\end{tabular}
|
||||
|
||||
\paragraph{$\FamSet$ as functors}
|
||||
|
||||
In the rest of the document, we will denote the simple category containing two elements and one non-identity arrow between them as $\TT$. The objects and arrow of this category are pictured below.
|
||||
|
||||
\begin{center}
|
||||
% YADE DIAGRAM G0.json
|
||||
% GENERATED LATEX
|
||||
\input{graphs/G0.tex}
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
|
||||
The functors over this categories are equivalent to families of sets, using the following mapping :
|
||||
|
||||
\[
|
||||
\begin{array}{l|l}
|
||||
X_\UU = X_0 & X_0 = X_\UU \\
|
||||
X_\El = \displaystyle\coprod_{A\in X_0}X_1(A) & X_1 = A \mapsto X_p^{-1}(\{A\})\\
|
||||
X_p = (A,B) \mapsto A &
|
||||
\end{array}
|
||||
\]
|
||||
|
||||
Therefore the categories of sorts of the transformed GATs will be built atop of the category $\TSet$ rather than atop of the category $\FamSet$ as it makes the formal proofs more elegant.
|
||||
|
||||
\paragraph{Goal}
|
||||
|
||||
The goal of this document is to make a relation between the category of models of the GAT $\CC$ and the category of models of the two-sortified GAT $\BB$. This relation will be an adjunction $F \vdash G$ that we will prove to be a coreflection.
|
||||
The goal my internship was to formally study this transformation, and to try to find a relation between the semantics of a GAT and its two-sorted version.
|
||||
|
||||
The category $\BB$ is built with an adjunction $R \vdash L$ to the category of models of the simple two-sort specification of sorts $\TSet$.
|
||||
We managed to construct a coreflection between a category of models and the category of models of the transformed GAT.
|
||||
The existence of this coreflection is enough to prove what Sestini conjectured.
|
||||
|
||||
We will give a formal definition of this coreflection in next section. It will consist of an adjunction $F \vdash G$ between the category $\CC$ of the models of the GAT and the category $\BB$ of the models of the two-sortified GAT, where G is full and faithful.
|
||||
The category $\BB$ will be built with a forgetful functor $R$ to $\BB_0$, the category of models of the two-sort sort specification $(\mathcal{O},\El)$. This forgetful $R$ functor is a composition of monadic functors, one for each sort constructor.
|
||||
|
||||
\begin{center}
|
||||
% YADE DIAGRAM G1-0.json
|
||||
@ -147,48 +122,124 @@
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
|
||||
\section{Construction of the coreflection}
|
||||
|
||||
\subsection{Preliminaries}
|
||||
|
||||
\paragraph{Category of models of the two-sort sort specification}
|
||||
|
||||
The usual way of defining the category of models of the two-sort specification $\BB_0$ is by taking the category of families of sets. However, in order to have more elegant constructions, we will use a the category of models of the two-sort specification the category $\TSet$ of presheaves over the category with one arrow.
|
||||
|
||||
In the rest of the document, we will denote this category with one arrow as $\TT$. The objects and arrow of this category are pictured below.
|
||||
|
||||
\begin{center}
|
||||
% YADE DIAGRAM G0.json
|
||||
% GENERATED LATEX
|
||||
\input{graphs/G0.tex}
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
|
||||
With this formalisation, a model of the two-sort GAT is a functor $X : \TSet$, such that
|
||||
\begin{itemize}
|
||||
\item $X_\UU$ is the set of the \enquote{sort objects}
|
||||
\item For each sort object $\Gamma \in X_\UU$, the set of objects corresponding to the sort object is $X_p^-1(\{\Gamma\}) \subset X_\El$
|
||||
\end{itemize}
|
||||
|
||||
Therefore the categories of models of the transformed GATs will be built atop of this category $\BB_0 = \TSet$.
|
||||
|
||||
\paragraph{Grothendieck Construction}
|
||||
For a category $\mathcal{C}$ and a functor $F : \mathcal{C} \to \Cat$, the Grothendieck construction is a category whose objects are pairs of
|
||||
\begin{itemize}
|
||||
\item $X$ an object of $\mathcal{C}$
|
||||
\item an object of $F(X)$
|
||||
\end{itemize}
|
||||
|
||||
The morphism $(X,Y) \to (X',Y')$ is therefore a pair of a morphism $f : X \to X'$ in $\mathcal{C}$ and a morphism $g : F(f)(Y) \to Y'$ in $H(X')$.
|
||||
|
||||
We will denote this category $(X : \mathcal{C}) \times F(X)$ as its objects are pairs. It can some times be found written as $\int^\mathcal{C} F$ or $\sqint^\mathcal{C} F$
|
||||
|
||||
\paragraph{Slice category}
|
||||
For a category $\mathcal{C}$ and $X$ an object in that category, the slice category (or over category) $\mathcal{C}/A$ is a category whose objects are pairs of
|
||||
\begin{itemize}
|
||||
\item $Y$ an object of $\mathcal{C}$
|
||||
\item an arrow $X \to Y$ of $\mathcal{C}$
|
||||
\end{itemize}
|
||||
|
||||
A morphism $(Y,f) \to (Y',f')$ is a morphism $g : Y \to Y'$ such that $g \circ f = f'$.
|
||||
|
||||
We can deduce a functor $\left(\mathcal{C}/\dash\right) : \mathcal{C} \to \Cat$ from this construction.
|
||||
|
||||
If the category $\mathcal{C}$ is $\Set$, we have that $\Set/X \cong \Set^X$.
|
||||
|
||||
We will often concatenate the two method above to create from a category $\mathcal{C}$ and a functor $H : \mathcal{C} \to \Set$ a new category $(X : \mathcal{C}) \times \left(\Set\middle/H(X)\right)$.
|
||||
|
||||
\paragraph{$\Hbar$ functor}
|
||||
|
||||
Where $\Hbar_A$ is a functor $(X:C) \times (\Set/A(X)) \to \TSet$ defined as
|
||||
\[
|
||||
\Hbar_X(X,(Y,f)) = \TSetObject{Y}{f}{A(X)}
|
||||
\]
|
||||
The morphisms are translated as-is.
|
||||
|
||||
\begin{remark}
|
||||
This functor can be constructed using the property of the Grothendieck construction
|
||||
\end{remark}
|
||||
|
||||
\subsection{Constructing the categories}
|
||||
|
||||
We will construct both categories $\CC$ and $\BB$ recursively, adding new sorts one by one.
|
||||
The categories $\CC_i$ are described as in Fiore's paper \cite{Fiore2008}, and the categories $\BB_i$ are constructed atop of the category $\TSet$ with a method inspired by the category of models described by Altenkirch et al. \cite{Altenkirch2018}.
|
||||
We will construct both categories $\CC$ and $\BB$ recursively, adding new sorts one by one for each constructor. At each recursion step, we will build the categories, the adjunction, and keep some invariants that will be stated in \autoref{sec:hypotheses}.
|
||||
|
||||
At the i-th recursion step, we will build the category $\CC_i$ which is the category of models of the $i$ first sorts of the sort specification. $\BB_i$ will samewise be the category of models of the 2-sorted $i$ first sorts of the sort specification.
|
||||
|
||||
The overall recursive construction of the categories and of the adjunctions $F_i \vdash G_i$ is given below.
|
||||
|
||||
\begin{center}
|
||||
% YADE DIAGRAM G1.json
|
||||
% GENERATED LATEX
|
||||
\input{graphs/G1.tex}
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
|
||||
The first step of our recursion is the trivial adjunction $\lambda . \star \vdash \lambda . 1$ between the categories $\BB_0 = \TSet$ and $\CC_0 = 1$.
|
||||
|
||||
The functors $R_{i-1}^i$ are the forgetful monadic functors that forget about the $i$-th sort contsructor. They have a left adjoint denoted $L_{i-1}^i$.
|
||||
As we can compose the adjunctions $R_0^1$,$R_1^2$,...,$R_{i-1}^i$, we will use the two following adjunctions
|
||||
\[\begin{array}{c}
|
||||
R_0^i = R_{0}^{i-1} \circ R_{i-1}^{i} = R_{0}^{1} \circ ... \circ R_{i-1}^{i}\\
|
||||
L_0^i = L_{i-1}^{i} \circ L_{0}^{i-1} = L_{i-1}^{i} \circ ... \circ L_{0}^{1}
|
||||
\end{array}\]
|
||||
|
||||
\begin{remark}
|
||||
There is also an adjunction chain between $\CC_0$,$\dots$,$\CC_{i-1}$,$\CC_i$, but we don't use it in the proof.
|
||||
\end{remark}
|
||||
|
||||
\subsubsection{Constructing $\CC_i$}
|
||||
|
||||
We construct the category $\CC_i$ as the following pair:
|
||||
\[
|
||||
\CC_i = (X : \CC_{i-1}) \times \left(\Set\middle/\Hom(O_i,X)\right)
|
||||
\CC_i = (X : \CC_{i-1}) \times \left(\Set\middle/H_i\right) = (X : \CC_{i-1}) \times \left(\Set^{H_i}\right)
|
||||
\]
|
||||
where for any category $\mathcal{C}$ and $X$ an object of $\mathcal{C}$, $(\mathcal{C}/X)$ it the slice category (or over category) of arrows pointing out of $X$ (its objects $(Y,f)$ are arrows $f : X \to Y$ and its morphisms are morphisms creating commutative triangles).\inlinetodo{Assez clair ?} \inlinetodo{On ne voit pas que $(\Set/A(X)) \cong \Set^{A(X)}$}
|
||||
and where $H_i$ is a specific representable functor $\CC_{i-1} \to \Set$, such that $H_i(X)$ is the set of parameters for the construction of the new sort.
|
||||
|
||||
and where $O_i$ is a specific object of the category $\CC_{i-1}$, such that $\Hom(O_i,X)$ is the set of parameters for the construction of the new sort.
|
||||
\todo{Comment indiquer que la paire est dépendante ?}
|
||||
|
||||
I will give now an example of those $O_i$ objects for our type theory example. We begin with
|
||||
\paragraph{$H_i$ functors for Type Theory}
|
||||
I will give now an example of those $H_i$ objects for our type theory example. We begin with
|
||||
\[
|
||||
O_1 = \star \in \operatorname{Obj}(\CC_0) = \operatorname{Obj}(1)
|
||||
H_1(\star) = 1 \in \operatorname{Obj}(\Set)
|
||||
\]
|
||||
so $\Hom(O_1,X) = 1$, which corresponds to the fact that $\Con$ takes no parameter.
|
||||
which corresponds to the fact that $\Con$ takes no parameter.
|
||||
|
||||
Therefore $\CC_1 = 1 \times \Set^1 = \Set$
|
||||
Therefore $\CC_1 = 1 \times \Set^1 = \Set$, and the set of a model corresponds to \enquote{the set of contexts}.
|
||||
|
||||
Then, we take the singleton object $O_2 = 1$ (this means, that types need \emph{one} context to be built), and so, for a set $X_\Con$, $\Hom(O_2,X_\Con) \cong X_\Con$, which corresponds to the fact that $\Ty$ take one $\Con$ as a parameter.
|
||||
Then, we take the functor $H_2(X_\Con) = X_\Con$ (this means, that types need \emph{one} context to be built).
|
||||
|
||||
Therefore $\CC_2 = (X:\Set) \times \Set^X \cong \FamSet$.
|
||||
Therefore $\CC_2 = (X:\Set) \times \Set^X \cong \FamSet$, families of sets.
|
||||
|
||||
Finally, we take the object $O_3 = (1, \lambda \star . 1)$ (this means that terms need \emph{one} context, and \emph{one} type of that context). With this object, for a pair $(X_\Con,X_\Ty)$ in $\CC_2$, we have $\Hom(O_3,(X_\Con,X_\Ty)) \cong \left(\Gamma: X_\Con, A: X_\Ty(\Gamma)\right)$.
|
||||
Finally, we take the functor $H_3(X_\Con,X_\Ty) = \sum_{\Gamma : X_\Con}X_\Ty(\Gamma)$ (this means that terms need \emph{one} context, and \emph{one} type of that context).
|
||||
|
||||
The final category $\CC_3$ is composed of triples $(X_\Con: \Set, X_\Ty : X_\Con \to \Set, X_\Tm : (\Delta: X_\Con) \to X_\Ty(\Delta) \to \Set)$
|
||||
|
||||
\begin{remark}
|
||||
There is a way of getting the object $O_i$ from the syntax, which is given in \autoref{sec:CtoSSetFiore}.
|
||||
There is a way of getting the functor $H_i$ from the syntax, which is given in \autoref{sec:CtoSSetFiore}.
|
||||
\end{remark}
|
||||
|
||||
\subsubsection{Constructing $\BB_i$}
|
||||
@ -198,9 +249,10 @@
|
||||
An object of $\BB_i$ is
|
||||
\begin{itemize}
|
||||
\item an object $X$ of $\BB_{i-1}$
|
||||
\item a \enquote{sort constructor} $\Cstr_i$ as a function $\Hom_{\BB_{i-1}} (G_{i-1}O_i,X) \to (R_0^{i-1}X)_\UU$
|
||||
\item a \enquote{sort constructor} $\Cstr_i$ as a function $H_i(F_{i-1}X) \to (R_0^{i-1}X)_\UU$
|
||||
\newline
|
||||
where $O_i$ is the object of $\CC_{i-1}$ that describe the sort constructor being processed, and $G_{i-1}$ is the left part of the adjunction $\CC_{i-1} \to \BB_{i-1}$ that we are defining recursively at the same time.
|
||||
where $H_i$ is the functor $\CC_{i-1} \to \Set$ that describe the sort constructor being processed, and $F_{i-1}$ is the right part of the adjunction $\BB_{i-1} \to \CC_{i-1}$ that we are defining recursively at the same time.
|
||||
This $H_i$ functor will be so that $H_i \circ F_{i-1} \circ \inj_1^{i-1}$ is an isomorphism. \inlinetodo{Pas déclaré ici, c'est grâve ?}
|
||||
\end{itemize}
|
||||
|
||||
|
||||
@ -216,35 +268,31 @@
|
||||
Identities and compositions are that of the category $\BB_{i-1}$, and categorical equalities are trivially derived from the diagram above.
|
||||
|
||||
\paragraph{The adjunction}
|
||||
We also define a functor $R_{i-1}^i : \BB_i \to \BB_{i-1}$ that sends objects and morphisms to their first component. This functor is a \emph{right adjunct} of another functor we call $L_{i-1}^i$.
|
||||
We also define a functor $R_{i-1}^i : \BB_i \to \BB_{i-1}$ that sends objects and morphisms to their first component. This functor is a \emph{right adjoint} of another functor we call $L_{i-1}^i$.
|
||||
|
||||
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.
|
||||
\[\begin{array}{c}
|
||||
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}
|
||||
\end{array}\]
|
||||
|
||||
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 will also denote $\eta_i^j : \mathbf{1} \to R_i^j L_i^j$ and $\varepsilon_i^j : L_i^j R_i^j \to \mathbf{1}$ to be the unit and counit of the adjunction $R_i^j \vdash L_i^j$.
|
||||
|
||||
\paragraph{The coproduct}
|
||||
For an object $X$ in $\BB_i$ and $Y$ in $\BB_0$, there is a coproduct $X \oplus_i L_0^i Y$ in the category $\BB_{i-1}$. We will denote as $\inj_1^i : X \to X \oplus L_0^iY$ (resp. $\inj_2^i : L_0^iY \to X \oplus L_0^iY$) the first (resp. second) injector of the coproduct of $\BB_i$. For every morphism $f : X \to Z$ and $g : L_0^iY \to Z$, we will denote with $\{f;g\}$ the unique morphism from $X \oplus L_0^iY$ to $Z$ such that $\{f;g\} \circ \inj^i_1 = f$ and $\{f;g\} \circ \inj^i_2 = g$.
|
||||
For an object $X$ in $\BB_i$ and $Y$ in $\BB_0$, there is a coproduct $X \oplus_i L_0^i Y$ in the category $\BB_{i-1}$. We will denote as $\inj_1^i : X \to X \oplus L_0^iY$ (resp. $\inj_2^i : L_0^iY \to X \oplus L_0^iY$) the first (resp. second) injector of the coproduct of $\BB_i$. For every morphism $f : X \to Z$ and $g : L_0^iY \to Z$, we will denote with $\{f;g\}$ the unique morphism from $X \oplus L_0^iY$ to $Z$ such that $\{f;g\} \circ \inj^i_1 = f$ and $\{f;g\} \circ \inj^i_2 = g$.
|
||||
|
||||
\begin{remark}
|
||||
This adjunction and the existence of a coproduct comes from seeing $\BB_i$ being a category of algebras in $\BB_{i-1}$ over the morphism $inj_1 : G_{i-1}O_i \to G_{i-1}O_i \oplus L_0^{i-1} y\UU$.
|
||||
This adjunction and the existence of a coproduct comes from seeing $\BB_i$ being a category of algebras in $\BB_{i-1}$ over the morphism $inj_1 : G_{i-1}O_i \to G_{i-1}O_i \oplus L_0^{i-1} y\UU$. \inlinetodo{Ça ne marche plus du coup :/}
|
||||
\end{remark}
|
||||
|
||||
|
||||
\subsection{Some Hypotheses}
|
||||
\subsection{Induction Hypotheses}
|
||||
|
||||
In order to build and prove the adjunction, we will state some recurrence invariants that we will prove after having built objects.
|
||||
|
||||
\begin{property}[H1]
|
||||
|
||||
The canonical morphism
|
||||
\[
|
||||
\simpleArrow{R_{i-1}^i X \oplus L_0^{i-1} Y}{\left\{R_{i-1}^i \inj_1^i ; R_{i-1}^i \inj_2^i \circ \eta_{i-1}^i\right\}}{R_{i-1}^i(X \oplus_i L_0^i Y)}
|
||||
\]
|
||||
is an isomorphism.
|
||||
that we will denote as $\en_{i-1}^i$ is an isomorphism.
|
||||
|
||||
Its recursive version is the following isomorphism
|
||||
Its recursive version is the following isomorphism, denoted as $\en_0^i$
|
||||
\[
|
||||
\simpleArrow{ R_{0}^i X \oplus_0 Y}{\left\{R_0^i \inj_1^i ; R_0^i \inj_2^i \circ \eta_0^i\right\}}{R_0^i(X \oplus_i L_0^i Y)}
|
||||
\]
|
||||
@ -266,6 +314,8 @@
|
||||
\simpleArrow{\Hom(G_i O, X)}{(inj_1^i \circ \dash)}{\Hom(G_i O,X \oplus L_0^i Y)}
|
||||
\]
|
||||
|
||||
\todo{Du coup techniquement, c'est une propriété de $H_i$. Faut réussir que c'est \emph{parce que} $H_i$ est représentable que l'on peut déduire H3' de H3.}
|
||||
|
||||
\end{property}
|
||||
|
||||
\subsection{Constructing the functors}
|
||||
@ -279,33 +329,26 @@
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
|
||||
\todo{$G_{i-1} \times \id$ et son compère, c'est bien legit ?}
|
||||
|
||||
The first part $G_{i-1} \times \id \dashv F_{i-1} \times \id$ is proven and defined as an adjunction from the previous step of the recurrence.
|
||||
|
||||
|
||||
\subsubsection{W definition}
|
||||
|
||||
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}$
|
||||
We define a functor $W : \left(X : \BB_{i-1}\right) \times \Set/H_i(F_{i-1}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}O_i,\dash)}(X,Y), \widetilde{\inj_2} \right)
|
||||
W(X,Y) := \left(X \oplus L_0^{i-1} \Hbar_{H_iF_{i-1}}(X,Y), \widetilde{\inj_2} \right)
|
||||
\]
|
||||
|
||||
Where $\Hbar_A$ is a functor $(X:C) \times (\Set/A(X)) \to \TSet$ defined as
|
||||
\[
|
||||
\Hbar_X(X,(Y,f)) = \TSetObject{Y}{f}{A(X)}
|
||||
\]
|
||||
The morphisms are translated as-is.
|
||||
|
||||
\begin{remark}
|
||||
This functor can be constructed as a lax colimit seeing elements of $A(X)/\Set$ as lax cocones over the diagram $\left[1 \xrightarrow{A(X)} \Set\right]$ in $\Cat$, and seeing elements of $\TSet$ as lax cocones over the diagram with no arrow $\left[\Set \quad \Set\right]$. \inlinetodo{Vérifier ça}
|
||||
\end{remark}
|
||||
|
||||
With $\widetilde{\inj_2}$ being defined by \inlinetodo{Changer les noms des hypothèses H3' et H1r}
|
||||
\[
|
||||
\begin{array}{lcl}
|
||||
\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 \\
|
||||
H_iF_{i-1}(X \oplus L_0^{i-1} \Hbar_\bullet(X,Y)))
|
||||
& \to^{\text{H3'}} & H_i(F_{i-1}X)\\
|
||||
& = & \left(\Hbar_{H_iF_{i-1}}(X,Y)\right)_\UU \\
|
||||
& \to^{\inj_2^0} & \left(R_0^{i-1}X \oplus \Hbar_\bullet(X,Y)\right)_\UU \\
|
||||
& \to^{\text{H1r}} & \left(R_0^{i-1}(X \oplus L_0^{i-1}\Hbar_\bullet(X,Y))\right)_\UU
|
||||
\end{array}
|
||||
@ -313,7 +356,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}O_i,\dash)}(g,h)\right)
|
||||
W(g,h) := \left(g \oplus L_0^{i-1} \Hbar_{H_iF_{i-1}}(g,h)\right)
|
||||
\]
|
||||
|
||||
It is indeed a morphism from $\BB_{i}$ as it makes the following diagram commute.
|
||||
@ -327,7 +370,7 @@
|
||||
|
||||
\subsubsection{E definition}
|
||||
|
||||
We define $E : \BB_{i} \to \left(X : \BB_{i-1}\right) \times (\Set/\Hom_{\BB_{i-1}}(G_{i-1}O_i,X))$
|
||||
We define $E : \BB_{i} \to \left(X : \BB_{i-1}\right) \times (\Set/H_iF_{i-1}X)$
|
||||
|
||||
The action on objects is
|
||||
\[
|
||||
@ -351,12 +394,11 @@
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
|
||||
|
||||
\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}O_i,X))$ and $Z$ in $\BB_i$, an isomorphism $\phi_{XYZ}$.
|
||||
We want to construct for each $(X,Y)$ in $(X : \BB_{i-1}) \times (\Set/H_iF_{i-1}X)$ and $Z$ in $\BB_i$, an isomorphism $\phi_{XYZ}$.
|
||||
|
||||
\[
|
||||
\phi_{XYZ} : \Hom(W(X,Y),Z) \to \Hom((X,Y),E(Z))
|
||||
@ -431,7 +473,10 @@
|
||||
|
||||
The constructor goes as follows:
|
||||
\[
|
||||
\Hom_{\BB_{i-1}}(G_{i-1}\Gamma_i,R_{i-1}^i X \oplus_{i-1} L_0^{i-1} Y) \equiv \Hom_{\BB_{i-1}}(G_{i-1}\Gamma_i,R_{i-1}^i X) \to (R_0^{i-1} X)_\UU \to (R_0^i (R_{i-1}^i X \oplus_{i-1} L_0^{i-1} Y))_\UU
|
||||
H_iF_{i-1}(R_{i-1}^i X \oplus_{i-1} L_0^{i-1} Y) \equiv
|
||||
H_iF_{i-1}(R_{i-1}^i X) \to
|
||||
(R_0^{i-1} X)_\UU \to
|
||||
(R_0^i (R_{i-1}^i X \oplus_{i-1} L_0^{i-1} Y))_\UU
|
||||
\]
|
||||
|
||||
The first injector $X \to X \oplus_i L_0^i Y$ is defined as follows:
|
||||
@ -456,7 +501,7 @@
|
||||
|
||||
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$.
|
||||
This goes from $L_0^i Y = L_{i-1}^i L_0^{i-1} Y$ to $L_{i-1}^i(R_{i-1}^i X \oplus_{i-1} L_0^{i-1} Y)$, which is equivalent to $L_{i-1}^i R_{i-1}^i X \oplus_i L_0^i Y)$ as $L_{i-1}^i$ is a left-adjoint functor and therefore it preserves colimits; then goes to $X \oplus_i L_0^i Y$.
|
||||
|
||||
We will now show that this definition is actually a definition of the coproduct in $\BB_i$.
|
||||
To that extent, we take two objects $X$ and $Z$ in $\BB_i$, $Y$ in $\TSet$ and two morphisms of $\BB_i$ $\varphi_1 : X \to Z$ and $\varphi_2 : L_0^i Y \to Z$.
|
||||
@ -759,3 +804,23 @@
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
@ -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":1,"id":4,"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":5,"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":6,"label":{"isPullshout":false,"label":"\\Delta","style":{"alignment":"right","bend":0.20000000000000004,"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}},{"id":3,"label":{"isMath":true,"label":"\\circlearrowleft","pos":[302,76.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":1,"id":4,"label":{"kind":"normal","label":"\\Gamma","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":2,"id":5,"label":{"kind":"normal","label":"A","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":2,"id":6,"label":{"kind":"normal","label":"\\Delta","style":{"alignment":"right","bend":0.20000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","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}},{"id":3,"label":{"isMath":true,"label":"\\circlearrowleft","pos":[302,76.8125],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12}
|
||||
@ -1 +1 @@
|
||||
{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}\n\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}","tabs":[{"active":true,"edges":[{"from":0,"id":4,"label":{"kind":"normal","label":"\\Cstr^X","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":5,"label":{"kind":"normal","label":"R_0^{i-1} X_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":6,"label":{"kind":"normal","label":"f \\circ \\dash","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":7,"label":{"kind":"normal","label":"\\Cstr^{X'}","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\Hom_{\\BB_{i-1}}(G_{i-1}O_i,X)","pos":[180,60],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"(R_0^{i-1} X)_\\UU","pos":[450,60],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^{i-1} X')_\\UU","pos":[450,143],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\Hom_{\\BB_{i-1}}(G_{i-1}O_i,X')","pos":[180,143],"zindex":-10000}}],"sizeGrid":120,"title":"1"}]},"version":12}
|
||||
{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}\n\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}","tabs":[{"active":true,"edges":[{"from":0,"id":4,"label":{"kind":"normal","label":"\\Cstr^X","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":5,"label":{"kind":"normal","label":"R_0^{i-1} X_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":6,"label":{"kind":"normal","label":"f \\circ \\dash","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":7,"label":{"kind":"normal","label":"\\Cstr^{X'}","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2}],"nodes":[{"id":0,"label":{"isMath":true,"label":"H_i(F_{i-1}X)","pos":[180,60],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"(R_0^{i-1} X)_\\UU","pos":[450,60],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^{i-1} X')_\\UU","pos":[450,143],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_i(F_{i-1}X')","pos":[180,143],"zindex":-10000}}],"sizeGrid":120,"title":"1"}]},"version":12}
|
||||
@ -1 +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}
|
||||
{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":4,"label":{"kind":"normal","label":"\\phi_{XYZ}","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":"E(f) \\circ \\dash \\circ (g,h)","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":6,"label":{"kind":"normal","label":"f \\circ \\dash \\circ W(g,h)","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":7,"label":{"kind":"normal","label":"\\phi_{X'Y'Z'}","style":{"alignment":"left","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":"\\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":12}
|
||||
@ -1 +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}
|
||||
{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":10,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":true,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":11,"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":12,"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":13,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":4,"id":14,"label":{"kind":"normal","label":"\\Cstr^Z","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":0,"id":15,"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":16,"label":{"kind":"normal","label":"(\\inj_1^{i-1} \\circ \\dash)","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":17,"label":{"kind":"normal","label":"R_{i-1}^i f","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":18,"label":{"kind":"normal","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,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":5,"id":19,"label":{"kind":"normal","label":"\\square_\\UU","style":{"alignment":"right","bend":0.2,"color":"blue","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":5,"id":20,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":7,"id":21,"label":{"kind":"normal","label":"(\\inj_2^0)_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":8},{"from":8,"id":22,"label":{"kind":"normal","label":"\\text{H1'}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":9},{"from":9,"id":23,"label":{"kind":"normal","label":"(R_0^i f)_\\UU","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":6,"id":24,"label":{"kind":"normal","label":"\\Cstr^{W(X,Y)}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":9},{"from":13,"id":25,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","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":12}
|
||||
File diff suppressed because one or more lines are too long
@ -1 +1 @@
|
||||
{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}\n\\newcommand{\\ensuremath}[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\\newcommand{\\inj}{\\operatorname{inj}}\n\\newcommand{\\idr}{\\operatorname{id}}\n","tabs":[{"active":true,"edges":[{"from":0,"id":10,"label":{"kind":"normal","label":"\\text{H3'}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":-1},"to":1},{"from":2,"id":11,"label":{"kind":"normal","label":"\\inj_2^0","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":12,"label":{"kind":"normal","label":"\\text{H1r}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":4,"id":13,"label":{"kind":"normal","label":"R_0^i(g \\oplus L_0^{i-1}\\Hbar_\\bullet(g,h))_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":3,"id":14,"label":{"kind":"normal","label":"(R_0^i g \\oplus \\Hbar(g,h))_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":6,"id":15,"label":{"kind":"normal","label":"\\text{H1r}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":2,"id":16,"label":{"kind":"normal","label":"\\left[\\Hbar_\\bullet(g,h)\\right]_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":1,"id":17,"label":{"kind":"normal","label":"g \\circ \\dash","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":8},{"from":8,"id":18,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":0,"id":19,"label":{"kind":"normal","label":"(g \\oplus L_0^{i-1}\\Hbar_\\bullet(g,h)) \\circ \\dash","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":9},{"from":9,"id":20,"label":{"kind":"normal","label":"H3'","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":8},{"from":7,"id":21,"label":{"kind":"normal","label":"\\inj_2^0","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":1,"id":22,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":2}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\Hom(G_{i-1}O_i,X \\oplus L_0^{i-1}\\Hbar_\\bullet(X,Y))","pos":[306,72],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\Hom(G_{i-1}O_i,X)","pos":[570,72],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\left[\\Hbar_\\bullet(X,Y)\\right]_\\UU","pos":[722,72],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\left[R_0^{i-1} X \\oplus \\Hbar_\\bullet(X,Y)\\right]_\\UU","pos":[956,72],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"R_0^{i-1}(X \\oplus L_0^{i-1} \\Hbar_\\bullet(X,Y))_\\UU","pos":[1234,72],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"R_0^{i-1}(X' \\oplus L_0^{i-1} \\Hbar_\\bullet(X',Y'))_\\UU","pos":[1234,230],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"\\left[R_0^{i-1} X' \\oplus \\Hbar_\\bullet(X',Y')\\right]_\\UU","pos":[956,230],"zindex":-10000}},{"id":7,"label":{"isMath":true,"label":"\\left[\\Hbar_\\bullet(X',Y')\\right]_\\UU","pos":[722,230],"zindex":0}},{"id":8,"label":{"isMath":true,"label":"\\Hom(G_{i-1}O_i,X')","pos":[570,230],"zindex":0}},{"id":9,"label":{"isMath":true,"label":"\\Hom(G_{i-1}O_i,X' \\oplus L_0^{i-1}\\Hbar_\\bullet(X',Y'))","pos":[306,230],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12}
|
||||
{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}\n\\newcommand{\\ensuremath}[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\\newcommand{\\inj}{\\operatorname{inj}}\n\\newcommand{\\idr}{\\operatorname{id}}\n","tabs":[{"active":true,"edges":[{"from":0,"id":10,"label":{"kind":"normal","label":"\\text{H3'}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":-1},"to":1},{"from":2,"id":11,"label":{"kind":"normal","label":"\\inj_2^0","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":12,"label":{"kind":"normal","label":"\\text{H1r}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":4,"id":13,"label":{"kind":"normal","label":"R_0^i(g \\oplus L_0^{i-1}\\Hbar_\\bullet(g,h))_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":3,"id":14,"label":{"kind":"normal","label":"(R_0^i g \\oplus \\Hbar_\\bullet(g,h))_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":6,"id":15,"label":{"kind":"normal","label":"\\text{H1r}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":2,"id":16,"label":{"kind":"normal","label":"\\left[\\Hbar_\\bullet(g,h)\\right]_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":1,"id":17,"label":{"kind":"normal","label":"g \\circ \\dash","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":8},{"from":8,"id":18,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":0,"id":19,"label":{"kind":"normal","label":"H_iF_{i-1}(g \\oplus L_0^{i-1}\\Hbar_\\bullet(g,h))","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":9},{"from":9,"id":20,"label":{"kind":"normal","label":"H3'","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":8},{"from":7,"id":21,"label":{"kind":"normal","label":"\\inj_2^0","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":1,"id":22,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":2}],"nodes":[{"id":0,"label":{"isMath":true,"label":"H_iF_{i-1}(X \\oplus L_0^{i-1}\\Hbar_\\bullet(X,Y))","pos":[306,72],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"H_iF_{i-1}(X)","pos":[530,72],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\left[\\Hbar_\\bullet(X,Y)\\right]_\\UU","pos":[682,72],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\left[R_0^{i-1} X \\oplus \\Hbar_\\bullet(X,Y)\\right]_\\UU","pos":[916,72],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"R_0^{i-1}(X \\oplus L_0^{i-1} \\Hbar_\\bullet(X,Y))_\\UU","pos":[1194,72],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"R_0^{i-1}(X' \\oplus L_0^{i-1} \\Hbar_\\bullet(X',Y'))_\\UU","pos":[1194,230],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"\\left[R_0^{i-1} X' \\oplus \\Hbar_\\bullet(X',Y')\\right]_\\UU","pos":[916,230],"zindex":-10000}},{"id":7,"label":{"isMath":true,"label":"\\left[\\Hbar_\\bullet(X',Y')\\right]_\\UU","pos":[682,230],"zindex":0}},{"id":8,"label":{"isMath":true,"label":"H_iF_{i-1}(X')","pos":[530,230],"zindex":0}},{"id":9,"label":{"isMath":true,"label":"H_iF_{i-1}(X' \\oplus L_0^{i-1}\\Hbar_\\bullet(X',Y'))","pos":[306,230],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12}
|
||||
@ -1 +1 @@
|
||||
{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":4,"label":{"kind":"normal","label":"h","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":0,"id":5,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":6,"label":{"kind":"normal","label":"R_0^i(X)_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":1,"id":7,"label":{"kind":"normal","label":"\\Cstr^X_i","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3}],"nodes":[{"id":0,"label":{"isMath":true,"label":"A","pos":[100,117.8125],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\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}
|
||||
{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":4,"label":{"kind":"normal","label":"h","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":0,"id":5,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":6,"label":{"kind":"normal","label":"R_0^i(X)_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":1,"id":7,"label":{"kind":"normal","label":"\\Cstr^X_i","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3}],"nodes":[{"id":0,"label":{"isMath":true,"label":"A","pos":[100,117.8125],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"H_iF_{i-1}(R_{i-1}^i X)","pos":[100,195.8125],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"R_0^i(X)_\\El","pos":[358,117.8125],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"R_0^i(X)_\\UU","pos":[358,195.8125],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12}
|
||||
@ -1 +1 @@
|
||||
{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":8,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":9,"label":{"kind":"normal","label":"R_0^i(X)_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":10,"label":{"kind":"normal","label":"h","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.30000000000000004,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":11,"label":{"kind":"normal","label":"\\Cstr^X_i","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":4,"id":12,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":5,"id":13,"label":{"kind":"normal","label":"R_0^i(X')_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":4,"id":14,"label":{"kind":"normal","label":"h'","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.30000000000000004,"tail":"none"},"zindex":0},"to":7},{"from":7,"id":15,"label":{"kind":"normal","label":"\\Cstr^{X'}_i","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":0,"id":16,"label":{"kind":"normal","label":"!","style":{"alignment":"left","bend":0,"color":"black","dashed":true,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":1},"to":4},{"from":1,"id":17,"label":{"kind":"normal","label":"R_0^i(f)_\\El","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":3,"id":18,"label":{"kind":"normal","label":"\\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}
|
||||
{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":8,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":9,"label":{"kind":"normal","label":"R_0^i(X)_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":10,"label":{"kind":"normal","label":"h","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.30000000000000004,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":11,"label":{"kind":"normal","label":"\\Cstr^X_i","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":4,"id":12,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":5,"id":13,"label":{"kind":"normal","label":"R_0^i(X')_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":4,"id":14,"label":{"kind":"normal","label":"h'","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.30000000000000004,"tail":"none"},"zindex":0},"to":7},{"from":7,"id":15,"label":{"kind":"normal","label":"\\Cstr^{X'}_i","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":0,"id":16,"label":{"kind":"normal","label":"!","style":{"alignment":"left","bend":0,"color":"black","dashed":true,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":1},"to":4},{"from":1,"id":17,"label":{"kind":"normal","label":"R_0^i(f)_\\El","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":3,"id":18,"label":{"kind":"normal","label":"H_iF_{i-1}R_{i-1}^i f","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.10000000000000003,"tail":"none"},"zindex":0},"to":7},{"from":2,"id":19,"label":{"kind":"normal","label":"R_0^i(f)_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.6,"tail":"none"},"zindex":0},"to":6},{"from":14,"id":20,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":12},{"from":10,"id":21,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":8}],"nodes":[{"id":0,"label":{"isMath":true,"label":"A","pos":[125,115],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"R_0^i(X)_\\El","pos":[403,115],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"R_0^i(X)_\\UU","pos":[403,297],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}(R_{i-1}^i X)","pos":[125,297],"zindex":-10000}},{"id":4,"label":{"isMath":true,"label":"A'","pos":[249,190.8125],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"R_0^i(X')_\\El","pos":[521,190.8125],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"R_0^i(X')_\\UU","pos":[521,372.8125],"zindex":0}},{"id":7,"label":{"isMath":true,"label":"H_iF_{i-1}(R_{i-1}^i X')","pos":[249,372.8125],"zindex":-10000}}],"sizeGrid":250,"title":"1"}]},"version":12}
|
||||
@ -1 +1 @@
|
||||
{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":6,"label":{"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}
|
||||
{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":6,"label":{"kind":"normal","label":"\\Cstr^X","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":7,"label":{"kind":"normal","label":"(R_0^{i-1} (\\inj_1^{i-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":8,"label":{"kind":"normal","label":"H_iF_{i-1}\\inj_1^{i-1}","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":4,"id":9,"label":{"kind":"normal","label":"R_0^{i-1}(\\inj_1^{i-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":3,"id":10,"label":{"kind":"normal","label":"(\\inj_1^{i-1} \\circ \\dash)^{-1}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"normal","position":0.5,"tail":"none"},"zindex":-3},"to":5},{"from":5,"id":11,"label":{"kind":"normal","label":"\\Cstr^X","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":0,"id":12,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":4,"id":13,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":3,"id":14,"label":{"kind":"normal","label":"\\Cstr^{X \\oplus L_0^i Y}","style":{"alignment":"left","bend":0.1,"color":"green","dashed":true,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2}],"nodes":[{"id":0,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i X)","pos":[236.5,73.5],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"(R_0^i X)_\\UU","pos":[1013,73.8125],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^{i-1} (R_{i-1}^i X \\oplus L_0^{i-1} Y))_\\UU","pos":[1017.5,249.5],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}(R_{i-1}^i X \\oplus_{i-1} L_0^{i-1} Y)","pos":[236.5,249.5],"zindex":-10000}},{"id":4,"label":{"isMath":true,"label":"(R_0^i X)_\\UU","pos":[706,235.8125],"zindex":-10000}},{"id":5,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i X","pos":[556,234.8125],"zindex":-10000}}],"sizeGrid":147,"title":"1"}]},"version":12}
|
||||
@ -1 +1 @@
|
||||
{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":6,"label":{"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}
|
||||
{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":6,"label":{"kind":"normal","label":"H_iF_{i-1}\\inj^{i-1}_1","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":7,"label":{"kind":"normal","label":"\\Cstr^X","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":8,"label":{"kind":"normal","label":"H_iF_{i-1}\\{\\varphi_1 ; \\varphi_2\\}","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":2,"id":9,"label":{"kind":"normal","label":"(R_0^{i-1} \\inj_1^{i-1})_\\UU","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.6,"tail":"none"},"zindex":-1},"to":4},{"from":4,"id":10,"label":{"kind":"normal","label":"(R_0^i \\{\\varphi_1;\\varphi_2\\})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":3,"id":11,"label":{"kind":"normal","label":"\\Cstr^Z","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":1,"id":12,"label":{"kind":"normal","label":"R_{i-1}^i \\varphi_1 \\circ \\dash","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":2,"id":13,"label":{"kind":"normal","label":"(R_0^i \\varphi_1)_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5}],"nodes":[{"id":0,"label":{"isMath":true,"label":"H_iF_{i-1}(R_{i-1}^i X \\oplus L_0^{i-1} Y)","pos":[225,75],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i X","pos":[477,75],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i X)_\\UU","pos":[571,142.8125],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i Z","pos":[225,365],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"(R_0^{i-1} (R_{i-1}^i X \\oplus L_0^{i-1} Y))_\\UU","pos":[777,75],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[777,365],"zindex":0}}],"sizeGrid":150,"title":"1"}]},"version":12}
|
||||
@ -1 +1 @@
|
||||
{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":6,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":7,"label":{"kind":"normal","label":"(R_0^i Z)_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":8,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":9,"label":{"kind":"normal","label":"\\Cstr^Z","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":4,"id":10,"label":{"kind":"normal","label":"h","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":5,"id":11,"label":{"kind":"normal","label":"\\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}
|
||||
{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":6,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":7,"label":{"kind":"normal","label":"(R_0^i Z)_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":8,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":9,"label":{"kind":"normal","label":"\\Cstr^Z","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":4,"id":10,"label":{"kind":"normal","label":"h","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":5,"id":11,"label":{"kind":"normal","label":"H_iF_{i-1}(R_{i-1}^i f \\circ \\inj_1)","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.10000000000000003,"tail":"hook"},"zindex":8},"to":3},{"from":4,"id":12,"label":{"kind":"normal","label":"\\left[R_{i-1}^i f \\circ \\inj_2\\right]_\\El","style":{"alignment":"left","bend":-0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":4,"id":13,"label":{"kind":"normal","label":"\\phi_{XYZ}(f)_2","style":{"alignment":"left","bend":0,"color":"black","dashed":true,"head":"default","kind":"normal","position":0.6,"tail":"none"},"zindex":0},"to":0}],"nodes":[{"id":0,"label":{"isMath":true,"label":"E(z)","pos":[290,174],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"(R_0^i Z)_\\El","pos":[490,174],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[490,304],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i Z","pos":[290,304],"zindex":-10000}},{"id":4,"label":{"isMath":true,"label":"A","pos":[100,100],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"H_iF_{i-1}X","pos":[101,224.8125],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12}
|
||||
@ -1 +1 @@
|
||||
{"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}
|
||||
{"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":"H_iF_{i-1}g","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":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":"H_iF_{i-1}R_{i-1}^i Z","pos":[390,234],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"H_iF_{i-1}X","pos":[130,234],"zindex":-10000}}],"sizeGrid":260,"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\\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}
|
||||
{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":8,"label":{"kind":"normal","label":"\\text{H3'}","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.30000000000000004,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":9,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":10,"label":{"kind":"normal","label":"\\inj_2^0","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":11,"label":{"kind":"normal","label":"\\text{H1r}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":4,"id":12,"label":{"kind":"normal","label":"R_0^{i-1}\\left\\{g;\\eta_0^i \\circ L_0^{i-1} \\square \\right\\}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":2,"id":13,"label":{"kind":"normal","label":"(\\varepsilon_0^{i-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":6,"id":14,"label":{"kind":"normal","label":"(R_0^{i-1} \\inj_2^{i-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":6,"id":15,"label":{"kind":"normal","label":"R_0^{i-1}(\\eta_0^i \\circ L_0^{i-1} \\square)_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.7,"tail":"none"},"zindex":0},"to":5},{"from":2,"id":16,"label":{"kind":"normal","label":"\\Cstr^Z \\circ H_iF_{i-1}g","style":{"alignment":"right","bend":0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.30000000000000004,"tail":"none"},"zindex":0},"to":5},{"from":0,"id":17,"label":{"kind":"normal","label":"H_iF_{i-1}\\left\\{g;\\eta_0^i \\circ L_0^{i-1} \\square \\right\\}","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":7,"id":18,"label":{"kind":"normal","label":"\\Cstr^Z","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":1,"id":19,"label":{"kind":"normal","label":"H_iF_{i-1}g","style":{"alignment":"left","bend":0,"color":"red","dashed":false,"head":"default","kind":"normal","position":0.4,"tail":"none"},"zindex":0},"to":7}],"nodes":[{"id":0,"label":{"isMath":true,"label":"H_iF_{i-1}(X \\oplus L_0^{i-1}\\Hbar_\\bullet(X,Y))","pos":[210,64],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"H_iF_{i-1}X","pos":[329,129.8125],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\Hbar(X,Y)_\\UU","pos":[410,64.8125],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\left[R_0^{i-1} X \\oplus \\Hbar(X,Y)\\right]_\\UU","pos":[604.9999999999999,61.8125],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"R_0^{i-1}\\left(X \\oplus L_0^{i-1}\\Hbar(X,Y)\\right)","pos":[853,61.8125],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[853,303.8125],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"\\left[R_0^{i-1}L_0^{i-1}\\Hbar(X,Y)\\right]_\\UU","pos":[688,198.625],"zindex":0}},{"id":7,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i Z","pos":[210,306],"zindex":0}}],"sizeGrid":140,"title":"1"}]},"version":12}
|
||||
@ -1 +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}
|
||||
{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":1,"id":6,"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":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":3},{"from":1,"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":4},{"from":4,"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":3},{"from":0,"id":10,"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":11,"label":{"kind":"normal","label":"\\dash \\circ g","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":0,"id":12,"label":{"kind":"normal","label":"(\\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,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":13,"label":{"kind":"normal","label":"h","style":{"alignment":"left","bend":0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":0,"id":14,"label":{"kind":"normal","label":"\\phi_{XYZ}(\\phi^{-1}_{XYZ}(g,h))_2","style":{"alignment":"left","bend":-0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.7,"tail":"none"},"zindex":0},"to":1},{"from":8,"id":15,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":6}],"nodes":[{"id":0,"label":{"isMath":true,"label":"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":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\\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}
|
||||
{"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":{"kind":"normal","label":"p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":0}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\UU","pos":[100,178],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\El","pos":[100,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\\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":"F","style":{"alignment":"right","bend":0.20000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":4,"label":{"kind":"normal","label":"G","style":{"alignment":"right","bend":0.20000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":2,"id":5,"label":{"kind":"normal","label":"L","style":{"alignment":"right","bend":0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":0,"id":6,"label":{"kind":"normal","label":"R","style":{"alignment":"right","bend":0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":3,"id":7,"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":4},{"from":6,"id":8,"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}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\BB","pos":[300,100],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\CC","pos":[500,100],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\TSet","pos":[300,300],"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\\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":"F","style":{"alignment":"right","bend":0.20000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":4,"label":{"kind":"normal","label":"G","style":{"alignment":"right","bend":0.20000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":2,"id":5,"label":{"kind":"normal","label":"L","style":{"alignment":"right","bend":0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":0,"id":6,"label":{"kind":"normal","label":"R","style":{"alignment":"right","bend":0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":3,"id":7,"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":4},{"from":6,"id":8,"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}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\BB","pos":[300,100],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\CC","pos":[486,100],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\BB_0","pos":[300,174],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12}
|
||||
File diff suppressed because one or more lines are too long
@ -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":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}
|
||||
{"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/H_iX\\right.","pos":[386,74],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\left(X : \\BB_{i-1}\\right) \\times \\left.\\Set\\middle/H_iF_{i-1}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,4 +1,10 @@
|
||||
% Loading packages
|
||||
\usepackage[utf8]{inputenc}
|
||||
\usepackage{ae}
|
||||
\usepackage[T1]{fontenc}
|
||||
\usepackage{fontspec}
|
||||
\usepackage{alphabeta}
|
||||
\usepackage{polyglossia}
|
||||
\usepackage{hyperref}
|
||||
\usepackage{bookmark}
|
||||
\hypersetup{
|
||||
@ -11,7 +17,6 @@
|
||||
\usepackage{amssymb}
|
||||
\usepackage{bbm}
|
||||
\usepackage{stmaryrd}
|
||||
\usepackage[main=english]{babel}
|
||||
\usepackage{csquotes}
|
||||
\usepackage{listings}
|
||||
\usepackage{lstautogobble}
|
||||
@ -38,6 +43,7 @@
|
||||
\usepackage{pdfpages}
|
||||
\usepackage{lipsum}
|
||||
\usepackage{newunicodechar}
|
||||
\usepackage{txfonts}
|
||||
\usepackage{yade}
|
||||
|
||||
\usepackage[textheight=0.75\paperheight]{geometry}
|
||||
@ -98,8 +104,9 @@
|
||||
|
||||
|
||||
% Macros caractères spécifiques au document
|
||||
\newunicodechar{λ}{{\lambda}}
|
||||
\newfontface\russian{Liberation Serif}
|
||||
\newcommand\BB{{\ensuremath{\mathcal{B}}}}
|
||||
\newcommand\en{{\text{\russian н}}}
|
||||
\newcommand\TT{{\ensuremath{\mathcal{T}}}}
|
||||
\newcommand\UU{{\ensuremath{\mathcal{U}}}}
|
||||
\newcommand\CC{{\ensuremath{\mathcal{C}}}}
|
||||
|
||||
324
Report/yade.sty
324
Report/yade.sty
@ -46,13 +46,13 @@
|
||||
\tikzset{curve/.style={settings={#1},to path={
|
||||
let \p1 = ($(\tikztostart) - (\tikztotarget)$) in
|
||||
(\tikztostart)
|
||||
.. controls
|
||||
($(\tikztostart)!\pv{pos}!(\tikztotarget)!{veclen(\x1,\y1)*\pv{ratio}*0.65pt}!270:(\tikztotarget)$)
|
||||
and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!{veclen(\x1,\y1)*\pv{ratio}*0.65pt}!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}
|
||||
.. controls
|
||||
($(\tikztostart)!\pv{pos}!(\tikztotarget)!{veclen(\x1,\y1)*\pv{ratio}*0.65pt}!270:(\tikztotarget)$)
|
||||
and ($(\tikztostart)!1-\pv{pos}!(\tikztotarget)!{veclen(\x1,\y1)*\pv{ratio}*0.65pt}!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) {} ; %
|
||||
@ -81,21 +81,21 @@
|
||||
\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$}}}}
|
||||
\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$}}}}
|
||||
\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$}}}}
|
||||
\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$}}}}
|
||||
\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$}}}}
|
||||
\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$}}}}
|
||||
\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$}}}}
|
||||
\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$}}}}
|
||||
\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
|
||||
|
||||
@ -281,7 +281,7 @@
|
||||
\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}%
|
||||
\inetatom(#1){#2}%
|
||||
}
|
||||
|
||||
\newcommand{\gimpll}{\ssf{Rien}{\impll}}
|
||||
@ -315,76 +315,76 @@
|
||||
}
|
||||
|
||||
\tikzset{
|
||||
mod/.style={postaction={
|
||||
decorate,
|
||||
decoration={
|
||||
markings,
|
||||
mark=at position .5 with {
|
||||
\path[draw,-] (0,-3pt) -- (0,3pt);
|
||||
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 ;}
|
||||
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$} ;}
|
||||
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$} ;}
|
||||
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$} ;}
|
||||
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 ;}
|
||||
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$} ;}
|
||||
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$} ;}
|
||||
labelonat/.style 2 args={postaction={
|
||||
decorate,
|
||||
decoration={
|
||||
markings,
|
||||
mark=at position #2 with {\node[inner sep=0.1pt,fill=white] {$\scriptstyle #1$} ;}
|
||||
}}}}
|
||||
|
||||
\tikzset{
|
||||
labelonatsloped/.style 2 args={postaction={
|
||||
decorate,
|
||||
decoration={
|
||||
markings,
|
||||
mark=at position #2 with {\node[inner sep=0.1pt,fill=white,transform shape] {#1} ;}
|
||||
labelonatsloped/.style 2 args={postaction={
|
||||
decorate,
|
||||
decoration={
|
||||
markings,
|
||||
mark=at position #2 with {\node[inner sep=0.1pt,fill=white,transform shape] {#1} ;}
|
||||
}}}}
|
||||
|
||||
|
||||
@ -394,18 +394,18 @@
|
||||
\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}}
|
||||
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}}
|
||||
{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},%
|
||||
{nodes={inner sep=1pt,outer sep=0pt},%
|
||||
ampersand replacement=\&,%
|
||||
row sep={#1 cm,between origins}, %
|
||||
column sep={#2 cm,between origins}%
|
||||
@ -416,9 +416,9 @@
|
||||
\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} }}
|
||||
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}, %
|
||||
@ -426,156 +426,156 @@
|
||||
inner sep=-.1ex}} %
|
||||
|
||||
\tikzset{
|
||||
two/.style 2 args={postaction={
|
||||
decorate,
|
||||
decoration={
|
||||
markings,
|
||||
mark=at position .5 with \node (#1) [#2] {} ;
|
||||
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) {} ;
|
||||
twocenter/.style={postaction={
|
||||
decorate,
|
||||
decoration={
|
||||
markings,
|
||||
mark=at position .5 with \node (#1) {} ;
|
||||
}}}}
|
||||
|
||||
\tikzset{
|
||||
twoon/.style 2 args={twocenter={#1},label={{$\scriptstyle #2$}}}
|
||||
twoon/.style 2 args={twocenter={#1},label={{$\scriptstyle #2$}}}
|
||||
}
|
||||
\tikzset{
|
||||
twoo/.style={two={on},label={{$\scriptstyle #1$}}}
|
||||
twoo/.style={two={on},label={{$\scriptstyle #1$}}}
|
||||
}
|
||||
\tikzset{
|
||||
twol/.style={two={l}{right},label={[left]{$\scriptstyle #1$}}}
|
||||
twol/.style={two={l}{right},label={[left]{$\scriptstyle #1$}}}
|
||||
}
|
||||
\tikzset{
|
||||
twoleft/.style 2 args={two={#1}{right},label={[left]{$\scriptstyle #2$}}}
|
||||
twoleft/.style 2 args={two={#1}{right},label={[left]{$\scriptstyle #2$}}}
|
||||
}
|
||||
\tikzset{
|
||||
twor/.style={two={r}{left},label={[right]{$\scriptstyle #1$}}}
|
||||
twor/.style={two={r}{left},label={[right]{$\scriptstyle #1$}}}
|
||||
}
|
||||
\tikzset{
|
||||
tworight/.style 2 args={two={#1}{left},label={[right]{$\scriptstyle #2$}}}
|
||||
tworight/.style 2 args={two={#1}{left},label={[right]{$\scriptstyle #2$}}}
|
||||
}
|
||||
\tikzset{
|
||||
twou/.style={two={u}{below},label={[above]{$\scriptstyle #1$}}}
|
||||
twou/.style={two={u}{below},label={[above]{$\scriptstyle #1$}}}
|
||||
}
|
||||
\tikzset{
|
||||
twoa/.style={two={a}{below},label={[above]{$\scriptstyle #1$}}}
|
||||
twoa/.style={two={a}{below},label={[above]{$\scriptstyle #1$}}}
|
||||
}
|
||||
\tikzset{
|
||||
twoup/.style 2 args={two={#1}{below},label={[above]{$\scriptstyle #2$}}}
|
||||
twoup/.style 2 args={two={#1}{below},label={[above]{$\scriptstyle #2$}}}
|
||||
}
|
||||
\tikzset{
|
||||
twoabove/.style 2 args={two={#1}{below},label={[above]{$\scriptstyle #2$}}}
|
||||
twoabove/.style 2 args={two={#1}{below},label={[above]{$\scriptstyle #2$}}}
|
||||
}
|
||||
\tikzset{
|
||||
twod/.style={two={d}{above},label={[below]{$\scriptstyle #1$}}}
|
||||
twod/.style={two={d}{above},label={[below]{$\scriptstyle #1$}}}
|
||||
}
|
||||
\tikzset{
|
||||
twob/.style={two={b}{above},label={[below]{$\scriptstyle #1$}}}
|
||||
twob/.style={two={b}{above},label={[below]{$\scriptstyle #1$}}}
|
||||
}
|
||||
\tikzset{
|
||||
twodown/.style 2 args={two={#1}{above},label={[below]{$\scriptstyle #2$}}}
|
||||
twodown/.style 2 args={two={#1}{above},label={[below]{$\scriptstyle #2$}}}
|
||||
}
|
||||
\tikzset{
|
||||
twobelow/.style 2 args={two={#1}{above},label={[below]{$\scriptstyle #2$}}}
|
||||
twobelow/.style 2 args={two={#1}{above},label={[below]{$\scriptstyle #2$}}}
|
||||
}
|
||||
\tikzset{
|
||||
twoal/.style={two={al}{right},label={[above left]{$\scriptstyle #1$}}}
|
||||
twoal/.style={two={al}{right},label={[above left]{$\scriptstyle #1$}}}
|
||||
}
|
||||
\tikzset{
|
||||
twoaboveleft/.style 2 args={two={#1}{above},label={[above left]{$\scriptstyle #2$}}}
|
||||
twoaboveleft/.style 2 args={two={#1}{above},label={[above left]{$\scriptstyle #2$}}}
|
||||
}
|
||||
\tikzset{
|
||||
twoar/.style={two={ar}{left},label={[above right]{$\scriptstyle #1$}}}
|
||||
twoar/.style={two={ar}{left},label={[above right]{$\scriptstyle #1$}}}
|
||||
}
|
||||
\tikzset{
|
||||
twoaboveright/.style 2 args={two={#1}{above},label={[above right]{$\scriptstyle #2$}}}
|
||||
twoaboveright/.style 2 args={two={#1}{above},label={[above right]{$\scriptstyle #2$}}}
|
||||
}
|
||||
\tikzset{
|
||||
twobr/.style={two={br}{left},label={[below right]{$\scriptstyle #1$}}}
|
||||
twobr/.style={two={br}{left},label={[below right]{$\scriptstyle #1$}}}
|
||||
}
|
||||
\tikzset{
|
||||
twobelowright/.style 2 args={two={#1}{left},label={[below right]{$\scriptstyle #2$}}}
|
||||
twobelowright/.style 2 args={two={#1}{left},label={[below right]{$\scriptstyle #2$}}}
|
||||
}
|
||||
\tikzset{
|
||||
twobl/.style={two={bl}{right},label={[below left]{$\scriptstyle #1$}}}
|
||||
twobl/.style={two={bl}{right},label={[below left]{$\scriptstyle #1$}}}
|
||||
}
|
||||
\tikzset{
|
||||
twobelowleft/.style 2 args={two={#1}{right},label={[below left]{$\scriptstyle #2$}}}
|
||||
twobelowleft/.style 2 args={two={#1}{right},label={[below left]{$\scriptstyle #2$}}}
|
||||
}
|
||||
\tikzset{
|
||||
twol/.style={two={l}{right},label={[left]{$\scriptstyle #1$}}}
|
||||
twol/.style={two={l}{right},label={[left]{$\scriptstyle #1$}}}
|
||||
}
|
||||
|
||||
\tikzset{
|
||||
labell/.style={label={[left]{$\scriptstyle #1$}}}
|
||||
labell/.style={label={[left]{$\scriptstyle #1$}}}
|
||||
}
|
||||
\tikzset{
|
||||
labellat/.style 2 args={labelat={[left]{$\scriptstyle #1$}}{#2}}
|
||||
labellat/.style 2 args={labelat={[left]{$\scriptstyle #1$}}{#2}}
|
||||
}
|
||||
\tikzset{
|
||||
labelr/.style={label={[right]{$\scriptstyle #1$}}}
|
||||
labelr/.style={label={[right]{$\scriptstyle #1$}}}
|
||||
}
|
||||
\tikzset{
|
||||
labelrat/.style 2 args={labelat={[right]{$\scriptstyle #1$}}{#2}}
|
||||
labelrat/.style 2 args={labelat={[right]{$\scriptstyle #1$}}{#2}}
|
||||
}
|
||||
\tikzset{
|
||||
labelar/.style={label={[above right]{$\scriptstyle #1$}}}
|
||||
labelar/.style={label={[above right]{$\scriptstyle #1$}}}
|
||||
}
|
||||
\tikzset{
|
||||
labelarat/.style 2 args={labelat={[above right]{$\scriptstyle #1$}}{#2}}
|
||||
labelarat/.style 2 args={labelat={[above right]{$\scriptstyle #1$}}{#2}}
|
||||
}
|
||||
\tikzset{
|
||||
labelbr/.style={label={[below right]{$\scriptstyle #1$}}}
|
||||
labelbr/.style={label={[below right]{$\scriptstyle #1$}}}
|
||||
}
|
||||
\tikzset{
|
||||
labelbrat/.style 2 args={labelat={[below right]{$\scriptstyle #1$}}{#2}}
|
||||
labelbrat/.style 2 args={labelat={[below right]{$\scriptstyle #1$}}{#2}}
|
||||
}
|
||||
\tikzset{
|
||||
labelu/.style={label={[above]{$\scriptstyle #1$}}}
|
||||
labelu/.style={label={[above]{$\scriptstyle #1$}}}
|
||||
}
|
||||
\tikzset{
|
||||
labeluat/.style 2 args={labelat={[above]{$\scriptstyle #1$}}{#2}}
|
||||
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}}
|
||||
labelaat/.style 2 args={labelat={[above]{$\scriptstyle #1$}}{#2}}
|
||||
}
|
||||
\tikzset{
|
||||
loina/.style={label={[above=.5em]{$\scriptstyle #1$}}}
|
||||
}
|
||||
\tikzset{
|
||||
labeld/.style={label={[below]{$\scriptstyle #1$}}}
|
||||
labeld/.style={label={[below]{$\scriptstyle #1$}}}
|
||||
}
|
||||
\tikzset{
|
||||
labelb/.style={label={[below]{$\scriptstyle #1$}}}
|
||||
labelb/.style={label={[below]{$\scriptstyle #1$}}}
|
||||
}
|
||||
\tikzset{
|
||||
labelbat/.style 2 args={labelat={[below]{$\scriptstyle #1$}}{#2}}
|
||||
labelbat/.style 2 args={labelat={[below]{$\scriptstyle #1$}}{#2}}
|
||||
}
|
||||
\tikzset{
|
||||
loinb/.style={label={[below=.5em]{$\scriptstyle #1$}}}
|
||||
loinb/.style={label={[below=.5em]{$\scriptstyle #1$}}}
|
||||
}
|
||||
\tikzset{
|
||||
labelal/.style={label={[above left]{$\scriptstyle #1$}}}
|
||||
labelal/.style={label={[above left]{$\scriptstyle #1$}}}
|
||||
}
|
||||
\tikzset{
|
||||
labelalat/.style 2 args={labelat={[above left]{$\scriptstyle #1$}}{#2}}
|
||||
labelalat/.style 2 args={labelat={[above left]{$\scriptstyle #1$}}{#2}}
|
||||
}
|
||||
\tikzset{
|
||||
labelbl/.style={label={[below left]{$\scriptstyle #1$}}}
|
||||
labelbl/.style={label={[below left]{$\scriptstyle #1$}}}
|
||||
}
|
||||
\tikzset{
|
||||
labelblat/.style 2 args={labelat={[below left]{$\scriptstyle #1$}}{#2}}
|
||||
labelblat/.style 2 args={labelat={[below left]{$\scriptstyle #1$}}{#2}}
|
||||
}
|
||||
\tikzset{
|
||||
labellat/.style 2 args={labelat={[left]{$\scriptstyle #1$}}{#2}}
|
||||
labellat/.style 2 args={labelat={[left]{$\scriptstyle #1$}}{#2}}
|
||||
}
|
||||
|
||||
\newcommand{\cs}[2][draw,->]{ %
|
||||
@ -635,7 +635,7 @@
|
||||
\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)$) ; %
|
||||
@ -696,19 +696,19 @@
|
||||
|
||||
\tikzset{shortenlr/.style 2 args={shorten <={#1 ex},shorten >={#2 ex}}}
|
||||
\tikzset{
|
||||
back/.style={densely dotted}
|
||||
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}
|
||||
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}}
|
||||
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}
|
||||
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}}
|
||||
@ -719,7 +719,7 @@
|
||||
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}}}
|
||||
@ -747,33 +747,33 @@
|
||||
\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);}
|
||||
}}}
|
||||
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);}}
|
||||
@ -845,7 +845,7 @@
|
||||
(#2) edge[twod={#4},bend left=15] (#1) %
|
||||
; %
|
||||
\path (u) -- node[pos=.5,sloped] {$\dashv$} (d) ; %
|
||||
}
|
||||
}
|
||||
|
||||
\newcommand{\ladjunction}[4]{%
|
||||
\path[->] %
|
||||
@ -853,7 +853,7 @@
|
||||
(#2) edge[twod={#4},bend left=15] (#1) %
|
||||
; %
|
||||
\path (u) -- node[pos=.5,sloped] {$\vdash$} (d) ; %
|
||||
}
|
||||
}
|
||||
|
||||
\newcommand{\adjs}[8][1]{%
|
||||
\begin{tikzpicture} %
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user