Prise en compte des commentaires, déplacement de la preuve de l'adjonction en annexe
This commit is contained in:
parent
4effe18e0f
commit
f6bc7f8db9
GPG Key ID:
0220AC4A3D6A328B
@ -26,7 +26,7 @@
|
||||
\section{Introduction}
|
||||
|
||||
A Generalized Algebraic Theory (or GAT), first introduced by Cartmell \cite{CartmellGATs}, is a syntactic specification of an algebraic structure. From a GAT, one can define a category of models describing the models of the algebraic structure.
|
||||
A GAT typically starts with a sort specification i.e. a list of sort declarations, eventually followed by a list of constructors.
|
||||
A GAT typically starts with a sort specification i.e. a list of sort declarations, which may be 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 to understand the rest of the document.
|
||||
|
||||
\paragraph{Sort specification}
|
||||
@ -46,9 +46,9 @@
|
||||
|
||||
A sort specification therefore specifies the differents families of sets contained in a model, and how they relate to each other in terms of indexing.
|
||||
|
||||
\paragraph{Constructor specification}
|
||||
We can also add constructors to a sort specification. They are composed of parameters (the same kind as sort declarations) and of a codomain which is a sort defined in a previous sort declaration. Those constructors specify elements of the sets contained in the model.
|
||||
For example, for the previous sort specification, one can add the following constructors:
|
||||
\paragraph{Term specification}
|
||||
Once we have a sort specification, we can add constructors to it in order to make a complete GAT. Constructors are composed of parameters (the same kind as for sort declarations) and of a codomain which is a sort defined by a previous sort declaration. Those constructors specify elements of the sets contained in the model.
|
||||
For example, to the previous sort specification, one can add the following constructors:
|
||||
|
||||
\vspace{1em}
|
||||
\renewcommand\arraystretch{1.5}
|
||||
@ -61,7 +61,7 @@
|
||||
|
||||
\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. Let us present this transformation.
|
||||
|
||||
The sort specification of the transformed GAT is always the same, and contains these two sort declarations:
|
||||
|
||||
@ -74,7 +74,7 @@
|
||||
|
||||
|
||||
|
||||
Then, we replace all occurrences of $\Set$ to $\mathcal{O}$, and we apply $\El$ to every parameter. We write $\underline{o}$ rather than $\El(o)$ in order to ease reading. For example, the Type Theory GAT presented above becomes that which follows:
|
||||
Then, we replace all occurrences of $\Set$ to $\mathcal{O}$, and we apply $\El$ to every parameter. We write $\underline{o}$ rather than $\El(o)$ in order to ease reading. For example, the GAT of Type Theory presented above becomes that which follows:
|
||||
|
||||
\begin{tabular}{p{0.4\textwidth}|p{0.5\textwidth}}
|
||||
$\Con : \mathcal{O}$ & One sort object is called \enquote{$\Con$} \\
|
||||
@ -99,7 +99,8 @@
|
||||
|
||||
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. In this document, we will only study sort specifications (i.e. lists of sort declaration, with no constructors).
|
||||
|
||||
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.
|
||||
We constructed a coreflection between those two categories, whose formal definition is given in \autoref{sec:proofSection}. 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.
|
||||
This coreflection justifies the transformation as the initial object of $\CC$ can be computed as the image by $F$ of the initial object of $\BB$.
|
||||
|
||||
The category $\BB$ is equipped with a forgetful functor $R$ to $\BB_0$, the category of models of the two-sort sort specification $(\mathcal{O},\El)$.
|
||||
|
||||
@ -113,7 +114,7 @@
|
||||
\section{Examples}
|
||||
\label{sec:Examples}
|
||||
|
||||
Before making the formal proof, we will study our construction on three examples.
|
||||
Before making the formal proof, we will study our construction on three examples, in order to ease understanding of the formal proof.
|
||||
|
||||
\paragraph{Structure of the proof}
|
||||
The formal proof will be an 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}).
|
||||
@ -156,7 +157,7 @@
|
||||
\end{center}
|
||||
\vspace{.5ex}
|
||||
|
||||
The usual way of defining the category of models of this sort specification is by taking the category of families of sets $\FamSet$, whose objects are pairs of a set $X$ and a family of sets indexed by $X$ : $(Y_x)_{x\in X}$. However, we will rather use another category : $\TSet$, the category of presheaves over the category $\TT$, the category with two object and one non-trivial arrow between them. The objects and morphism of $\TT$ are described below:
|
||||
The usual way of defining the category of models of this sort specification is by taking the category of families of sets $\FamSet$, whose objects are pairs of a set $X$ and a family of sets indexed by $X$ : $(Y_x)_{x\in X}$. However, we will rather use another category : $\TSet$, the category of presheaves over the category $\TT$, the category with two objects and one non-trivial arrow between them. The objects and morphism of $\TT$ are described below:
|
||||
|
||||
\begin{center}
|
||||
% YADE DIAGRAM CategoryTT.json
|
||||
@ -495,7 +496,7 @@
|
||||
\todo{L'exemple, ou sinon remplacer toutes les occurences de «trois» par «deux»}
|
||||
|
||||
\section{Constructing the coreflection}
|
||||
|
||||
\label{sec:proofSection}
|
||||
The proof will take form of an induction on the number of sorts taken into account. At each induction step, we will build the following objects:
|
||||
|
||||
\begin{itemize}
|
||||
@ -543,14 +544,14 @@
|
||||
|
||||
\subsection{Preliminaries}
|
||||
|
||||
\paragraph{Grothendieck Construction}
|
||||
\paragraph{Grothendieck construction}
|
||||
For a category $\mathcal{C}$ and a functor $F : \mathcal{C} \to \Cat$, the Grothendieck construction of $F$ is a category whose objects are pairs of
|
||||
\begin{itemize}
|
||||
\item $X$ an object of $\mathcal{C}$
|
||||
\item an object of $F(X)$
|
||||
\end{itemize}
|
||||
|
||||
The morphism $(X,Y) \to (X',Y')$ is therefore a pair of a morphism $f : X \to X'$ in $\mathcal{C}$ and a morphism $g : F(f)(Y) \to Y'$ in $H(X')$.
|
||||
A morphism $(X,Y) \to (X',Y')$ is a pair of a morphism $f : X \to X'$ in $\mathcal{C}$ and a morphism $g : F(f)(Y) \to Y'$ in $H(X')$.
|
||||
|
||||
We will denote this category $(X : \mathcal{C}) \times F(X)$ as its objects are pairs.
|
||||
|
||||
@ -576,7 +577,7 @@
|
||||
This equivalence is described by the following correspondence of objects.
|
||||
An object $(Y,f)$ of $\Set/X$ is transformed into the family of sets $A : X \to \Set$ defined by
|
||||
\[
|
||||
A(x) := f^{-1}(\{x\}) = \text{the coimage by f of the singleton $\{x\}$}
|
||||
A(x) := f^{-1}(\{x\}) = \text{the preimage by f of the singleton $\{x\}$}
|
||||
\]
|
||||
|
||||
Conversly, a familiy of sets $A : X \to \Set$ is transformed into the following object of $\Set/X$
|
||||
@ -601,7 +602,7 @@
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
|
||||
This category is equivalent to the catgegory $\FamSet$, as $(X : \Set) \times \Set^X$ is equivalent to $(X : \Set) \times (\Set/X)$ (as seen above), which is isomorphic to $\TSet$ (both categories consists of two sets and one arrow between them).
|
||||
This category is equivalent to the category $\FamSet$, as $(X : \Set) \times \Set^X$ is equivalent to $(X : \Set) \times (\Set/X)$ (as seen above), which is isomorphic to $\TSet$ (both categories consists of two sets and one arrow between them).
|
||||
|
||||
The categories of models of the transformed GATs will be built atop of this category $\BB_0 = \TSet$.
|
||||
|
||||
@ -772,9 +773,11 @@
|
||||
% END OF GENERATED LATEX
|
||||
\end{center}
|
||||
|
||||
\subsection{Inductive Step: Proof of the adjunction}
|
||||
\subsection{Inductive Step: Proof of the coreflection}
|
||||
|
||||
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.
|
||||
In this subsection, we prove that $(W,E)$ make up a coreflection i.e. an adjunction where the left adjoint is full and faithful.
|
||||
|
||||
\paragraph{Adjunction} We will prove the 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$, a natural isomorphism $\phi_{XYZ}$.
|
||||
|
||||
@ -782,80 +785,21 @@
|
||||
\phi_{XYZ} : \Hom(W(X,Y),Z) \to \Hom((X,Y),E(Z))
|
||||
\]
|
||||
|
||||
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}.
|
||||
You can find the proof of the adjunction in \autoref{apx:adjunction}, made of the following parts:
|
||||
\begin{itemize}
|
||||
\item The construction of $\phi_{XYZ}$
|
||||
\item The construction of $\phi_{XYZ}^{-1}$
|
||||
\item A proof that $\phi_{XYZ}^{-1} \circ \phi_{XYZ} (f) = f$
|
||||
\item A proof that $\phi_{XYZ} \circ \phi_{XYZ}^{-1} (g,h) = (g,h)$
|
||||
\item A proof that $\phi_{XYZ}$ is natural.
|
||||
\end{itemize}
|
||||
|
||||
\subsubsection{Constructing $\phi_{XYZ}$}
|
||||
All these steps give us that $F_i$ and $G_i$ are in an adjunction $F_i \vdash G_i$.
|
||||
|
||||
Let $f$ be in $\Hom(W(X,Y),Z)$.
|
||||
We want to construct $\phi_{XYZ}(f) : (X,Y) \to E(Z)$.
|
||||
\paragraph{Coreflection}
|
||||
Next, 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 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:
|
||||
|
||||
\begin{center}
|
||||
% YADE DIAGRAM PhiXYZSndComponentPullback.json
|
||||
% GENERATED LATEX
|
||||
\input{graphs/PhiXYZSndComponentPullback.tex}
|
||||
% END OF GENERATED LATEX
|
||||
|
||||
\end{center}
|
||||
|
||||
\subsubsection{Constructing $\phi^{-1}_{XYZ}$}
|
||||
|
||||
Now, we take $(g,h)$ a morphism from $(X,Y)$ to $E(Z)$.
|
||||
|
||||
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 the introduction of this section.
|
||||
|
||||
\[
|
||||
\phi^{-1}_{XYZ}(g,h) := \left\{g ; \square \right\}
|
||||
\]
|
||||
|
||||
\todo{Est-ce qu'il faut que j'écrive $R_{i-1}^i\phi^{-1}_{XYZ}(g,h) := ...$ pour être plus «homogène» ?}
|
||||
|
||||
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 PhiXYZ-1Square.json
|
||||
% GENERATED LATEX
|
||||
\input{graphs/PhiXYZ-1Square.tex}
|
||||
% END OF GENERATED LATEX
|
||||
|
||||
\end{center}
|
||||
|
||||
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 PhiXYZ-1MorphismOfBi.json
|
||||
% GENERATED LATEX
|
||||
\input{graphs/PhiXYZ-1MorphismOfBi.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}
|
||||
|
||||
The proofs of these statements are given in \autoref{apx:phi-WE-isnat}.
|
||||
|
||||
|
||||
|
||||
\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 that statement is given in \autoref{apx:FG-refl}.
|
||||
The proof of that second statement is given in \autoref{apx:FG-refl}.
|
||||
|
||||
\subsection{Inductive step: Constructing $\tl^i$}
|
||||
|
||||
@ -1166,8 +1110,63 @@
|
||||
\appendixpage
|
||||
|
||||
\section{$W \dashv E$ adjunction}
|
||||
\label{apx:phi-WE-isnat}
|
||||
\label{apx:adjunction}
|
||||
|
||||
\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 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:
|
||||
|
||||
\begin{center}
|
||||
% YADE DIAGRAM PhiXYZSndComponentPullback.json
|
||||
% GENERATED LATEX
|
||||
\input{graphs/PhiXYZSndComponentPullback.tex}
|
||||
% END OF GENERATED LATEX
|
||||
|
||||
\end{center}
|
||||
|
||||
\subsubsection{Constructing $\phi^{-1}_{XYZ}$}
|
||||
|
||||
Now, we take $(g,h)$ a morphism from $(X,Y)$ to $E(Z)$.
|
||||
|
||||
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 the introduction of this section.
|
||||
|
||||
\[
|
||||
\phi^{-1}_{XYZ}(g,h) := \left\{g ; \square \right\}
|
||||
\]
|
||||
|
||||
\todo{Est-ce qu'il faut que j'écrive $R_{i-1}^i\phi^{-1}_{XYZ}(g,h) := ...$ pour être plus «homogène» ?}
|
||||
|
||||
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 PhiXYZ-1Square.json
|
||||
% GENERATED LATEX
|
||||
\input{graphs/PhiXYZ-1Square.tex}
|
||||
% END OF GENERATED LATEX
|
||||
|
||||
\end{center}
|
||||
|
||||
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 PhiXYZ-1MorphismOfBi.json
|
||||
% GENERATED LATEX
|
||||
\input{graphs/PhiXYZ-1MorphismOfBi.tex}
|
||||
% END OF GENERATED LATEX
|
||||
|
||||
\end{center}
|
||||
|
||||
\subsection{Composition $\phi_{XYZ} \circ \phi_{XYZ}^{-1}$}
|
||||
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user