Compare commits
2 Commits
5c75b2b701
...
b3af010882
| Author | SHA1 | Date | |
|---|---|---|---|
b3af010882
|
|||
|
87358efe42
|
@ -33,7 +33,7 @@
|
||||
|
||||
A sort specification is a list of \emph{sort declarations} that are defined with \emph{parameters} with $\Set$ as its codomain.
|
||||
|
||||
We give an example of a classical sort specification for Type Theory. On the right column we give the interpretation of the sort declaration on models.
|
||||
We give an example of a sort specification for Type Theory. On the right column we give the interpretation of the sort declarations as components of the models.
|
||||
|
||||
\vspace{1em}
|
||||
\renewcommand\arraystretch{1.5}
|
||||
@ -44,24 +44,24 @@
|
||||
\end{tabular}
|
||||
\vspace{1em}
|
||||
|
||||
A sort declaration therefore describes the sets that the model contains.
|
||||
A sort specification therefore specifies the differents kinds of sets contained in a model, and how they relate to each other.
|
||||
|
||||
\paragraph{Constructor specification}
|
||||
We can also add constructors to a sort specification to make a complete GAT. Those constructors rather describe elements of the sets contained in the model, previously defined by the sort declaration.
|
||||
We can also add constructors to a sort specification. Those constructors specify elements of the sets contained in the model, previously defined by the sort declaration.
|
||||
For example, for the previous sort specification, one can add the following constructors:
|
||||
|
||||
\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 \in X_\Con$, an element$\operatorname{unit}\;\Gamma \in X_\Ty(\Gamma)$.\\
|
||||
$\operatorname{unit} : (\Gamma : \Con) \to \Ty\;\Gamma$ & In any context $\Gamma \in X_\Con$, a type $\operatorname{unit}(\Gamma) \in X_\Ty(\Gamma)$.\\
|
||||
|
||||
$\operatorname{tt}: (\Gamma : \Con) \to \Tm\;\Gamma\;(\operatorname{unit}\;\Gamma)$ & In any context $\Gamma \in X_\Con$, an element $\operatorname{tt}\;\Gamma \in X_\Tm(\Gamma,\operatorname{unit}\;\Gamma)$.
|
||||
$\operatorname{tt}: (\Gamma : \Con) \to \Tm\;\Gamma\;(\operatorname{unit}(\Gamma))$ & In any context $\Gamma \in X_\Con$, an element $\operatorname{tt}(\Gamma) \in X_\Tm(\Gamma,\operatorname{unit}(\Gamma))$.
|
||||
\end{tabular}
|
||||
\vspace{1em}
|
||||
|
||||
\paragraph{Two-sortification}
|
||||
|
||||
It was observed\cite{AmbrusSzumiXie2sort} that one can transform any GAT into a GAT with only two sorts. We will present this transformation.
|
||||
It was observed \cite{AmbrusSzumiXie2sort} that one can transform any GAT into a GAT with only two sorts. We will present this transformation.
|
||||
|
||||
The sort specification of the transformed GAT is always the same, and contains these two sort declarations:
|
||||
|
||||
@ -89,9 +89,9 @@
|
||||
$\dots$
|
||||
\end{tabular}
|
||||
|
||||
This process has not been formally justified, although it has been used like in Phipippo Sestini's thesis.
|
||||
This process is useful when studying GATs, as it allows to restrict a study to GATs with only two sorts without loss of generality. It has been used in Philippo Sestini's thesis, although it has not been formally justified.
|
||||
|
||||
\todo{choose}
|
||||
\todo{Ça veut dire qqch que le \enquote{process} pas été \enquote{justified} ?}
|
||||
|
||||
\begin{quote}
|
||||
Many instances of multi-sorted IITs [IITs are variants 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.
|
||||
@ -99,7 +99,7 @@
|
||||
|
||||
\paragraph{Goal}
|
||||
|
||||
The goal of my internship was to study and undestrand the relationship between the categories of models of an original GAT and the category of models of the transformed GAT, in order to legitimate this transformation.
|
||||
The goal of my internship was to study and understand the relationship between the categories of models of an original GAT and the category of models of the transformed GAT, in order to legitimate this transformation.
|
||||
|
||||
We constructed a coreflection between those two categories, whose formal definition is given in next section. It consists 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.
|
||||
|
||||
@ -116,30 +116,48 @@
|
||||
|
||||
\section{Construction of the coreflection}
|
||||
|
||||
\subsection{Preliminaries}
|
||||
\paragraph{Structure of the proof}
|
||||
|
||||
\paragraph{Category of models of the two-sort sort specification}
|
||||
We will only only formalize the transformation for \emph{sort specification} (i.e. lists of sort declaration). We will show how we take into account the constructors in \autoref{sec:constructors2trans}.
|
||||
|
||||
The usual way of defining the category of models of the two-sort specification $\BB_0$ is by taking the category of families of sets. However, we will rather use a the category of models of the two-sort specification the category $\TSet$ of presheaves over the category with one arrow.
|
||||
This proof is a big induction on the number of sorts taken into account. At each step, we will add a new sort declaration, represented by a functor $H_i$ described later \inlinetodo{MISSING REF}.
|
||||
|
||||
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
|
||||
At the $i$-th recursion step, we will build the following objects :
|
||||
\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$
|
||||
\setlength\itemsep{-1ex}
|
||||
\item The category of models of the GAT $\CC_i$
|
||||
\item The category of models of the transformed GAT $\BB_i$
|
||||
\item A functor $R_{i-1}^i : \BB_i \to \BB_{i-1}$ and $R_0^i : \BB_i \to \BB_0$, taking track of the fixed sort specification of the transformed GAT. \inlinetodo{Mal Dit, est-ce nécessaire ?}
|
||||
\item An bifunctor $\tl^i : \BB_i \times \BB_0 \to \BB_i$ along with a morphism $\inj_\tl^i : X \to X \tl^i Y$ for every $X,Y$ in $\BB_i \times \BB_0$, and an isomorphism $\en_{i-1}^i : R_{i-1}^i (X \tl^i Y) \to (R_{i-1}^i X) \tl^{i-1} Y$. This bifunctor follows a specific universal property: For every morphisms $g : X \to Z$ and $h : Y \to R_0^iZ$, there is an unique morphism $\{g;h\}$ such that the two following diagrams commute:
|
||||
\begin{center}
|
||||
% YADE DIAGRAM TlUniversal.json
|
||||
% GENERATED LATEX
|
||||
\input{graphs/TlUniversal.tex}
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
|
||||
where $\en_0^i$ is the composition $\en_0^1 \circ R_0^1\en_1^2 \circ \dots \circ R_0^{i-1}\en_{i-1}^i : R_0^i(X \tl^i Y) \to (R_0^iX) \oplus Y = (R_0^iX)\tl^0 Y$.
|
||||
|
||||
\todo{Faut indiquer $\oplus = \tl^0$ à un moment :/}
|
||||
|
||||
\item A functor $F_i : \BB_i \to \CC_i$
|
||||
\item A functor $G_i : \CC_i \to \BB_i$
|
||||
\item An adjunction between them $F_i \vdash G_i$
|
||||
\item A proof that $F_iG_i \cong \Id_{\CC_i}$ (i.e. $F_i \vdash G_i$ make up a coreflection)
|
||||
\item A proof that $F_i\inj_1$ is an isomorphism
|
||||
\end{itemize}
|
||||
|
||||
Therefore the categories of models of the transformed GATs will be built atop of this category $\BB_0 = \TSet$.
|
||||
Here is a figure that describes the recursive construction of some of the above objects
|
||||
\begin{center}
|
||||
% YADE DIAGRAM G1.json
|
||||
% GENERATED LATEX
|
||||
\input{graphs/G1.tex}
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
|
||||
\subsection{Preliminaries}
|
||||
|
||||
\paragraph{Grothendieck Construction}
|
||||
\paragraph{Grothendieck Construction}
|
||||
For a category $\mathcal{C}$ and a functor $F : \mathcal{C} \to \Cat$, the Grothendieck construction is a category whose objects are pairs of
|
||||
\begin{itemize}
|
||||
\item $X$ an object of $\mathcal{C}$
|
||||
@ -165,6 +183,29 @@
|
||||
|
||||
We will often concatenate the two method above to create from a category $\mathcal{C}$ and a functor $H : \mathcal{C} \to \Set$ a new category $(X : \mathcal{C}) \times \left(\Set\middle/H(X)\right)$.
|
||||
|
||||
\paragraph{Category of models of the two-sort sort specification}
|
||||
|
||||
The usual way of defining the category of models of the two-sort specification $\BB_0$ is by taking the category of families of sets. However, we will rather use a the category of models of the two-sort specification the category $\TSet$ of presheaves over the category with one arrow.
|
||||
|
||||
In the rest of the document, we will denote this category with one arrow as $\TT$. The objects and arrow of this category are pictured below.
|
||||
|
||||
\begin{center}
|
||||
% YADE DIAGRAM G0.json
|
||||
% GENERATED LATEX
|
||||
\input{graphs/G0.tex}
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
|
||||
With this formalisation, a model of the two-sort GAT is a functor $X : \TSet$, such that
|
||||
\begin{itemize}
|
||||
\item $X_\UU$ is the set of the \enquote{sort objects}
|
||||
\item For each sort object $\Gamma \in X_\UU$, the set of objects corresponding to the sort object is $X_p^-1(\{\Gamma\}) \subset X_\El$
|
||||
\end{itemize}
|
||||
|
||||
Therefore the categories of models of the transformed GATs will be built atop of this category $\BB_0 = \TSet$.
|
||||
|
||||
\todo{Rewrite this part explaining the correspondance}
|
||||
|
||||
\paragraph{$\Hbar$ functor}
|
||||
|
||||
Where $\Hbar_A$ is a functor $(X:C) \times (\Set/A(X)) \to \TSet$ defined as
|
||||
@ -176,81 +217,79 @@
|
||||
\begin{remark}
|
||||
This functor can be constructed using the formal construction of the Grothendieck construction as a pullback in the category of categories $\Cat$
|
||||
\end{remark}
|
||||
|
||||
\subsection{Initialization}
|
||||
In the first step, corresponding to an empty sort specification, the objects are defined as follows:
|
||||
|
||||
\begin{itemize}
|
||||
\setlength\itemsep{-1ex}
|
||||
\item $\CC_i$ is $\one$, the category with only one object and one morphism (i.e. the terminal category of $\Cat$), because the empty sort specification only has one model. \inlinetodo{Isn't it up to isomorphism ?}
|
||||
\item $\BB_i$ is $\TSet$, the category of sorts of the ($\mathcal{O},\El$ sort specification)
|
||||
\item $\tl^0 : \BB_0 \times \BB_0 \to \BB_0$ is the coproduct of $\TSet$, with $\inj_\tl^0 : X \to X \oplus Y$ being the first injector of the coproduct. We will also denote as $\inj_2^0$ the second injector of this coproduct. \inlinetodo{Est-ce que ça pose problème de parler de \emph{the} coproduct ?}
|
||||
\item $F_0 : \TSet \to \one$ is the terminal functor of $\Cat$
|
||||
\item $G_0 : \one \to \TSet$ is the functor that sends the only object of $\one$ to the initial object of $\TSet$: $0_\TSet$
|
||||
\item With $\star$ being the object of $\one$, and for $X$ an object of $\TSet$, we have
|
||||
\[\Hom(G_0 \star,X) = \Hom(0_\TSet,X) \cong 1 \cong \Hom(\star,F_0 X)\]
|
||||
Therefore, we have that $F_0 \vdash G_0$ \inlinetodo{Are the iso/equiv equalities correct ?}
|
||||
\item $F_0G_0 : \one \to \one$ so $F_0G_0 = \Id_\one$ as $\one$ is terminal in $\Cat$
|
||||
\item $F_i\inj_1 = \id_\star$ which is an isomorphism
|
||||
\end{itemize}
|
||||
|
||||
|
||||
\subsection{Constructing the categories}
|
||||
|
||||
We will construct both categories $\CC$ and $\BB$ sort declaration by sort declaration in one big recursive process. At each step, we will build the categories $\CC_i$ and $\BB_i$, the adjunction $F_i \vdash G_i$, and keep some invariants that will be stated in \autoref{sec:hypotheses}.
|
||||
In this part, i will show how we construct recursively both categories $\CC_i$ and $\BB_i$, along with the functor $R_{i-1}^i : \BB_i \to \BB_{i-1}$. We will use the loop invariants that we expressed in the introduction of this section.
|
||||
|
||||
At the i-th recursion step, we will build the category $\CC_i$ which is the category of models of the $i$ first sorts of the sort specification. Likewise, $\BB_i$ will be the category of models of the 2-sorted $i$ first sorts of the sort specification.
|
||||
|
||||
The overall recursive construction of the categories and of the adjunctions $F_i \vdash G_i$ is given below.
|
||||
|
||||
\begin{center}
|
||||
% YADE DIAGRAM G1.json
|
||||
% GENERATED LATEX
|
||||
\input{graphs/G1.tex}
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
|
||||
The first step of our recursion is the trivial adjunction $\lambda . \star \vdash \lambda . 1$ between the categories $\BB_0 = \TSet$ and $\CC_0 = 1$, the category with one object and one morphism (i.e. the terminal element of $\Cat$). $\lambda. \star$ is the terminal morphism of this object, and its right adjoint sends the only object of $1$ to the terminal object of the category $\TSet$.
|
||||
|
||||
The functors $R_{i-1}^i$ are the forgetful monadic functors that forget about the $i$-th sort contsructor. They have a left adjoint denoted $L_{i-1}^i$.
|
||||
As we can compose the adjunctions $R_0^1$,$R_1^2$,...,$R_{i-1}^i$, we will use the two following adjunctions
|
||||
\[\begin{array}{c}
|
||||
R_0^i = R_{0}^{i-1} \circ R_{i-1}^{i} = R_{0}^{1} \circ ... \circ R_{i-1}^{i}\\
|
||||
L_0^i = L_{i-1}^{i} \circ L_{0}^{i-1} = L_{i-1}^{i} \circ ... \circ L_{0}^{1}
|
||||
\end{array}\]
|
||||
In order to construct the categories, we need some object describing the specific sort we are adding to the categories. This object is a specific functor $H_i : \CC_{i-1} \to \Set$. We suppose that those $H_i$ functors are given.
|
||||
|
||||
\begin{remark}
|
||||
There is also an adjunction chain between $\CC_0$,$\dots$,$\CC_{i-1}$,$\CC_i$, but we don't use it in the proof.
|
||||
There is a way of getting the functor $H_i$ from the syntax, which is described in \autoref{sec:HiFromSyntax}.
|
||||
\end{remark}
|
||||
|
||||
\subsubsection{Constructing $\CC_i$}
|
||||
|
||||
We construct the category $\CC_i$ as the following pair:
|
||||
We construct the category $\CC_i$ as the following Grothendieck pair:
|
||||
\[
|
||||
\CC_i = (X : \CC_{i-1}) \times \left(\Set\middle/H_i(X)\right) = (X : \CC_{i-1}) \times \left(\Set^{H_i(X)}\right)
|
||||
\]
|
||||
and where $H_i$ is a specific functor $\CC_{i-1} \to \Set$, such that $H_i(X)$ is the set of parameters for the construction of the new sort.
|
||||
and where $H_i$ is the specific functor described above.
|
||||
|
||||
\todo{Do we need this functor to be representable. If so, precise it}
|
||||
|
||||
\paragraph{$H_i$ functors for our Type Theory example}
|
||||
Let us give an example of those $H_i$ objects for our type theory example. We begin with
|
||||
Let us now give an example of those $H_i$ objects for our type theory example.
|
||||
|
||||
We begin with the following functor, corresponding to the sort declaration $\boxed{\Con : \Set}$
|
||||
\[
|
||||
H_1(\star) = 1 \in \operatorname{Obj}(\Set)
|
||||
H_1(\star) = 1 \in \operatorname{Obj}(\Set)
|
||||
\]
|
||||
which corresponds to the fact that $\Con$ takes no parameter.
|
||||
|
||||
Therefore $\CC_1 = 1 \times \Set^1 = \Set$, and the set of a model corresponds to \enquote{the set of contexts}.
|
||||
Therefore $\CC_1 = 1 \times \Set^1 = \Set$, which is as expected: a model is a set.
|
||||
|
||||
Then, we take the functor $H_2(X_\Con) = X_\Con$ (this means, that types need \emph{one} context to be built).
|
||||
Then, we take the functor $H_2(X_\Con) = X_\Con$, corresponding to the sort declaration $\boxed{\Ty : (\Gamma : \Con) \to \Set}$ (this means, that types need \emph{one} context to be built).
|
||||
|
||||
Therefore $\CC_2 = (X:\Set) \times \Set^X \cong \FamSet$, families of sets.
|
||||
Therefore $\CC_2 = (X:\Set) \times (\Set/X) \simeq (X:\Set) \times (\Set^X) = \FamSet$, a model is a family of sets.
|
||||
|
||||
Finally, we take the functor $H_3(X_\Con,X_\Ty) = \sum_{\Gamma : X_\Con}X_\Ty(\Gamma)$ (this means that terms need \emph{one} context, and \emph{one} type of that context).
|
||||
Finally, we take the functor $H_3(X_\Con,X_\Ty) = \sum_{\Gamma : X_\Con}X_\Ty(\Gamma)$, that corresponds to the sort declaration $\boxed{\Tm : (\Delta : \Con) \to (A : \Ty\;\Delta) \to \Set}$ (this means that terms need \emph{one} context, and \emph{one} type of that context).
|
||||
|
||||
The final category $\CC_3$ is composed of triples $(X_\Con: \Set, X_\Ty : X_\Con \to \Set, X_\Tm : (\Delta: X_\Con) \to X_\Ty(\Delta) \to \Set)$
|
||||
|
||||
\begin{remark}
|
||||
There is a way of getting the functor $H_i$ from the syntax, which is given in \autoref{sec:CtoSSetFiore}.
|
||||
\end{remark}
|
||||
An object of that final category $\CC_3$ is a triple $(X_\Con: \Set, X_\Ty : X_\Con \to \Set, X_\Tm : (\Delta: X_\Con) \to X_\Ty(\Delta) \to \Set)$
|
||||
|
||||
\subsubsection{Constructing $\BB_i$}
|
||||
|
||||
\paragraph{The category} We construct the category $\BB_i$ as follows.
|
||||
We construct the category $\BB_i$ as follows.
|
||||
|
||||
An object of $\BB_i$ is
|
||||
\begin{itemize}
|
||||
\item an object $X$ of $\BB_{i-1}$
|
||||
\item a \enquote{sort constructor} $\Cstr_i$ as a function $H_i(F_{i-1}X) \to (R_0^{i-1}X)_\UU$
|
||||
\item a \enquote{sort constructor} $\Cstr$ as a function $H_iF_{i-1}X \to (R_0^{i-1}X)_\UU$
|
||||
\newline
|
||||
where $H_i$ is the functor $\CC_{i-1} \to \Set$ that describe the sort constructor being processed, and $F_{i-1}$ is the right part of the adjunction $\BB_{i-1} \to \CC_{i-1}$ that we are defining recursively at the same time.
|
||||
This $H_i$ functor will be so that $H_i \circ F_{i-1} \circ \inj_1^{i-1}$ is an isomorphism. \inlinetodo{Pas déclaré ici, c'est grâve ?}
|
||||
where $H_i$ is the functor $\CC_{i-1} \to \Set$ described above and $F_{i-1}$ is the right part of the adjunction $\BB_{i-1} \to \CC_{i-1}$ that we are defining recursively at the same time.
|
||||
\end{itemize}
|
||||
|
||||
If we have an object $X$ of $\BB_i$, the first component is denoted as $R_{i-1}^iX$, and the second component is denoted as $\Cstr^X : R_{i-1}^i \to (R_0^iX)_\UU$.
|
||||
|
||||
A morphism $(X,\Cstr_i) \to (X',\Cstr'_i)$ of $\BB_i$ is a morphism $f : X \to X'$ in $\BB_{i-1}$ such that the following diagram commutes.
|
||||
A morphism $X \to X'$ of $\BB_i$ is a morphism $f : R_{i-1}^iX \to R_{i-1}^iX'$ in $\BB_{i-1}$ such that the following diagram commutes.
|
||||
|
||||
\begin{center}
|
||||
% YADE DIAGRAM D1.json
|
||||
@ -259,62 +298,15 @@
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
|
||||
For a morphism $f : X \to X'$ of $\BB_i$, we denote as $R_{i-1}^if$ the underlying morphism $R_{i-1}^i X \to R_{i-1}^i X'$.
|
||||
|
||||
Identities and compositions are that of the category $\BB_{i-1}$, and categorical equalities are trivially derived from the diagram above.
|
||||
|
||||
\paragraph{The adjunction}
|
||||
We also define a functor $R_{i-1}^i : \BB_i \to \BB_{i-1}$ that sends objects and morphisms to their first component. This functor is a \emph{right adjoint} of another functor we call $L_{i-1}^i$.
|
||||
|
||||
We will also denote $\eta_i^j : \mathbf{1} \to R_i^j L_i^j$ and $\varepsilon_i^j : L_i^j R_i^j \to \mathbf{1}$ to be the unit and counit of the adjunction $R_i^j \vdash L_i^j$.
|
||||
|
||||
\paragraph{The coproduct}
|
||||
For an object $X$ in $\BB_i$ and $Y$ in $\BB_0$, there is a coproduct $X \oplus_i L_0^i Y$ in the category $\BB_{i-1}$. We will denote as $\inj_1^i : X \to X \oplus L_0^iY$ (resp. $\inj_2^i : L_0^iY \to X \oplus L_0^iY$) the first (resp. second) injector of the coproduct of $\BB_i$. For every morphism $f : X \to Z$ and $g : L_0^iY \to Z$, we will denote with $\{f;g\}$ the unique morphism from $X \oplus L_0^iY$ to $Z$ such that $\{f;g\} \circ \inj^i_1 = f$ and $\{f;g\} \circ \inj^i_2 = g$.
|
||||
|
||||
\begin{remark}
|
||||
This adjunction and the existence of a coproduct comes from seeing $\BB_i$ being a category of algebras in $\BB_{i-1}$ over the morphism $inj_1 : G_{i-1}O_i \to G_{i-1}O_i \oplus L_0^{i-1} y\UU$. \inlinetodo{Ça ne marche plus du coup :/}
|
||||
\end{remark}
|
||||
|
||||
|
||||
\subsection{Induction Hypotheses}
|
||||
|
||||
In order to build and prove the adjunction, we will state some recurrence invariants that we will prove after having built objects.
|
||||
|
||||
\begin{property}[H1]
|
||||
|
||||
The canonical morphism
|
||||
\[
|
||||
\simpleArrow{R_{i-1}^i X \oplus L_0^{i-1} Y}{\left\{R_{i-1}^i \inj_1^i ; R_{i-1}^i \inj_2^i \circ \eta_{i-1}^i\right\}}{R_{i-1}^i(X \oplus_i L_0^i Y)}
|
||||
\]
|
||||
that we will denote as $\en_{i-1}^i$ is an isomorphism.
|
||||
|
||||
Its recursive version is the following isomorphism, denoted as $\en_0^i$
|
||||
\[
|
||||
\simpleArrow{ R_{0}^i X \oplus_0 Y}{\left\{R_0^i \inj_1^i ; R_0^i \inj_2^i \circ \eta_0^i\right\}}{R_0^i(X \oplus_i L_0^i Y)}
|
||||
\]
|
||||
\end{property}
|
||||
|
||||
\begin{property}[H3]
|
||||
\[
|
||||
\simpleArrow{F_i X}{F(\inj_1^i)}{F_i(X \oplus L_0^i Y)}
|
||||
\]
|
||||
is an isomorphism.
|
||||
|
||||
We will often this equality along with the $F_i \vdash G_i$ adjunction (for an object $O$ in $\CC_i$)
|
||||
\[
|
||||
\Hom(G_i O, X) \cong \Hom(O, F_i X) \cong \Hom(O, F_i(X \oplus L_0^i Y)) \cong \Hom(G_i O, X \oplus L_0^i Y)
|
||||
\]
|
||||
|
||||
This new isomorphism is the following:
|
||||
\[
|
||||
\simpleArrow{\Hom(G_i O, X)}{(inj_1^i \circ \dash)}{\Hom(G_i O,X \oplus L_0^i Y)}
|
||||
\]
|
||||
|
||||
\todo{Du coup techniquement, c'est une propriété de $H_i$. Faut réussir que c'est \emph{parce que} $H_i$ est représentable que l'on peut déduire H3' de H3.}
|
||||
|
||||
\end{property}
|
||||
$R_{i-1}^i$ acts on objects and morphisms, and therefore creates a functor $\BB_i \to \BB_{i-1}$.
|
||||
|
||||
\subsection{Constructing the functors}
|
||||
|
||||
In order to use all the power of the recurrence, we will build the $F_i \vdash G_i$ adjunction using the $F_{i-1} \vdash G_{i-1}$ adjunction, following the diagram below.
|
||||
Build the $F_i \vdash G_i$ adjunction using the two functors of the $F_{i-1} \vdash G_{i-1}$ adjunction, following the diagram below.
|
||||
|
||||
\begin{center}
|
||||
% YADE DIAGRAM G2.json
|
||||
@ -323,34 +315,39 @@
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
|
||||
\todo{$G_{i-1} \times \id$ et son compère, c'est bien legit ?}
|
||||
|
||||
The first part $G_{i-1} \times \id \dashv F_{i-1} \times \id$ is proven and defined as an adjunction from the previous step of the recurrence.
|
||||
Where
|
||||
\[
|
||||
(F_{i-1} \times \id)(X,(Y,y)) = (F_{i-1}X,(Y,y))
|
||||
\]
|
||||
and
|
||||
\[
|
||||
(G_{i-1} \times \id)(X,(Y,y)) = (G_{i-1}X,(Y,H_i\eta_{i-1} \circ y))
|
||||
\]
|
||||
\todo{Définir $\eta_{i-1}$ ici !}
|
||||
\todo{Plus de précision sur ces constructions ?}
|
||||
\todo{Expliquer pourquoi $(F_{i-1} \times \id) \vdash (G_{i-1} \times \id)$ est une adjonction}
|
||||
|
||||
|
||||
\subsubsection{W definition}
|
||||
|
||||
We define a functor $W : \left(X : \BB_{i-1}\right) \times \Set/H_i(F_{i-1}X) \to \BB_{i}$
|
||||
We define a functor $W : \left(X : \BB_{i-1}\right) \times \Set/H_iF_{i-1}X \to \BB_{i}$
|
||||
|
||||
The action on objects is as follows:
|
||||
\[
|
||||
W(X,Y) := \left(X \oplus L_0^{i-1} \Hbar_{H_iF_{i-1}}(X,Y), \widetilde{\inj_2} \right)
|
||||
W(X,Y) := \left(X \tl^{i-1} K_{H_iF_{i-1}}(X,Y), \widetilde{\inj_2} \right)
|
||||
\]
|
||||
|
||||
With $\widetilde{\inj_2}$ being defined by \inlinetodo{Changer les noms des hypothèses H3' et H1r}
|
||||
\[
|
||||
\begin{array}{lcl}
|
||||
H_iF_{i-1}(X \oplus L_0^{i-1} \Hbar_\bullet(X,Y)))
|
||||
& \to^{\text{H3'}} & H_i(F_{i-1}X)\\
|
||||
& = & \left(\Hbar_{H_iF_{i-1}}(X,Y)\right)_\UU \\
|
||||
& \to^{\inj_2^0} & \left(R_0^{i-1}X \oplus \Hbar_\bullet(X,Y)\right)_\UU \\
|
||||
& \to^{\text{H1r}} & \left(R_0^{i-1}(X \oplus L_0^{i-1}\Hbar_\bullet(X,Y))\right)_\UU
|
||||
\end{array}
|
||||
\]
|
||||
With $\widetilde{\inj_2}$ being defined by the composition
|
||||
\begin{center}
|
||||
% YADE DIAGRAM Wdef.json
|
||||
% GENERATED LATEX
|
||||
\input{graphs/Wdef.tex}
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
|
||||
The action on a morphism $(g,h)$ from $(X,Y)$ to $(X',Y')$ is the following:
|
||||
The action on a morphism $(g,h)$ from $(X,(Y,y))$ to $(X',(Y',y'))$ is the following:
|
||||
\[
|
||||
W(g,h) := \left(g \oplus L_0^{i-1} \Hbar_{H_iF_{i-1}}(g,h)\right)
|
||||
W(g,h) := \left(g \tl^{i-1} K_{H_iF_{i-1}}(g,h)\right)
|
||||
\]
|
||||
|
||||
It is indeed a morphism from $\BB_{i}$ as it makes the following diagram commute.
|
||||
@ -368,7 +365,7 @@
|
||||
|
||||
The action on objects is
|
||||
\[
|
||||
E(X) = (R_{i-1}^i X, (A,h))
|
||||
E(X) = (R_{i-1}^i X, (A,h))
|
||||
\]
|
||||
Where $(A,h)$ is defined as the following pullback:
|
||||
|
||||
@ -405,7 +402,7 @@
|
||||
Let $f$ be in $\Hom(W(X,Y),Z)$.
|
||||
We want to construct $\phi_{XYZ}(f) : (X,Y) \to E(Z)$.
|
||||
|
||||
The first component of $\phi_{XYZ}(f)$ is $R_{i-1}^i f \circ inj_1^{i-1} : X \to R_{i-1}^i Z$, with $R_{i-1}^i f$ being a morphism of $\BB_{i-1}$ from $R_{i-1}^i(W(X,Y)) = X \oplus_{i-1} L_0^{i-1}$ to $R_{i-1}^i Z$.
|
||||
The first component of $\phi_{XYZ}(f)$ is $R_{i-1}^i f \circ inj_\tl^{i-1} : X \to R_{i-1}^i Z$, with $R_{i-1}^i f$ being a morphism of $\BB_{i-1}$ from $R_{i-1}^i(W(X,Y)) = X \tl^{i-1}K_{H_iF_{i-1}}(X,Y)$ to $R_{i-1}^i Z$.
|
||||
|
||||
The second component is defined through the universal property of the pullback defined by $E(Z)$ according to the following diagram:
|
||||
|
||||
@ -420,7 +417,8 @@
|
||||
|
||||
Now, we take $(g,h)$ a morphism from $(X,Y)$ to $E(Z)$.
|
||||
|
||||
We define $\phi^{-1}_{XYZ}(g,h)$ as a morphism of $\BB_i$ from $W(X,Y)$ to $Z$, i.e. a morphism of $\BB_{i-1}$ from $X \oplus_{i-1} L_0^{i-1} \Hbar (X,Y)$ to $R_0^{i-1}(Z)$ that makes a certain diagram commute:
|
||||
We define $\phi^{-1}_{XYZ}(g,h)$ as a morphism of $\BB_i$ from $W(X,Y)$ to $Z$, i.e. a morphism of $\BB_{i-1}$ from $X \tl^{i-1} K_{H_iF_{i-1}} (X,Y)$ to $R_{i-1}^i(Z)$ that is built using the universal property of $\tl^{i-1}$
|
||||
\todo{Describe the initial property}
|
||||
\[
|
||||
\phi^{-1}_{XYZ}(g,h) := \left\{g ; \varepsilon_0^i \circ L_0^{i-1} \square \right\}
|
||||
\]
|
||||
@ -437,7 +435,7 @@
|
||||
This is indeed a morphism of $\BB_i$ from $W(X,Y)$ to $Z$ as it makes the following diagram commute
|
||||
|
||||
\begin{center}
|
||||
% YADE DIAGRAM D8.json
|
||||
% YADE DIAGRAM D8.json
|
||||
% GENERATED LATEX
|
||||
\input{graphs/D8.tex}
|
||||
% END OF GENERATED LATEX
|
||||
@ -452,30 +450,29 @@
|
||||
|
||||
The proof is given in \autoref{apx:FG-refl}.
|
||||
|
||||
\subsection{Proof of the hypotheses}
|
||||
\subsubsection{Proof of H1}
|
||||
\subsection{Other objects}
|
||||
\subsubsection{Constructing $\tl^i$}
|
||||
|
||||
\todo{Relire + réeexpliquer pourquoi ça prouve}
|
||||
\label{sec:coproductConstr}
|
||||
We will define the sums of the form $X \oplus_i L_0^i Y$ in $\BB_i$.
|
||||
|
||||
\paragraph{Constructing the objects}
|
||||
We will define the $\tl^i$ bifunctor of two objects $X$ from $\BB_i$ and $Y$ from $\BB_0$ as follows:
|
||||
\[
|
||||
X \oplus_i L_0^i Y := \left(R_{i-1}^i X \oplus_{i-1} L_0^{i-1} Y, (R_0^{i-1} \inj_1^{i-1})_\UU \circ \Cstr_i^X \circ (H_iF_{i-1}\inj_1^{i-1})^{-1}\right)
|
||||
X \tl_i Y := \left(R_{i-1}^i X \tl^{i-1} Y, (R_0^{i-1} \inj_\tl^{i-1})_\UU \circ \Cstr_i^X \circ (H_iF_{i-1}\inj_\tl^{i-1})^{-1}\right)
|
||||
\]
|
||||
|
||||
Here, $(\inj_1^{i-1} \circ \dash)^{-1}$ is the inverse of the isomorphism of hypothesis H3', and
|
||||
|
||||
|
||||
The constructor goes as follows:
|
||||
\[
|
||||
H_iF_{i-1}(R_{i-1}^i X \oplus_{i-1} L_0^{i-1} Y) \equiv
|
||||
H_iF_{i-1}(R_{i-1}^i X) \to
|
||||
(R_0^{i-1} X)_\UU \to
|
||||
(R_0^i (R_{i-1}^i X \oplus_{i-1} L_0^{i-1} Y))_\UU
|
||||
\]
|
||||
|
||||
The first injector $X \to X \oplus_i L_0^i Y$ is defined as follows:
|
||||
\begin{center}
|
||||
% YADE DIAGRAM TlConstructor.json
|
||||
% GENERATED LATEX
|
||||
\input{graphs/TlConstructor.tex}
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
|
||||
The injector $\inj_\tl^i : X \to X \tl^i Y$ is defined as follows:
|
||||
\[
|
||||
\inj_1^i := \inj_1^{i-1} : R_{i-1}^i X \to R_{i-1}^i (X \oplus_i L_0^i Y) = R_{i-1}^i X \oplus_{i-1} L_0^{i-1} Y
|
||||
\inj_\tl^i := \inj_\tl^{i-1} : R_{i-1}^i X \to R_{i-1}^i (X \tl^i Y) = R_{i-1}^i X \tl^{i-1} Y
|
||||
\]
|
||||
|
||||
It is a morphism of $\BB_i$ as it makes the following diagram commute:
|
||||
@ -487,20 +484,18 @@
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
|
||||
\paragraph{Universal Property}
|
||||
We will now show that that the universal property stated holds.
|
||||
To that extent, we take two objects $X$ and $Z$ in $\BB_i$, $Y$ in $\BB_0$, a morphism $g : X \to Z$ in $\BB_i$ and a morphism $h : Y \to R_0^iZ$ in $\BB_0$. We want to build a morphism $\{g,h\}$ of $\BB_i$ such that the following two diagrams commute.
|
||||
|
||||
The second injector is defined as follows:
|
||||
\[
|
||||
\inj_2^i := (\varepsilon_i \oplus_i \id_{L_0^i Y}) \circ L_{i-1}^i \inj_2^{i-1}
|
||||
\]
|
||||
\begin{center}
|
||||
% YADE DIAGRAM TlUniversal.json
|
||||
% GENERATED LATEX
|
||||
\input{graphs/TlUniversal.tex}
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
|
||||
Where $\varepsilon_i$ is the counit of the adjunction $R_{i-1}^i \vdash L_{i-1}^i$, going from $L_{i-1}^i R_{i-1}^i X$ to $X$.
|
||||
|
||||
This goes from $L_0^i Y = L_{i-1}^i L_0^{i-1} Y$ to $L_{i-1}^i(R_{i-1}^i X \oplus_{i-1} L_0^{i-1} Y)$, which is equivalent to $L_{i-1}^i R_{i-1}^i X \oplus_i L_0^i Y$ as $L_{i-1}^i$ is a left-adjoint functor and therefore it preserves colimits; then goes to $X \oplus_i L_0^i Y$.
|
||||
|
||||
We will now show that this definition is actually a definition of the coproduct in $\BB_i$.
|
||||
To that extent, we take two objects $X$ and $Z$ in $\BB_i$, $Y$ in $\TSet$ and two morphisms of $\BB_i$ $\varphi_1 : X \to Z$ and $\varphi_2 : L_0^i Y \to Z$.
|
||||
|
||||
We define $\{\varphi_1 ; \varphi_2\}_{i } = \{R_{i-1}^i \varphi_1 ; R_{i-1}^i \varphi_2 \circ \eta^i_{L_0^{i-1} Y}\}_{i-1}$ a morphism of $\BB_i$ as it makes the following diagram commute:
|
||||
We define $\{g ; h\}_i = \{R_{i-1}^i g ; h\}_{i-1}$ a morphism of $\BB_i$ as it makes the following diagram commute:
|
||||
|
||||
\begin{center}
|
||||
% YADE DIAGRAM D5.json
|
||||
@ -509,13 +504,11 @@
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
|
||||
With this definition, the isomorphism $\en_{i-1}^i : R_{i-1}^i(X \tl^i Y) \to (R_{i-1}^i X) \tl^{i-1} Y$ is simply the identity morphism.
|
||||
|
||||
\todo{Justifier $R_{i-1}^i(\varepsilon_i \oplus_i \id_{L_0^i Y}) = R_{i-1}^i \varepsilon_i \oplus_{i-1} \id_{L_0^{i-1} Y}$ (with H1 ?)}
|
||||
|
||||
\subsubsection{Proof of H3}
|
||||
|
||||
We need to prove that, for any objects $(X,\Cstr)$ in $\BB_i$ and $Y$ in $\TSet$, that the morphism
|
||||
$F_i(\inj_1^i) : F_i(X,\Cstr) \to F_i((X,\Cstr) \oplus L_0^i Y)$ is an isomorphism.
|
||||
\paragraph{Composition with $F_i$}
|
||||
We finally need to prove, for any objects $X$ in $\BB_i$ and $Y$ in $\TSet$, that the morphism
|
||||
$F_i(\inj_\tl^i) : F_iX \to F_i(X \tl^i Y)$ is an isomorphism.
|
||||
|
||||
We know from \autoref{sec:coproductConstr} that $\inj_1^i := \inj_1^{i-1}$ as a morphism of $\BB_{i}$ is a morphism $\BB_{i-1}$ that verifies some equalities.
|
||||
|
||||
@ -633,6 +626,9 @@
|
||||
|
||||
\todo{(small) Show that it is actually a functor (should be trivial), potentially add a diagram}
|
||||
|
||||
\subsection{Adding 2-transformation of constructors}
|
||||
\label{sec:constructors2trans}
|
||||
\todo{Describe the process}
|
||||
|
||||
\subsection{Overview}
|
||||
|
||||
@ -666,6 +662,9 @@
|
||||
This equality allows us to construct the $\Gamma_i$ functors from the final $S$ category.
|
||||
\end{remark}
|
||||
|
||||
\subsection{Consructing the $H_i$ functors from the syntax}
|
||||
\label{sec:HiFromSyntax}
|
||||
|
||||
\section{Summary}
|
||||
|
||||
\lipsum[2-3]
|
||||
@ -874,6 +873,29 @@
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
@ -1 +1 @@
|
||||
{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}\n\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}","tabs":[{"active":true,"edges":[{"from":0,"id":4,"label":{"kind":"normal","label":"\\Cstr^X","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":5,"label":{"kind":"normal","label":"R_0^{i-1} X_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":6,"label":{"kind":"normal","label":"f \\circ \\dash","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":7,"label":{"kind":"normal","label":"\\Cstr^{X'}","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2}],"nodes":[{"id":0,"label":{"isMath":true,"label":"H_i(F_{i-1}X)","pos":[180,60],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"(R_0^{i-1} X)_\\UU","pos":[450,60],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^{i-1} X')_\\UU","pos":[450,143],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_i(F_{i-1}X')","pos":[180,143],"zindex":-10000}}],"sizeGrid":120,"title":"1"}]},"version":12}
|
||||
{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}\n\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}","tabs":[{"active":true,"edges":[{"from":0,"id":4,"label":{"kind":"normal","label":"\\Cstr^X","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":5,"label":{"kind":"normal","label":"(R_0^{i-1} f)_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":6,"label":{"kind":"normal","label":"H_iF_{i-1}f","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":7,"label":{"kind":"normal","label":"\\Cstr^{X'}","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2}],"nodes":[{"id":0,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^iX","pos":[180,60],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"(R_0^i X)_\\UU","pos":[450,60],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i X')_\\UU","pos":[450,143],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^iX'","pos":[180,143],"zindex":-10000}}],"sizeGrid":120,"title":"1"}]},"version":12}
|
||||
@ -1 +1 @@
|
||||
{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}\n\\newcommand{\\ensuremath}[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\\newcommand{\\inj}{\\operatorname{inj}}\n\\newcommand{\\idr}{\\operatorname{id}}\n","tabs":[{"active":true,"edges":[{"from":0,"id":10,"label":{"kind":"normal","label":"\\text{H3'}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":-1},"to":1},{"from":2,"id":11,"label":{"kind":"normal","label":"\\inj_2^0","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":12,"label":{"kind":"normal","label":"\\text{H1r}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":4,"id":13,"label":{"kind":"normal","label":"R_0^i(g \\oplus L_0^{i-1}\\Hbar_\\bullet(g,h))_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":3,"id":14,"label":{"kind":"normal","label":"(R_0^i g \\oplus \\Hbar_\\bullet(g,h))_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":6,"id":15,"label":{"kind":"normal","label":"\\text{H1r}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":2,"id":16,"label":{"kind":"normal","label":"\\left[\\Hbar_\\bullet(g,h)\\right]_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":1,"id":17,"label":{"kind":"normal","label":"g \\circ \\dash","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":8},{"from":8,"id":18,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":0,"id":19,"label":{"kind":"normal","label":"H_iF_{i-1}(g \\oplus L_0^{i-1}\\Hbar_\\bullet(g,h))","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":9},{"from":9,"id":20,"label":{"kind":"normal","label":"H3'","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":8},{"from":7,"id":21,"label":{"kind":"normal","label":"\\inj_2^0","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":1,"id":22,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":2}],"nodes":[{"id":0,"label":{"isMath":true,"label":"H_iF_{i-1}(X \\oplus L_0^{i-1}\\Hbar_\\bullet(X,Y))","pos":[306,72],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"H_iF_{i-1}(X)","pos":[530,72],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\left[\\Hbar_\\bullet(X,Y)\\right]_\\UU","pos":[682,72],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\left[R_0^{i-1} X \\oplus \\Hbar_\\bullet(X,Y)\\right]_\\UU","pos":[916,72],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"R_0^{i-1}(X \\oplus L_0^{i-1} \\Hbar_\\bullet(X,Y))_\\UU","pos":[1194,72],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"R_0^{i-1}(X' \\oplus L_0^{i-1} \\Hbar_\\bullet(X',Y'))_\\UU","pos":[1194,230],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"\\left[R_0^{i-1} X' \\oplus \\Hbar_\\bullet(X',Y')\\right]_\\UU","pos":[916,230],"zindex":-10000}},{"id":7,"label":{"isMath":true,"label":"\\left[\\Hbar_\\bullet(X',Y')\\right]_\\UU","pos":[682,230],"zindex":0}},{"id":8,"label":{"isMath":true,"label":"H_iF_{i-1}(X')","pos":[530,230],"zindex":0}},{"id":9,"label":{"isMath":true,"label":"H_iF_{i-1}(X' \\oplus L_0^{i-1}\\Hbar_\\bullet(X',Y'))","pos":[306,230],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12}
|
||||
{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}\n\\newcommand{\\ensuremath}[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\\newcommand{\\inj}{\\operatorname{inj}}\n\\newcommand{\\idr}{\\operatorname{id}}\n","tabs":[{"active":true,"edges":[{"from":0,"id":10,"label":{"kind":"normal","label":"(H_iF_{i-1}\\inj_\\tl^{i-1})^{-1}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":-1},"to":1},{"from":2,"id":11,"label":{"kind":"normal","label":"(\\inj_2^0)_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":12,"label":{"kind":"normal","label":"((\\en_0^{i-1})^{-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":4,"id":13,"label":{"kind":"normal","label":"R_0^i(g \\tl^{i-1}K_\\bullet(g,h))_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":3,"id":14,"label":{"kind":"normal","label":"(R_0^i g \\oplus K_{H_iF_{i-1}}(g,h))_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":6,"id":15,"label":{"kind":"normal","label":"((\\en_0^{i-1})^{-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":2,"id":16,"label":{"kind":"normal","label":"\\left[K_{H_iF_{i-1}}(g,h)\\right]_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":1,"id":17,"label":{"kind":"normal","label":"H_iF_{i-1}g","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":8},{"from":8,"id":18,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":0,"id":19,"label":{"kind":"normal","label":"H_iF_{i-1}(g \\tl^{i-1}K_{H_iF_{i-1}}(g,h))","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":9},{"from":9,"id":20,"label":{"kind":"normal","label":"(H_iF_{i-1}\\inj_\\tl^{i-1})^{-1}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":8},{"from":7,"id":21,"label":{"kind":"normal","label":"(\\inj_2^0)_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":1,"id":22,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":2}],"nodes":[{"id":0,"label":{"isMath":true,"label":"H_iF_{i-1}(X \\tl^{i-1}K_{H_iF_{i-1}}(X,Y))","pos":[306,64],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"H_iF_{i-1}X","pos":[634,64],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\left[K_{H_iF_{i-1}}(X,Y)\\right]_\\UU","pos":[810,64],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\left[R_0^{i-1} X \\oplus K_{H_iF_{i-1}}(X,Y)\\right]_\\UU","pos":[1068,64],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"R_0^{i-1}(X \\tl^{i-1} K_\\bullet(X,Y))_\\UU","pos":[1396,64],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"R_0^{i-1}(X' \\tl^{i-1} K_\\bullet(X',Y'))_\\UU","pos":[1396,206],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"\\left[R_0^{i-1} X' \\oplus K_{H_iF_{i-1}}(X',Y')\\right]_\\UU","pos":[1068,206],"zindex":-10000}},{"id":7,"label":{"isMath":true,"label":"\\left[K_{H_iF_{i-1}}(X',Y')\\right]_\\UU","pos":[810,206],"zindex":0}},{"id":8,"label":{"isMath":true,"label":"H_iF_{i-1}X'","pos":[634,206],"zindex":0}},{"id":9,"label":{"isMath":true,"label":"H_iF_{i-1}(X' \\tl^{i-1}K_{H_iF_{i-1}}(X',Y'))","pos":[306,206],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12}
|
||||
@ -1 +1 @@
|
||||
{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":4,"label":{"kind":"normal","label":"h","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":0,"id":5,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":6,"label":{"kind":"normal","label":"R_0^i(X)_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":1,"id":7,"label":{"kind":"normal","label":"\\Cstr^X_i","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3}],"nodes":[{"id":0,"label":{"isMath":true,"label":"A","pos":[100,117.8125],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"H_iF_{i-1}(R_{i-1}^i X)","pos":[100,195.8125],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"R_0^i(X)_\\El","pos":[358,117.8125],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"R_0^i(X)_\\UU","pos":[358,195.8125],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12}
|
||||
{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":4,"label":{"kind":"normal","label":"h","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":0,"id":5,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":6,"label":{"kind":"normal","label":"R_0^i(X)_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":1,"id":7,"label":{"kind":"normal","label":"\\Cstr^X","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":4,"id":8,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":5}],"nodes":[{"id":0,"label":{"isMath":true,"label":"A","pos":[100,117.8125],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i X","pos":[100,195.8125],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"R_0^i(X)_\\El","pos":[358,117.8125],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"R_0^i(X)_\\UU","pos":[358,195.8125],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12}
|
||||
@ -1 +1 @@
|
||||
{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":8,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":9,"label":{"kind":"normal","label":"R_0^i(X)_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":10,"label":{"kind":"normal","label":"h","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.30000000000000004,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":11,"label":{"kind":"normal","label":"\\Cstr^X_i","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":4,"id":12,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":5,"id":13,"label":{"kind":"normal","label":"R_0^i(X')_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":4,"id":14,"label":{"kind":"normal","label":"h'","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.30000000000000004,"tail":"none"},"zindex":0},"to":7},{"from":7,"id":15,"label":{"kind":"normal","label":"\\Cstr^{X'}_i","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":0,"id":16,"label":{"kind":"normal","label":"!","style":{"alignment":"left","bend":0,"color":"black","dashed":true,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":1},"to":4},{"from":1,"id":17,"label":{"kind":"normal","label":"R_0^i(f)_\\El","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":3,"id":18,"label":{"kind":"normal","label":"H_iF_{i-1}R_{i-1}^i f","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.10000000000000003,"tail":"none"},"zindex":0},"to":7},{"from":2,"id":19,"label":{"kind":"normal","label":"R_0^i(f)_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.6,"tail":"none"},"zindex":0},"to":6},{"from":14,"id":20,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":12},{"from":10,"id":21,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":8}],"nodes":[{"id":0,"label":{"isMath":true,"label":"A","pos":[125,115],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"R_0^i(X)_\\El","pos":[403,115],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"R_0^i(X)_\\UU","pos":[403,297],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}(R_{i-1}^i X)","pos":[125,297],"zindex":-10000}},{"id":4,"label":{"isMath":true,"label":"A'","pos":[249,190.8125],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"R_0^i(X')_\\El","pos":[521,190.8125],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"R_0^i(X')_\\UU","pos":[521,372.8125],"zindex":0}},{"id":7,"label":{"isMath":true,"label":"H_iF_{i-1}(R_{i-1}^i X')","pos":[249,372.8125],"zindex":-10000}}],"sizeGrid":250,"title":"1"}]},"version":12}
|
||||
{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":8,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":9,"label":{"kind":"normal","label":"R_0^i(X)_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":10,"label":{"kind":"normal","label":"h","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.30000000000000004,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":11,"label":{"kind":"normal","label":"\\Cstr^X","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":4,"id":12,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":5,"id":13,"label":{"kind":"normal","label":"R_0^i(X')_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":4,"id":14,"label":{"kind":"normal","label":"h'","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.30000000000000004,"tail":"none"},"zindex":0},"to":7},{"from":7,"id":15,"label":{"kind":"normal","label":"\\Cstr^{X'}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":0,"id":16,"label":{"kind":"normal","label":"!","style":{"alignment":"left","bend":0,"color":"black","dashed":true,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":1},"to":4},{"from":1,"id":17,"label":{"kind":"normal","label":"R_0^i(f)_\\El","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":3,"id":18,"label":{"kind":"normal","label":"H_iF_{i-1}R_{i-1}^i f","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.10000000000000003,"tail":"none"},"zindex":0},"to":7},{"from":2,"id":19,"label":{"kind":"normal","label":"R_0^i(f)_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.6,"tail":"none"},"zindex":0},"to":6},{"from":14,"id":20,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":12},{"from":10,"id":21,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":8}],"nodes":[{"id":0,"label":{"isMath":true,"label":"A","pos":[125,115],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"R_0^i(X)_\\El","pos":[403,115],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"R_0^i(X)_\\UU","pos":[403,297],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i X","pos":[125,297],"zindex":-10000}},{"id":4,"label":{"isMath":true,"label":"A'","pos":[249,190.8125],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"R_0^i(X')_\\El","pos":[521,190.8125],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"R_0^i(X')_\\UU","pos":[521,372.8125],"zindex":0}},{"id":7,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i X'","pos":[249,372.8125],"zindex":-10000}}],"sizeGrid":250,"title":"1"}]},"version":12}
|
||||
@ -1 +1 @@
|
||||
{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":6,"label":{"kind":"normal","label":"\\Cstr^X","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":7,"label":{"kind":"normal","label":"(R_0^{i-1} (\\inj_1^{i-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":8,"label":{"kind":"normal","label":"H_iF_{i-1}\\inj_1^{i-1}","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":4,"id":9,"label":{"kind":"normal","label":"R_0^{i-1}(\\inj_1^{i-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":3,"id":10,"label":{"kind":"normal","label":"(H_iF_{i-1}\\inj_1^{i-1})^{-1}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":-3},"to":5},{"from":5,"id":11,"label":{"kind":"normal","label":"\\Cstr^X","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":0,"id":12,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":4,"id":13,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":3,"id":14,"label":{"kind":"normal","label":"\\Cstr^{X \\oplus L_0^i Y}","style":{"alignment":"left","bend":0.1,"color":"green","dashed":true,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2}],"nodes":[{"id":0,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i X","pos":[236.5,73.5],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"(R_0^i X)_\\UU","pos":[1013,73.8125],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^{i-1} (R_{i-1}^i X \\oplus L_0^{i-1} Y))_\\UU","pos":[1017.5,249.5],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}(R_{i-1}^i X \\oplus_{i-1} L_0^{i-1} Y)","pos":[236.5,249.5],"zindex":-10000}},{"id":4,"label":{"isMath":true,"label":"(R_0^i X)_\\UU","pos":[706,235.8125],"zindex":-10000}},{"id":5,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i X","pos":[556,234.8125],"zindex":-10000}}],"sizeGrid":147,"title":"1"}]},"version":12}
|
||||
{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":6,"label":{"kind":"normal","label":"\\Cstr^X","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":7,"label":{"kind":"normal","label":"(R_0^{i-1} (\\inj_\\tl^{i-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":8,"label":{"kind":"normal","label":"H_iF_{i-1}\\inj_1^{i-1}","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":4,"id":9,"label":{"kind":"normal","label":"R_0^{i-1}(\\inj_\\tl^{i-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":3,"id":10,"label":{"kind":"normal","label":"(H_iF_{i-1}\\inj_1^{i-1})^{-1}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":-3},"to":5},{"from":5,"id":11,"label":{"kind":"normal","label":"\\Cstr^X","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":0,"id":12,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":4,"id":13,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":3,"id":14,"label":{"kind":"normal","label":"\\Cstr^{X \\tl^i Y}","style":{"alignment":"left","bend":0.1,"color":"green","dashed":true,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2}],"nodes":[{"id":0,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i X","pos":[236.5,73.5],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"(R_0^i X)_\\UU","pos":[939,73.8125],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^{i-1} (R_{i-1}^i X \\tl^{i-1} Y))_\\UU","pos":[943.5,243.5],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}(R_{i-1}^i X \\tl^{i-1}Y)","pos":[236.5,243.5],"zindex":-10000}},{"id":4,"label":{"isMath":true,"label":"(R_0^i X)_\\UU","pos":[676,229.8125],"zindex":-10000}},{"id":5,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i X","pos":[526,228.8125],"zindex":-10000}}],"sizeGrid":147,"title":"1"}]},"version":12}
|
||||
@ -1 +1 @@
|
||||
{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":6,"label":{"kind":"normal","label":"H_iF_{i-1}\\inj^{i-1}_1","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":7,"label":{"kind":"normal","label":"\\Cstr^X","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":8,"label":{"kind":"normal","label":"H_iF_{i-1}\\{\\varphi_1 ; \\varphi_2\\}","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":2,"id":9,"label":{"kind":"normal","label":"(R_0^{i-1} \\inj_1^{i-1})_\\UU","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.6,"tail":"none"},"zindex":-1},"to":4},{"from":4,"id":10,"label":{"kind":"normal","label":"(R_0^i \\{\\varphi_1;\\varphi_2\\})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":3,"id":11,"label":{"kind":"normal","label":"\\Cstr^Z","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":1,"id":12,"label":{"kind":"normal","label":"R_{i-1}^i \\varphi_1 \\circ \\dash","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":2,"id":13,"label":{"kind":"normal","label":"(R_0^i \\varphi_1)_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5}],"nodes":[{"id":0,"label":{"isMath":true,"label":"H_iF_{i-1}(R_{i-1}^i X \\oplus L_0^{i-1} Y)","pos":[225,75],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i X","pos":[477,75],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i X)_\\UU","pos":[571,142.8125],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i Z","pos":[225,365],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"(R_0^{i-1} (R_{i-1}^i X \\oplus L_0^{i-1} Y))_\\UU","pos":[777,75],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[777,365],"zindex":0}}],"sizeGrid":150,"title":"1"}]},"version":12}
|
||||
{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":6,"label":{"kind":"normal","label":"H_i(F_{i-1}\\inj^{i-1}_1)^{-1}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":7,"label":{"kind":"normal","label":"\\Cstr^X","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":8,"label":{"kind":"normal","label":"H_iF_{i-1}\\{g,h\\}","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":2,"id":9,"label":{"kind":"normal","label":"(R_0^{i-1} \\inj_\\tl^{i-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":-1},"to":4},{"from":4,"id":10,"label":{"kind":"normal","label":"(R_0^i \\{g,h\\})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":3,"id":11,"label":{"kind":"normal","label":"\\Cstr^Z","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":1,"id":12,"label":{"kind":"normal","label":"H_iF_{i-1}R_{i-1}^ig","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":2,"id":13,"label":{"kind":"normal","label":"(R_0^i g)_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5}],"nodes":[{"id":0,"label":{"isMath":true,"label":"H_iF_{i-1}(R_{i-1}^i X \\tl^{i-1} Y)","pos":[225,69],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i X","pos":[495,69],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i X)_\\UU","pos":[645,69],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i Z","pos":[225,251],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"(R_0^{i-1} (R_{i-1}^i X \\tl^{i-1} Y))_\\UU","pos":[893,69],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[893,251],"zindex":0}}],"sizeGrid":150,"title":"1"}]},"version":12}
|
||||
@ -1 +1 @@
|
||||
{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":6,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":7,"label":{"kind":"normal","label":"(R_0^i Z)_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":8,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":9,"label":{"kind":"normal","label":"\\Cstr^Z","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":4,"id":10,"label":{"kind":"normal","label":"h","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":5,"id":11,"label":{"kind":"normal","label":"H_iF_{i-1}(R_{i-1}^i f \\circ \\inj_1)","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.10000000000000003,"tail":"hook"},"zindex":8},"to":3},{"from":4,"id":12,"label":{"kind":"normal","label":"\\left[R_{i-1}^i f \\circ \\inj_2\\right]_\\El","style":{"alignment":"left","bend":-0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":4,"id":13,"label":{"kind":"normal","label":"\\phi_{XYZ}(f)_2","style":{"alignment":"left","bend":0,"color":"black","dashed":true,"head":"default","kind":"normal","position":0.6,"tail":"none"},"zindex":0},"to":0}],"nodes":[{"id":0,"label":{"isMath":true,"label":"E(z)","pos":[290,174],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"(R_0^i Z)_\\El","pos":[490,174],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[490,304],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i Z","pos":[290,304],"zindex":-10000}},{"id":4,"label":{"isMath":true,"label":"A","pos":[100,100],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"H_iF_{i-1}X","pos":[101,224.8125],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12}
|
||||
{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":6,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":7,"label":{"kind":"normal","label":"(R_0^i Z)_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":8,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":9,"label":{"kind":"normal","label":"\\Cstr^Z","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":4,"id":10,"label":{"kind":"normal","label":"h","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":5,"id":11,"label":{"kind":"normal","label":"H_iF_{i-1}(R_{i-1}^i f \\circ \\inj_\\tl^{i-1})","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.10000000000000003,"tail":"hook"},"zindex":8},"to":3},{"from":4,"id":12,"label":{"kind":"normal","label":"\\left[R_{i-1}^i f \\circ \\inj_\\tl^{i-1}\\right]_\\El","style":{"alignment":"left","bend":-0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":4,"id":13,"label":{"kind":"normal","label":"\\phi_{XYZ}(f)_2","style":{"alignment":"left","bend":0,"color":"black","dashed":true,"head":"default","kind":"normal","position":0.6,"tail":"none"},"zindex":0},"to":0},{"from":8,"id":14,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":6}],"nodes":[{"id":0,"label":{"isMath":true,"label":"E(z)","pos":[290,174],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"(R_0^i Z)_\\El","pos":[490,174],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[490,304],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i Z","pos":[290,304],"zindex":-10000}},{"id":4,"label":{"isMath":true,"label":"A","pos":[100,100],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"H_iF_{i-1}X","pos":[101,224.8125],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12}
|
||||
@ -1 +1 @@
|
||||
{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":8,"label":{"kind":"normal","label":"\\text{H3'}","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.30000000000000004,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":9,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":10,"label":{"kind":"normal","label":"\\inj_2^0","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":11,"label":{"kind":"normal","label":"\\text{H1r}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":4,"id":12,"label":{"kind":"normal","label":"R_0^{i-1}\\left\\{g;\\eta_0^i \\circ L_0^{i-1} \\square \\right\\}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":2,"id":13,"label":{"kind":"normal","label":"(\\varepsilon_0^{i-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":6,"id":14,"label":{"kind":"normal","label":"(R_0^{i-1} \\inj_2^{i-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":6,"id":15,"label":{"kind":"normal","label":"R_0^{i-1}(\\eta_0^i \\circ L_0^{i-1} \\square)_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.7,"tail":"none"},"zindex":0},"to":5},{"from":2,"id":16,"label":{"kind":"normal","label":"\\Cstr^Z \\circ H_iF_{i-1}g","style":{"alignment":"right","bend":0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.30000000000000004,"tail":"none"},"zindex":0},"to":5},{"from":0,"id":17,"label":{"kind":"normal","label":"H_iF_{i-1}\\left\\{g;\\eta_0^i \\circ L_0^{i-1} \\square \\right\\}","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":7,"id":18,"label":{"kind":"normal","label":"\\Cstr^Z","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":1,"id":19,"label":{"kind":"normal","label":"H_iF_{i-1}g","style":{"alignment":"left","bend":0,"color":"red","dashed":false,"head":"default","kind":"normal","position":0.4,"tail":"none"},"zindex":0},"to":7}],"nodes":[{"id":0,"label":{"isMath":true,"label":"H_iF_{i-1}(X \\oplus L_0^{i-1}\\Hbar_\\bullet(X,Y))","pos":[210,64],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"H_iF_{i-1}X","pos":[329,129.8125],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\Hbar(X,Y)_\\UU","pos":[410,64.8125],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\left[R_0^{i-1} X \\oplus \\Hbar(X,Y)\\right]_\\UU","pos":[604.9999999999999,61.8125],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"R_0^{i-1}\\left(X \\oplus L_0^{i-1}\\Hbar(X,Y)\\right)","pos":[853,61.8125],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[853,303.8125],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"\\left[R_0^{i-1}L_0^{i-1}\\Hbar(X,Y)\\right]_\\UU","pos":[688,198.625],"zindex":0}},{"id":7,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i Z","pos":[210,306],"zindex":0}}],"sizeGrid":140,"title":"1"}]},"version":12}
|
||||
{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":7,"label":{"kind":"normal","label":"H_iF_{i-1}\\inj_\\tl^{i-1}","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":8,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":9,"label":{"kind":"normal","label":"(\\inj_2)_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":10,"label":{"kind":"normal","label":"((\\en_0^{i-1})^{-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":4,"id":11,"label":{"kind":"normal","label":"(R_0^{i-1}\\left\\{g;\\square \\right\\})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":2,"id":12,"label":{"kind":"normal","label":"\\square_\\UU","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"none","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":0,"id":13,"label":{"kind":"normal","label":"H_iF_{i-1}\\left\\{g;\\square \\right\\}","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":6,"id":14,"label":{"kind":"normal","label":"\\Cstr^Z","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":1,"id":15,"label":{"kind":"normal","label":"H_iF_{i-1}g","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.4,"tail":"none"},"zindex":0},"to":6}],"nodes":[{"id":0,"label":{"isMath":true,"label":"H_iF_{i-1}(X \\tl^{i-1} K_{H_iF_{i-1}}(X,Y))","pos":[210,64],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"H_iF_{i-1}X","pos":[492,64],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"K_{H_iF_{i-1}}(X,Y)_\\UU","pos":[616,64],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\left[R_0^{i-1} X \\oplus K_{H_iF_{i-1}}(X,Y)\\right]_\\UU","pos":[870,64],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"R_0^{i-1}\\left(X \\tl^{i-1} K_\\bullet(X,Y)\\right)_\\UU","pos":[870,158],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[870,250],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i Z","pos":[210,250],"zindex":0}}],"sizeGrid":140,"title":"1"}]},"version":12}
|
||||
@ -1 +1 @@
|
||||
{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\CC{{\\ensuremath{\\mathcal{C}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":6,"label":{"kind":"normal","label":"","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":7,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"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":1,"id":9,"label":{"kind":"normal","label":"H_i\\eta^{FG}_{i-1} \\circ g","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":4,"id":10,"label":{"kind":"normal","label":"H_iF_{i-1}\\inj_0^{i-1}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":0,"id":11,"label":{"kind":"normal","label":"g","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":5,"id":12,"label":{"kind":"normal","label":"H_i\\text{HR}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4}],"nodes":[{"id":0,"label":{"isMath":true,"label":"B","pos":[100,100],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"B","pos":[300,100],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"A","pos":[678,100],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}(G_{i-1}X \\oplus L_0^{i-1}\\Hbar_\\bullet(G_{i-1}X,(B,g)))","pos":[678,211],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"H_iF_{i-1}G_{i-1}X","pos":[300,211],"zindex":-10000}},{"id":5,"label":{"isMath":true,"label":"H_iX","pos":[100,211],"zindex":-10000}}],"sizeGrid":200,"title":"1"}]},"version":12}
|
||||
{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\CC{{\\ensuremath{\\mathcal{C}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":6,"label":{"kind":"normal","label":"","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":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"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":1,"id":9,"label":{"kind":"normal","label":"H_i\\eta^{FG}_{i-1} \\circ g","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":4,"id":10,"label":{"kind":"normal","label":"H_iF_{i-1}\\inj_0^{i-1}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":0,"id":11,"label":{"kind":"normal","label":"g","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":5,"id":12,"label":{"kind":"normal","label":"H_i\\text{HR}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":4}],"nodes":[{"id":0,"label":{"isMath":true,"label":"B","pos":[100,100],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"B","pos":[300,100],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"A","pos":[678,100],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}(G_{i-1}X \\oplus L_0^{i-1}\\Hbar_\\bullet(G_{i-1}X,(B,g)))","pos":[678,211],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"H_iF_{i-1}G_{i-1}X","pos":[300,211],"zindex":-10000}},{"id":5,"label":{"isMath":true,"label":"H_iX","pos":[100,211],"zindex":-10000}}],"sizeGrid":200,"title":"1"}]},"version":12}
|
||||
File diff suppressed because one or more lines are too long
1
Report/graphs/TlConstructor.json
Normal file
1
Report/graphs/TlConstructor.json
Normal file
@ -0,0 +1 @@
|
||||
{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\CC{{\\ensuremath{\\mathcal{C}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":4,"label":{"kind":"normal","label":"H_i(F_{i-1}\\inj_\\tl^{i-1})^{-1}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":5,"label":{"kind":"normal","label":"\\Cstr^X","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":6,"label":{"kind":"normal","label":"(R_0^{i-1}\\inj_\\tl^{i-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3}],"nodes":[{"id":0,"label":{"isMath":true,"label":"H_iF_{i-1}(R_{i-1}^i X \\tl^{i-1} Y)","pos":[177,59],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"H_iF_{i-1}(R_{i-1}^i X)","pos":[177,135],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i X)_\\UU","pos":[177,207],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"(R_0^{i-1} (R_{i-1}^i X \\tl^{i-1} Y))_\\UU","pos":[177,285],"zindex":0}}],"sizeGrid":118,"title":"1"}]},"version":12}
|
||||
1
Report/graphs/TlUniversal.json
Normal file
1
Report/graphs/TlUniversal.json
Normal file
@ -0,0 +1 @@
|
||||
{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\CC{{\\ensuremath{\\mathcal{C}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":7,"label":{"kind":"normal","label":"\\inj_\\tl^{i-1}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":8,"label":{"kind":"normal","label":"\\{g,h\\}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":9,"label":{"kind":"normal","label":"g","style":{"alignment":"left","bend":0.1,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":3,"id":10,"label":{"kind":"normal","label":"(\\en^i_0)^{-1}","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":4,"id":11,"label":{"kind":"normal","label":"R_0^i\\{g,h\\}","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":3,"id":12,"label":{"kind":"normal","label":"\\inj_2","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":6,"id":13,"label":{"kind":"normal","label":"h","style":{"alignment":"left","bend":-0.1,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5}],"nodes":[{"id":0,"label":{"isMath":true,"label":"X","pos":[100,94],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"X \\tl^i Y","pos":[300,94],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"Z","pos":[300,318],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"R_0^{i-1}X \\oplus Y","pos":[514,94],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"R_0^{i-1}(X \\tl^i Y)","pos":[515,188.8125],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"R_0^i Z","pos":[514,318],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"Y","pos":[714,94],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12}
|
||||
1
Report/graphs/Wdef.json
Normal file
1
Report/graphs/Wdef.json
Normal file
@ -0,0 +1 @@
|
||||
{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\CC{{\\ensuremath{\\mathcal{C}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":5,"label":{"kind":"normal","label":"(H_iF_{i-1}\\inj_\\tl^{i-1})^{-1}","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":6,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":7,"label":{"kind":"normal","label":"\\inj_2","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":8,"label":{"kind":"normal","label":"((\\en_0^{i-1})^{-1})_\\UU","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":4}],"nodes":[{"id":0,"label":{"isMath":true,"label":"H_iF_{i-1}(X \\tl^{i-1} K_{H_iF_{i-1}}(X,Y))) ","pos":[230,46],"zindex":0}},{"id":1,"label":{"isMath":true,"label":" H_iF_{i-1}X","pos":[230,138],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\left(K_{H_iF_{i-1}}(X,Y)\\right)_\\UU","pos":[230,204],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\left(R_0^{i-1}X \\oplus K_{H_iF_{i-1}}(X,Y)\\right)_\\UU","pos":[230,296],"zindex":0}},{"id":4,"label":{"isMath":true,"label":" \\left(R_0^{i-1}(X \\tl^{i-1}K_{H_iF_{i-1}}(X,Y))\\right)_\\UU","pos":[230,388],"zindex":0}}],"sizeGrid":92,"title":"1"}]},"version":12}
|
||||
@ -49,7 +49,6 @@
|
||||
|
||||
\usepackage[textheight=0.75\paperheight]{geometry}
|
||||
|
||||
\usepackage{csquotes}
|
||||
\usepackage[lighttt]{lmodern}
|
||||
\usetikzlibrary{shapes.geometric,positioning,backgrounds}
|
||||
|
||||
@ -65,8 +64,6 @@
|
||||
\newcommand{\longdash}{\:\textrm{---}\:}
|
||||
\newcommand\hole{\left[\raisebox{-0.25ex}{\scalebox{1.2}{$\cdot$}}\right]}
|
||||
\newcommand\bracket[1]{\!\left[#1\right]}
|
||||
\newcommand{\ssi}{\quad\text{\underline{ssi}}\quad}
|
||||
\newcommand\eng[1]{\textit{\foreignlanguage{english}{#1}}}
|
||||
\newcommand\spacebar{\;|\;}
|
||||
\def\nDownarrow{\not\mspace{1mu}\Downarrow}
|
||||
\let\pprec\preccurlyeq
|
||||
@ -114,8 +111,11 @@
|
||||
\newcommand\FamSet{{\ensuremath{\operatorname{\mathcal{F}am\mathcal{S}et}}}}
|
||||
\newcommand\Hom{{\ensuremath{\operatorname{\mathcal{H}om}}}}
|
||||
\newcommand\this{{\ensuremath{\operatorname{\texttt{this}}}}}
|
||||
\newcommand\Hbar{{\ensuremath{\overline{H}}}}
|
||||
\newcommand\Hbar{{\ensuremath{K}}}
|
||||
\newcommand\one{{\ensuremath{\mathbf{1}}}}
|
||||
\newcommand\dash{{\;\textrm{---}\;}}
|
||||
\renewcommand\enquote[1]{``#1''}
|
||||
\newcommand\tl{{\triangleleft}}
|
||||
|
||||
\DeclareMathOperator{\inj}{inj}
|
||||
\DeclareMathOperator{\id}{id}
|
||||
|
||||
78
Report/synthese.tex
Normal file
78
Report/synthese.tex
Normal file
@ -0,0 +1,78 @@
|
||||
\documentclass[11pt]{article}
|
||||
|
||||
\usepackage[francais]{babel}
|
||||
\usepackage{csquotes}
|
||||
\usepackage{xcolor}
|
||||
|
||||
% \setlength{\parskip}{0.3\baselineskip}
|
||||
|
||||
\newcommand\question[1]{\textbf{\textcolor{orange}{#1}}}
|
||||
%\newcommand\question[1]{}
|
||||
|
||||
\begin{document}
|
||||
|
||||
\title{Sémantique catégorique de la réduction des GATs en GATs à deux sortes}
|
||||
|
||||
\author{Samy Avrillon, encadré par Ambroise Lafont\\
|
||||
\small Équipe PARTOUT, Laboratoire d'Informatique de l'École Polytechnique (LIX)}
|
||||
|
||||
\maketitle
|
||||
|
||||
\pagestyle{empty} %
|
||||
\thispagestyle{empty}
|
||||
|
||||
|
||||
\subsection*{Le contexte général}
|
||||
|
||||
Les théories algébriques généralisées (ou GAT) sont des objects syntaxiques introduits en 1986 par Cartmell qui permettent la description d'objects algébriques, comme une généralisation des types inductifs de théorie des types.
|
||||
|
||||
Un GAT est constitué d'une liste de \enquote{sortes} décrivant les ensembles, généralement suivie d'une liste de \enquote{constructeurs}.
|
||||
|
||||
\question{De quoi s'agit-il ?}
|
||||
\question{D'où vient-il ?}
|
||||
\question{Quels sont les travaux déjà accomplis dans ce domaine dans le monde ?}
|
||||
|
||||
\subsection*{Le problème étudié}
|
||||
|
||||
Il existe un processus qui permet de transformer n'importe quel GAT en un GAT avec seulement deux sortes. Cette transformation a été utilisée par Philippo Sestini dans sa thèse, afin de restreindre son sujet d'étude. Cependant, il n'a pas été prouvé que cette transformation ne réduisait pas la généralité de sa thèse.
|
||||
|
||||
\question{Quelle est la question que vous avez abordée ?}
|
||||
\question{Pourquoi est-elle importante, à quoi cela sert-il d'y répondre ?}
|
||||
\question{Est-ce un nouveau problème ?}
|
||||
\question{Si oui, pourquoi êtes-vous le premier chercheur de l'univers à l'avoir posée ?}
|
||||
\question{Si non, pourquoi pensiez-vous pouvoir apporter une contribution originale ?}
|
||||
|
||||
\subsection*{La contribution proposée}
|
||||
|
||||
Durant ce stage, j'ai apporté une formalisation sémantique de la transformation. J'ai décrit formellement la transformation de modèles du GAT original en modèle du GAT transformé, mais également la transformation réciproque. J'ai également prouvé certaines propriétés de cette transformation.
|
||||
|
||||
\question{Qu'avez vous proposé comme solution à cette question ?
|
||||
Attention, pas de technique, seulement les grandes idées !
|
||||
Soignez particulièrement la description de la démarche \emph{scientifique}.}
|
||||
|
||||
\subsection*{Les arguments en faveur de sa validité}
|
||||
|
||||
La preuve a été faite avec la sémantique en essayant de généraliser les objets utilisés au maximum.
|
||||
|
||||
Cette preuve valide la conjecture établie par Sestini dans sa thèse.
|
||||
|
||||
\question{Qu'est-ce qui montre que cette solution est une bonne solution ?}
|
||||
\question{Des expériences, des corollaires ?}
|
||||
\question{Commentez la \emph{robustesse} de votre proposition :
|
||||
comment la validité de la solution dépend-elle des hypothèses de travail ?}
|
||||
|
||||
\subsection*{Le bilan et les perspectives}
|
||||
|
||||
Nous avons formalisé la transformation sémantiquement, ce qui permet de gagner en généralité.
|
||||
Cette tranformation a été prouvée, et permet notamment de restreindre une étude aux seuls GATs à deux sortes.
|
||||
|
||||
Cette transformation met en correspondanc de façon intéressante les \enquote{déclarations de sortes} et les \enquote{constructeurs}, ce qui permetterai évenuellement de les recouper dans une même notion.
|
||||
|
||||
Nous avons également de quoi réfléchir à une généralisation des GATs qui décriraient par exemple des types mutuellement inductif, mais aussi d'autres objets plus \enquote{exotiques}. Il y a du travail à les étudier, et à observer l'effet de la transformation sur ces objets.
|
||||
|
||||
\question{Et après ? En quoi votre approche est-elle générale ?}
|
||||
\question{Qu'est-ce que votre contribution a apporté au domaine ?}
|
||||
\question{Que faudrait-il faire maintenant ?}
|
||||
\question{Quelle est la bonne \emph{prochaine} question ?}
|
||||
|
||||
\end{document}
|
||||
Loading…
x
Reference in New Issue
Block a user