Fin de la réharmonisation des preuves du document principal
This commit is contained in:
parent
b3af010882
commit
854aef6a88
GPG Key ID:
0220AC4A3D6A328B
@ -27,11 +27,11 @@
|
||||
|
||||
A Generalized Algebraic Theory (or GAT), first introduced by Cartmell \cite{CartmellGATs}, is a syntactic specification of an algebraic structure. From a GAT, one can define a category of models describing the models of the algebraic structure.
|
||||
A GAT typically starts with a sort specification i.e. a list of sort declarations, eventually followed by a list of constructors.
|
||||
In this document, we will not ask ourselves about the specific syntax of GATs, a \enquote{vague} definition is enough.
|
||||
In this document, we will not ask ourselves about the specific syntax of GATs. A \enquote{vague} definition is enough to understand the rest of the document.
|
||||
|
||||
\paragraph{Sort specification}
|
||||
|
||||
A sort specification is a list of \emph{sort declarations} that are defined with \emph{parameters} with $\Set$ as its codomain.
|
||||
A sort specification is a list of \emph{sort declarations}, composed of \emph{parameters} and $\Set$ as their codomain.
|
||||
|
||||
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.
|
||||
|
||||
@ -47,7 +47,7 @@
|
||||
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. Those constructors specify elements of the sets contained in the model, previously defined by the sort declaration.
|
||||
We can also add constructors to a sort specification. They are composed as parameters (the same kind as sort declarations) and a codomain which is a sort defined in a previous sort declaration. 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}
|
||||
@ -68,7 +68,7 @@
|
||||
\vspace{1em}
|
||||
\begin{tabular}{p{0.37\textwidth}|p{0.5\textwidth}}
|
||||
$\UU : \Set$ & The set of sorts \\
|
||||
$\El : \mathcal{O} \to \Set$ & For every sort object $o$ in the set of sorts, a set called $\El(o)$ of objects corresponding to the sort object.
|
||||
$\El : \mathcal{O} \to \Set$ & For every sort object $o$ in the set of sorts, a set called $\El(o)$ of objects corresponding to the sort object $o$.
|
||||
\end{tabular}
|
||||
\vspace{1em}
|
||||
|
||||
@ -89,17 +89,17 @@
|
||||
$\dots$
|
||||
\end{tabular}
|
||||
|
||||
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.
|
||||
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{Ç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.
|
||||
Many instances of multi-sorted IITs [IITs are a variant of GATs] can be reduced to equivalent two-sorted IITs, via a systematic reduction method originally observed by Zongpu (Szumi) Xie. We are not aware of a formal proof of this construction for arbitrary IITs, but we conjecture that it does apply to all instances of induction-induction and consequently that it shows two-sorted IITs are enough to represent any specifiable IIT.
|
||||
\end{quote}
|
||||
|
||||
\paragraph{Goal}
|
||||
|
||||
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.
|
||||
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 \enquote{two-sortified} 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.
|
||||
|
||||
@ -114,37 +114,46 @@
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
|
||||
\section{Construction of the coreflection}
|
||||
\section{Constructing the coreflection}
|
||||
|
||||
\paragraph{Structure of the proof}
|
||||
|
||||
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}.
|
||||
|
||||
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}.
|
||||
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 (\autoref{sec:constructingCategory}).
|
||||
|
||||
At the $i$-th recursion step, we will build the following objects :
|
||||
\begin{itemize}
|
||||
\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 A functor $R_{i-1}^i : \BB_i \to \BB_{i-1}$, taking track of the fixed sort specification of the transformed GAT. \inlinetodo{Mal Dit, est-ce nécessaire ?}
|
||||
|
||||
Those functors compose themselves into a functor $R_0^i : \BB_i \to \BB_0$.
|
||||
\[
|
||||
R_0^i = R^1_0 \circ \dots \circ R_{i-1}^i
|
||||
\]
|
||||
\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:
|
||||
\label{sec:tlUniversalProperty}
|
||||
|
||||
\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 :/}
|
||||
We will construct later that $\tl^0$ is $\oplus$, the coproduct of the category $\BB_0 = \TSet$. The second injector of this coproduct is denoted as $\inj_2$.
|
||||
|
||||
\todo{Faut-il remplacer $\en$ par $\en^{-1}$, vu qu'on utilise $\en^{-1}$ partout ?}
|
||||
|
||||
\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
|
||||
\item A proof that $F_i\inj_\tl^i$ is an isomorphism
|
||||
\end{itemize}
|
||||
|
||||
Here is a figure that describes the recursive construction of some of the above objects
|
||||
@ -177,17 +186,15 @@
|
||||
|
||||
A morphism $(Y,f) \to (Y',f')$ is a morphism $g : Y \to Y'$ such that $g \circ f = f'$.
|
||||
|
||||
We can deduce a functor $\left(\mathcal{C}/\dash\right) : \mathcal{C} \to \Cat$ from this construction.
|
||||
We can define a functor $\left(\mathcal{C}/\dash\right) : \mathcal{C} \to \Cat$ from this construction.
|
||||
|
||||
If the category $\mathcal{C}$ is $\Set$, we have the equivalence $\Set/X \simeq \Set^X$.
|
||||
|
||||
We will often concatenate the two method above to create from a category $\mathcal{C}$ and a functor $H : \mathcal{C} \to \Set$ a new category $(X : \mathcal{C}) \times \left(\Set\middle/H(X)\right)$.
|
||||
|
||||
\paragraph{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.
|
||||
\label{sec:categoryOfModelsOfTwoSorts}
|
||||
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 another category : $\TSet$, the category 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
|
||||
@ -196,6 +203,9 @@
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
|
||||
This category is equivalent to the catgegory $\FamSet$ with an equivalence that is given in \inlinetodo{annex reference}, with the following equivalence:
|
||||
\todo{Choose whether to tell the equivalence}
|
||||
|
||||
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}
|
||||
@ -204,13 +214,11 @@
|
||||
|
||||
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{$K$ functor}
|
||||
|
||||
\paragraph{$\Hbar$ functor}
|
||||
|
||||
Where $\Hbar_A$ is a functor $(X:C) \times (\Set/A(X)) \to \TSet$ defined as
|
||||
We define a functor $K : (X:C) \times (\Set/A(X)) \to \TSet$ defined as follows
|
||||
\[
|
||||
\Hbar_X(X,(Y,f)) = \TSetObject{Y}{f}{A(X)}
|
||||
K_X(X,(Y,f)) = \TSetObject{Y}{f}{A(X)}
|
||||
\]
|
||||
The morphisms are translated as-is.
|
||||
|
||||
@ -219,18 +227,23 @@
|
||||
\end{remark}
|
||||
|
||||
\subsection{Initialization}
|
||||
In the first step, corresponding to an empty sort specification, the objects are defined as follows:
|
||||
In this subsection, we will build the objects of the first step of our induction. This will correspond to the empty sort specification.
|
||||
|
||||
\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 $\CC_i$ is $\one$, the category with only one object and one trivial 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 (see \autoref{sec:categoryOfModelsOfTwoSorts} for its description)
|
||||
\item $\tl^0 : \BB_0 \times \BB_0 \to \BB_0$ is the coproduct $\oplus$ 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. Please note that there is only a second injector for the initial step of the recursion.
|
||||
|
||||
The universal property of $\tl^0$ is that of the coproduct.
|
||||
|
||||
\todo{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
|
||||
\item With $\star$ being the only 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 ?}
|
||||
Therefore, we have that $F_0 \vdash G_0$.
|
||||
\todo{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}
|
||||
@ -238,6 +251,7 @@
|
||||
|
||||
\subsection{Constructing the categories}
|
||||
|
||||
\label{sec:constructingCategory}
|
||||
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.
|
||||
|
||||
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.
|
||||
@ -250,31 +264,45 @@
|
||||
|
||||
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)
|
||||
\CC_i := (X : \CC_{i-1}) \times \left(\Set\middle/H_i(X)\right)
|
||||
\]
|
||||
and where $H_i$ is the specific functor described above.
|
||||
|
||||
\todo{Do we need this functor to be representable. If so, precise it}
|
||||
\todo{Do we need this functor to be representable ? If so, precise it}
|
||||
|
||||
\paragraph{$H_i$ functors for our Type Theory example}
|
||||
\paragraph{An example of $H_i$ functors}
|
||||
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)
|
||||
\boxed{\Con : \Set}
|
||||
\]
|
||||
which corresponds to the fact that $\Con$ takes no parameter.
|
||||
We begin with the following functor, corresponding to the sort declaration above
|
||||
\[
|
||||
H_1(\star) = 1 \in \operatorname{Obj}(\Set)
|
||||
\]
|
||||
|
||||
This corresponds to the fact that $\Con$ takes no parameter.
|
||||
|
||||
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$, corresponding to the sort declaration $\boxed{\Ty : (\Gamma : \Con) \to \Set}$ (this means, that types need \emph{one} context to be built).
|
||||
\[
|
||||
\boxed{\Ty : (\Gamma : \Con) \to \Set}
|
||||
\]
|
||||
|
||||
Therefore $\CC_2 = (X:\Set) \times (\Set/X) \simeq (X:\Set) \times (\Set^X) = \FamSet$, a model is a family of sets.
|
||||
Then, we take the functor $H_2(X_\Con) = X_\Con$, corresponding to the sort declaration above. This functor means that types need \emph{one} context to be built.
|
||||
|
||||
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).
|
||||
Therefore $\CC_2 = (X:\Set) \times (\Set/X) \simeq (X:\Set) \times (\Set^X) = \FamSet$, a model is a family of sets, as expected.
|
||||
|
||||
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)$
|
||||
\[
|
||||
\boxed{\Tm : (\Delta : \Con) \to (A : \Ty\;\Delta) \to \Set}
|
||||
\]
|
||||
|
||||
Finally, we take the functor $H_3(X_\Con,X_\Ty) = \sum_{\Gamma : X_\Con}X_\Ty(\Gamma)$. It means that terms need \emph{one} context, and \emph{one} type of that context.
|
||||
|
||||
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$}
|
||||
|
||||
We construct the category $\BB_i$ as follows.
|
||||
@ -282,12 +310,12 @@
|
||||
An object of $\BB_i$ is
|
||||
\begin{itemize}
|
||||
\item an object $X$ of $\BB_{i-1}$
|
||||
\item a \enquote{sort constructor} $\Cstr$ as a function $H_iF_{i-1}X \to (R_0^{i-1}X)_\UU$
|
||||
\item a \enquote{sort constructor} $\Cstr^X$ 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$ 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.
|
||||
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 have defined at the previous induction step.
|
||||
\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$.
|
||||
If we have an object $X$ of $\BB_i$, the first component is denoted as $R_{i-1}^iX \in \operatorname{Obj}(\BB_{i-1})$, and the second component is denoted as $\Cstr^X : R_{i-1}^i X \to (R_0^iX)_\UU$.
|
||||
|
||||
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.
|
||||
|
||||
@ -306,7 +334,7 @@
|
||||
|
||||
\subsection{Constructing the functors}
|
||||
|
||||
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.
|
||||
The adjunction $F_i \vdash G_i$ is built using the two functors from the adjunction $F_{i-1} \vdash G_{i-1}$ defined in the previous induction step. We use them to define the first part of the adjunction, and we compose them with two adjoint functors $W$ and $E$ that we will define in this section. The overall construction for this induction step is as follows:
|
||||
|
||||
\begin{center}
|
||||
% YADE DIAGRAM G2.json
|
||||
@ -317,20 +345,28 @@
|
||||
|
||||
Where
|
||||
\[
|
||||
(F_{i-1} \times \id)(X,(Y,y)) = (F_{i-1}X,(Y,y))
|
||||
(F_{i-1} \times \id)(X,\underset{y : Y \to F_{i-1}(X)}{(Y,y)}) = (F_{i-1}X,\underset{y : Y \to F_{i-1}X}{(Y,y)})
|
||||
\]
|
||||
\[
|
||||
(F_{i-1} \times \id)(f,g) = (F_{i-1}f,g)
|
||||
\]
|
||||
and
|
||||
\[
|
||||
(G_{i-1} \times \id)(X,(Y,y)) = (G_{i-1}X,(Y,H_i\eta_{i-1} \circ y))
|
||||
(G_{i-1} \times (H_i\eta_{i-1} \circ \dash))(X,\underset{y : Y \to H_iX}{(Y,y)}) = (G_{i-1}X,\underset{Y : Y \to H_i X \to H_iF_{i-1}(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}
|
||||
\[
|
||||
(G_{i-1} \times (H_i\eta_{i-1} \circ \dash))(f,g) = (G_{i-1}f,g)
|
||||
\]
|
||||
$\eta_{i-1} : X \to F_{i-1}G_{i-1}X$ denotes the unit of the adjunction $F_{i-1} \vdash G_{i-1}$.
|
||||
|
||||
These equations define two functors, that create an adjunction, as $F_{i-1} \vdash G_{i-1}$ is an adjuntion, and the action on morphism is that of $F_{i-1}$ and $G_{i-1}$.
|
||||
|
||||
\todo{Est-ce que c'est clair ? Besoin de plus de preuve ? Prouver que c'est des foncteurs ? Une adjonction ?}
|
||||
|
||||
|
||||
\subsubsection{W definition}
|
||||
|
||||
We define a functor $W : \left(X : \BB_{i-1}\right) \times \Set/H_iF_{i-1}X \to \BB_{i}$
|
||||
We define a functor $W : \left(\left(X : \BB_{i-1}\right) \times \Set/H_iF_{i-1}X\right) \to \BB_{i}$
|
||||
|
||||
The action on objects is as follows:
|
||||
\[
|
||||
@ -345,12 +381,12 @@
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
|
||||
The action on a morphism $(g,h)$ from $(X,(Y,y))$ to $(X',(Y',y'))$ is the following:
|
||||
The action on a morphism $(g,h)$ from $(X,Y)$ to $(X',Y')$ is the following:
|
||||
\[
|
||||
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.
|
||||
It is indeed a morphism of $\BB_{i}$ as it makes the following diagram commute.
|
||||
|
||||
\begin{center}
|
||||
% YADE DIAGRAM D2.json
|
||||
@ -358,6 +394,8 @@
|
||||
\input{graphs/D2.tex}
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
|
||||
\todo{Fixer l'affichage de ce diagramme}
|
||||
|
||||
\subsubsection{E definition}
|
||||
|
||||
@ -376,6 +414,8 @@
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
|
||||
\todo{Faut justifier qu'on puisse faire un pullback, non ? C'est quoi l'explication la moins complexe ?}
|
||||
|
||||
The action on a morphism $f$ from $X$ to $X'$ is defined as $E(f) = (R_{i-1}^i f, !)$, with $!$ being the only morphism making the following diagram commute (thanks to the pullback property):
|
||||
|
||||
\begin{center}
|
||||
@ -387,22 +427,29 @@
|
||||
|
||||
\subsection{Proof of the adjunction}
|
||||
|
||||
We prove that $(W,E)$ make an adjunction showing that there is a natural isomorphism between $\Hom$ sets in both categories.
|
||||
In this subsection, we prove that $(W,E)$ make an adjunction by showing that there is a natural isomorphism between $\Hom$ sets in both categories.
|
||||
|
||||
We want to construct for each $(X,Y)$ in $(X : \BB_{i-1}) \times (\Set/H_iF_{i-1}X)$ and $Z$ in $\BB_i$, an isomorphism $\phi_{XYZ}$.
|
||||
We want to construct for each $(X,Y)$ in $(X : \BB_{i-1}) \times (\Set/H_iF_{i-1}X)$ and $Z$ in $\BB_i$, a natural isomorphism $\phi_{XYZ}$.
|
||||
|
||||
\[
|
||||
\phi_{XYZ} : \Hom(W(X,Y),Z) \to \Hom((X,Y),E(Z))
|
||||
\]
|
||||
|
||||
I will give the construction of the isomorphisms and its inverse, the proofs are given in \autoref{apx:phi-WE-isnat}.
|
||||
I will present how the isomorphisms and its inverse are constructed. The proof that $\phi_{XYZ}$ and $\phi_{XYZ}^{-1}$ are inverse one of the other, and that they are natural are given in \autoref{apx:phi-WE-isnat}.
|
||||
|
||||
\subsubsection{Constructing $\phi_{XYZ}$}
|
||||
|
||||
Let $f$ be in $\Hom(W(X,Y),Z)$.
|
||||
We want to construct $\phi_{XYZ}(f) : (X,Y) \to E(Z)$.
|
||||
|
||||
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 first component of $\phi_{XYZ}(f)$ is defined as the following composition:
|
||||
|
||||
\begin{center}
|
||||
% YADE DIAGRAM PhiXYZFirstComponent.json
|
||||
% GENERATED LATEX
|
||||
\input{graphs/PhiXYZFirstComponent.tex}
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
|
||||
The second component is defined through the universal property of the pullback defined by $E(Z)$ according to the following diagram:
|
||||
|
||||
@ -417,13 +464,13 @@
|
||||
|
||||
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 \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}
|
||||
The morphism $\phi^{-1}_{XYZ}(g,h)$ of $\BB_i$ from $W(X,Y)$ to $Z$ is 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 make a specific diagram commute. We build this morphism using the universal property of $\tl^{i-1}$, stated in \autoref{sec:tlUniversalProperty}
|
||||
|
||||
\[
|
||||
\phi^{-1}_{XYZ}(g,h) := \left\{g ; \varepsilon_0^i \circ L_0^{i-1} \square \right\}
|
||||
\phi^{-1}_{XYZ}(g,h) := \left\{g ; \square \right\}
|
||||
\]
|
||||
|
||||
Where $\square$ is a morphism $\Hbar (X,Y) \to R_0^i Z$ in $\TSet$ defined by the following diagram:
|
||||
Where $\square$ is a morphism $K_{H_iF_{i-1}} (X,Y) \to R_0^i Z$ in $\TSet$ defined by the following diagram:
|
||||
|
||||
\begin{center}
|
||||
% YADE DIAGRAM D7.json
|
||||
@ -432,7 +479,7 @@
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
|
||||
This is indeed a morphism of $\BB_i$ from $W(X,Y)$ to $Z$ as it makes the following diagram commute
|
||||
Finally, we check that $\phi^{-1}_{XYZ}(g,h)$ is a morphism of $\BB_i$ from $W(X,Y)$ to $Z$, i.e. that it makes the following diagram commute:
|
||||
|
||||
\begin{center}
|
||||
% YADE DIAGRAM D8.json
|
||||
@ -440,15 +487,23 @@
|
||||
\input{graphs/D8.tex}
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
|
||||
In order to complete this proof, we need to show that
|
||||
\begin{itemize}
|
||||
\item $\phi_{XYZ}^{-1} \circ \phi_{XYZ} (f) = f$
|
||||
\item $\phi_{XYZ} \circ \phi_{XYZ}^{-1} (g,h) = (g,h)$
|
||||
\item $\phi_{XYZ}$ is natural.
|
||||
\end{itemize}
|
||||
|
||||
We show in \autoref{apx:phi-WE-isnat} that $\phi_{XYZ}$ and $\phi_{XYZ}^{-1}$ do indeed make a natural isomorphism.
|
||||
The proofs of these statements are given in \autoref{apx:phi-WE-isnat}.
|
||||
|
||||
|
||||
|
||||
\subsubsection{Properties of the adjunction}
|
||||
We have proven that $F_i \vdash G_i$ make a reflection, i.e. that $F_iG_i \cong \Id_{\CC_i}$.
|
||||
\subsubsection{Coreflection}
|
||||
|
||||
We have proven that this newly created adjunction $F_i \vdash G_i$ create a coreflection. It means that $F_iG_i \cong \Id_{\CC_i}$, or equivalently that $G_i is full and faithful$.
|
||||
|
||||
The proof is given in \autoref{apx:FG-refl}.
|
||||
The proof is that statement is given in \autoref{apx:FG-refl}.
|
||||
|
||||
\subsection{Other objects}
|
||||
\subsubsection{Constructing $\tl^i$}
|
||||
@ -458,7 +513,7 @@
|
||||
\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 \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)
|
||||
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)
|
||||
\]
|
||||
|
||||
The constructor goes as follows:
|
||||
@ -485,8 +540,8 @@
|
||||
\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.
|
||||
We will now show that that the universal property stated in \autoref{sec:tlUniversalProperty} holds.
|
||||
To that end, we take two objects $X$ and $Z$ in $\BB_i$, $Y$ in $\BB_0$, a morphism $g : X \to Z$ in $\BB_i$ and a morphism $h : Y \to R_0^iZ$ in $\BB_0$. We want to build a morphism $\{g,h\}$ of $\BB_i$ such that the following two diagrams commute.
|
||||
|
||||
\begin{center}
|
||||
% YADE DIAGRAM TlUniversal.json
|
||||
@ -495,7 +550,7 @@
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
|
||||
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:
|
||||
We define $\{g ; h\}_i = \{R_{i-1}^i g ; h\}_{i-1}$. This is a morphism of $\BB_i$ as it makes the following diagram commute:
|
||||
|
||||
\begin{center}
|
||||
% YADE DIAGRAM D5.json
|
||||
@ -510,13 +565,15 @@
|
||||
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.
|
||||
Morphisms $\BB_{i}$ are morphisms of $\BB_{i-1}$ that follows some equations, and composition is the same. Moreover, we know from the definition above that $R_{i-1^i} \inj_\tl^i := \inj_\tl^{i-1}$.
|
||||
|
||||
So, we just need to know that $R_{i-1}^i(F_{i-1}\inj_\tl^i)$ is an isomorphism.
|
||||
|
||||
We also know from the last induction step that $F_{i-1}\inj_1^{i-1}$ is an isomorphism.
|
||||
\[
|
||||
(X,\Cstr) \oplus L_0^iY \simeq (X \oplus L_0^{i-1}Y, (R_0^{i-1}\inj_1^{i-1})_\UU \circ \Cstr \circ (H_iF_{i-1}\inj_1^{i-1})^{-1})
|
||||
R_{i-1}^iF_i\inj_\tl^i = \left[(F_{i-1} \times \id) (E(\inj_\tl^i))\right]_1 = \left[(F_{i-1} \times \id) (R_{i-1}^i \inj_\tl^i,!)\right]_1 = F_{i-1} \inj_\tl^{-1}
|
||||
\]
|
||||
|
||||
|
||||
And we know from the previous induction step that $F_{i-1}\inj_\tl^{i-1}$ is an isomorphism. Therefore, $F_i\inj_\tl^i$ is an isomorphism.
|
||||
|
||||
\section{Misc}
|
||||
|
||||
@ -902,6 +959,19 @@
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
File diff suppressed because one or more lines are too long
@ -1 +1 @@
|
||||
{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":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}
|
||||
{"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.1,"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.1,"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":"left","bend":-0.2,"color":"black","dashed":false,"head":"none","kind":"normal","position":0.5,"tail":"none"},"zindex":-1},"to":3},{"from":2,"id":13,"label":{"kind":"normal","label":"(R_0^i g)_\\UU","style":{"alignment":"right","bend":0.2,"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":[375,125],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i X","pos":[525,75],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i X)_\\UU","pos":[675,75],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i Z","pos":[375,275],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"(R_0^{i-1} (R_{i-1}^i X \\tl^{i-1} Y))_\\UU","pos":[825,125],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[825,275],"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_\\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}
|
||||
{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":10,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":11,"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":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":3},{"from":3,"id":13,"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":14,"label":{"kind":"normal","label":"y","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":4,"id":15,"label":{"kind":"normal","label":"\\phi_{XYZ}(f)_2","style":{"alignment":"left","bend":0,"color":"black","dashed":true,"head":"default","kind":"normal","position":0.6,"tail":"none"},"zindex":0},"to":0},{"from":4,"id":16,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":6},{"from":7,"id":17,"label":{"kind":"normal","label":"(\\en_0^{i-1})^{-1}","style":{"alignment":"left","bend":-0.2,"color":"black","dashed":false,"head":"default","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":8},{"from":8,"id":18,"label":{"kind":"normal","label":"(R_0^{i-1}f)_\\El","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":5,"id":19,"label":{"kind":"normal","label":"H_iF_{i-1}(R_{i-1}^i f \\circ \\inj_\\tl^{i-1})","style":{"alignment":"left","bend":0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.6,"tail":"none"},"zindex":6},"to":9},{"from":9,"id":20,"label":{"kind":"normal","label":"H_iF_{i-1}R_{i-1}^if","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":6,"id":21,"label":{"kind":"normal","label":"(\\inj_2)_\\El","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":12,"id":22,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":10}],"nodes":[{"id":0,"label":{"isMath":true,"label":"E(Z)","pos":[440,280],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"(R_0^i Z)_\\El","pos":[600,280],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[600,440],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i Z","pos":[440,440],"zindex":-10000}},{"id":4,"label":{"isMath":true,"label":"Y","pos":[40,120],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"H_iF_{i-1}X","pos":[40,280],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"(K_{H_iF_{i-1}}(X,Y))_\\El","pos":[40,40],"zindex":0}},{"id":7,"label":{"isMath":true,"label":"\\left(R_0^{i-1}X \\oplus K_{H_iF_{i-1}}(X,Y)\\right)_\\El","pos":[360,40],"zindex":0}},{"id":8,"label":{"isMath":true,"label":"R_0^{i-1}(X \\tl^{i-1} K_{H_iF_{i-1}}(X,Y))_\\El","pos":[600,120],"zindex":0}},{"id":9,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i(W(X,Y))","pos":[200,440],"zindex":-10000}}],"sizeGrid":80,"title":"1"}]},"version":12}
|
||||
@ -1 +1 @@
|
||||
{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":6,"label":{"kind":"normal","label":"h","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":7,"label":{"kind":"normal","label":"\\pi_1","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":8,"label":{"kind":"normal","label":"(R_0^i Z)_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":1,"id":9,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":4,"id":10,"label":{"kind":"normal","label":"\\Cstr^Z","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":0,"id":11,"label":{"kind":"normal","label":"h","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":5,"id":12,"label":{"kind":"normal","label":"H_iF_{i-1}g","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":0,"id":13,"label":{"kind":"normal","label":"\\square_\\El","style":{"alignment":"left","bend":-0.2,"color":"blue","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":5,"id":14,"label":{"kind":"normal","label":"\\square_\\UU","style":{"alignment":"right","bend":0.10000000000000003,"color":"blue","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":9,"id":15,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":7}],"nodes":[{"id":0,"label":{"isMath":true,"label":"Y","pos":[130,130],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"E(Z)","pos":[390,130],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i Z)_\\El","pos":[608,130],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[608,234],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i Z","pos":[390,234],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"H_iF_{i-1}X","pos":[130,234],"zindex":-10000}}],"sizeGrid":260,"title":"1"}]},"version":12}
|
||||
{"graph":{"latexPreamble":"\\newcommand{\\coqproof}[1]{\\checkmark}","tabs":[{"active":true,"edges":[{"from":0,"id":6,"label":{"kind":"normal","label":"h","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":7,"label":{"kind":"normal","label":"\\pi_1","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":8,"label":{"kind":"normal","label":"(R_0^i Z)_p","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":1,"id":9,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":4,"id":10,"label":{"kind":"normal","label":"\\Cstr^Z","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":0,"id":11,"label":{"kind":"normal","label":"y","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":5,"id":12,"label":{"kind":"normal","label":"H_iF_{i-1}g","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":0,"id":13,"label":{"kind":"normal","label":"\\square_\\El","style":{"alignment":"left","bend":-0.2,"color":"blue","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":5,"id":14,"label":{"kind":"normal","label":"\\square_\\UU","style":{"alignment":"right","bend":0.10000000000000003,"color":"blue","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":9,"id":15,"label":{"kind":"pullshout","label":"","style":{"alignment":"","bend":0,"color":"black","dashed":false,"head":"","kind":"normal","position":0,"tail":""},"zindex":0},"to":7}],"nodes":[{"id":0,"label":{"isMath":true,"label":"Y","pos":[130,130],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"E(Z)","pos":[390,130],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"(R_0^i Z)_\\El","pos":[608,130],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[608,234],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i Z","pos":[390,234],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"H_iF_{i-1}X","pos":[130,234],"zindex":-10000}}],"sizeGrid":260,"title":"1"}]},"version":12}
|
||||
@ -1 +1 @@
|
||||
{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":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}
|
||||
{"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":"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":"","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":"double","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":0,"id":12,"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":13,"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":14,"label":{"kind":"normal","label":"H_iF_{i-1}g","style":{"alignment":"left","bend":-0.30000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.4,"tail":"none"},"zindex":0},"to":6},{"from":1,"id":15,"label":{"kind":"normal","label":"\\square_\\UU","style":{"alignment":"right","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":"H_iF_{i-1}(X \\tl^{i-1} K_{H_iF_{i-1}}(X,Y))","pos":[210,124],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"H_iF_{i-1}X","pos":[350,70],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"K_{H_iF_{i-1}}(X,Y)_\\UU","pos":[490,70],"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":[630,124],"zindex":0}},{"id":4,"label":{"isMath":true,"label":"R_0^{i-1}\\left(X \\tl^{i-1} K_\\bullet(X,Y)\\right)_\\UU","pos":[630,206],"zindex":0}},{"id":5,"label":{"isMath":true,"label":"(R_0^i Z)_\\UU","pos":[630,284],"zindex":0}},{"id":6,"label":{"isMath":true,"label":"H_iF_{i-1}R_{i-1}^i Z","pos":[210,284],"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\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":3,"label":{"kind":"normal","label":"F","style":{"alignment":"right","bend":0.20000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":4,"label":{"kind":"normal","label":"G","style":{"alignment":"right","bend":0.20000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":2,"id":5,"label":{"kind":"normal","label":"L","style":{"alignment":"right","bend":0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":0,"id":6,"label":{"kind":"normal","label":"R","style":{"alignment":"right","bend":0.2,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":3,"id":7,"label":{"kind":"adjunction","label":"\\vdash","style":{"alignment":"over","bend":0,"color":"black","dashed":false,"head":"none","kind":"none","position":0.5,"tail":"none"},"zindex":0},"to":4},{"from":6,"id":8,"label":{"kind":"adjunction","label":"\\vdash","style":{"alignment":"over","bend":0,"color":"black","dashed":false,"head":"none","kind":"none","position":0.5,"tail":"none"},"zindex":0},"to":5}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\BB","pos":[300,100],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\CC","pos":[486,100],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\BB_0","pos":[300,174],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12}
|
||||
{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":3,"label":{"kind":"normal","label":"F","style":{"alignment":"right","bend":0.20000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":4,"label":{"kind":"normal","label":"G","style":{"alignment":"right","bend":0.20000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":0,"id":5,"label":{"kind":"normal","label":"R","style":{"alignment":"right","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":3,"id":6,"label":{"kind":"adjunction","label":"\\vdash","style":{"alignment":"over","bend":0,"color":"black","dashed":false,"head":"none","kind":"none","position":0.5,"tail":"none"},"zindex":0},"to":4}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\BB","pos":[300,100],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\CC","pos":[486,100],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\BB_0","pos":[300,174],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12}
|
||||
@ -1 +1 @@
|
||||
{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":4,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":5,"label":{"kind":"normal","label":"G_{i-1} \\times \\id","style":{"alignment":"right","bend":0.30000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":6,"label":{"kind":"normal","label":"F_{i-1} \\times \\id","style":{"alignment":"right","bend":0.30000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":2,"id":7,"label":{"kind":"normal","label":"W","style":{"alignment":"right","bend":0.30000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":8,"label":{"kind":"normal","label":"E","style":{"alignment":"right","bend":0.30000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":9,"label":{"kind":"normal","label":"G_i","style":{"alignment":"right","bend":0.6,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":10,"label":{"kind":"normal","label":"F_i","style":{"alignment":"right","bend":-0.4,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":6,"id":11,"label":{"kind":"adjunction","label":"\\vdash","style":{"alignment":"over","bend":0,"color":"black","dashed":false,"head":"none","kind":"none","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":8,"id":12,"label":{"kind":"adjunction","label":"\\vdash","style":{"alignment":"over","bend":0,"color":"black","dashed":false,"head":"none","kind":"none","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":10,"id":13,"label":{"kind":"adjunction","label":"\\vdash","style":{"alignment":"over","bend":0,"color":"black","dashed":false,"head":"none","kind":"none","position":0.5,"tail":"none"},"zindex":0},"to":9}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\CC_i","pos":[176,73.8125],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\left(X : \\CC_{i-1}\\right) \\times \\left.\\Set\\middle/H_iX\\right.","pos":[386,74],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\left(X : \\BB_{i-1}\\right) \\times \\left.\\Set\\middle/H_iF_{i-1}X\\right.","pos":[386,171.8125],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\BB_i","pos":[386,274],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12}
|
||||
{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":0,"id":4,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":1,"id":5,"label":{"kind":"normal","label":"G_{i-1} \\times (H_i\\eta_{i-1}\\circ \\dash)","style":{"alignment":"right","bend":0.30000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":2,"id":6,"label":{"kind":"normal","label":"F_{i-1} \\times \\id","style":{"alignment":"right","bend":0.30000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":2,"id":7,"label":{"kind":"normal","label":"W","style":{"alignment":"right","bend":0.30000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":8,"label":{"kind":"normal","label":"E","style":{"alignment":"right","bend":0.30000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2},{"from":0,"id":9,"label":{"kind":"normal","label":"G_i","style":{"alignment":"right","bend":0.6,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":10,"label":{"kind":"normal","label":"F_i","style":{"alignment":"right","bend":-0.4,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":6,"id":11,"label":{"kind":"adjunction","label":"\\vdash","style":{"alignment":"over","bend":0,"color":"black","dashed":false,"head":"none","kind":"none","position":0.5,"tail":"none"},"zindex":0},"to":5},{"from":8,"id":12,"label":{"kind":"adjunction","label":"\\vdash","style":{"alignment":"over","bend":0,"color":"black","dashed":false,"head":"none","kind":"none","position":0.5,"tail":"none"},"zindex":0},"to":7},{"from":10,"id":13,"label":{"kind":"adjunction","label":"\\vdash","style":{"alignment":"over","bend":0,"color":"black","dashed":false,"head":"none","kind":"none","position":0.5,"tail":"none"},"zindex":0},"to":9}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\CC_i","pos":[176,73.8125],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\left(X : \\CC_{i-1}\\right) \\times \\left.\\Set\\middle/H_iX\\right.","pos":[386,74],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\left(X : \\BB_{i-1}\\right) \\times \\left.\\Set\\middle/H_iF_{i-1}X\\right.","pos":[386,171.8125],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\BB_i","pos":[386,274],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12}
|
||||
1
Report/graphs/PhiXYZFirstComponent.json
Normal file
1
Report/graphs/PhiXYZFirstComponent.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":"\\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":5,"label":{"kind":"normal","label":"","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"none","kind":"double","position":0.5,"tail":"none"},"zindex":0},"to":3},{"from":3,"id":6,"label":{"kind":"normal","label":"R_{i-1}^i f","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":2}],"nodes":[{"id":0,"label":{"isMath":true,"label":"X","pos":[100,100],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"X \\tl^{i-1}K_{H_iF_{i-1}}(X,Y)","pos":[300,100],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"R_{i-1}^iZ","pos":[700,100],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"R_{i-1}^i(W(X,Y))","pos":[500,100],"zindex":-10000}}],"sizeGrid":200,"title":"1"}]},"version":12}
|
||||
Loading…
x
Reference in New Issue
Block a user