From f6bc7f8db993f95953ff4ad753b499d291b24ce8 Mon Sep 17 00:00:00 2001 From: Samy Avrillon Date: Sat, 17 Aug 2024 01:43:49 +0200 Subject: [PATCH] =?UTF-8?q?Prise=20en=20compte=20des=20commentaires,=20d?= =?UTF-8?q?=C3=A9placement=20de=20la=20preuve=20de=20l'adjonction=20en=20a?= =?UTF-8?q?nnexe?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Report/M2Report.tex | 175 ++++++++++++++++++++++---------------------- 1 file changed, 87 insertions(+), 88 deletions(-) diff --git a/Report/M2Report.tex b/Report/M2Report.tex index fb89c5b..8776d78 100644 --- a/Report/M2Report.tex +++ b/Report/M2Report.tex @@ -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}$}