From 86dd4ec9002443946d75bc25dbd2197f8a34d3b8 Mon Sep 17 00:00:00 2001 From: Samy Avrillon Date: Fri, 16 Aug 2024 00:59:15 +0200 Subject: [PATCH] Renamed Graphs --- Report/M2Report.tex | 116 +++++++++++------- Report/graphs/B1.json | 1 - .../{D1.json => BiMorphismDiagram.json} | 0 ...9.json => CompositionSecondComponent.json} | 0 ...son => CompositionSquareConstruction.json} | 0 .../{D3b.json => EDefinitionMorphism.json} | 0 .../{D3a.json => EDefinitionPullback.json} | 0 ...1-0.json => GlobalConstructionSimple.json} | 0 ....json => GlobalRecursiveConstruction.json} | 0 .../{G2.json => InductionStepDiagram.json} | 0 .../{D10.0.json => NaturalityDiagram.json} | 0 ...> NaturalityDoublePullbackDefinition.json} | 0 .../{D8.json => PhiXYZ-1MorphismOfBi.json} | 0 .../graphs/{D7.json => PhiXYZ-1Square.json} | 0 ...6.json => PhiXYZSndComponentPullback.json} | 0 ...json => ReflectionFGExtendedPullback.json} | 0 ...json => ReflectionFGIsomorphismFirst.json} | 0 ...son => ReflectionFGIsomorphismSecond.json} | 0 .../{E1.json => ReflectionFGPullback.json} | 0 .../{D4.json => TlInj1MorphismOfBi.json} | 0 ...D5.json => TlUniversalMorphismIsOfBi.json} | 0 .../graphs/{D2.json => WghMorphismOfBi.json} | 0 22 files changed, 70 insertions(+), 47 deletions(-) delete mode 100644 Report/graphs/B1.json rename Report/graphs/{D1.json => BiMorphismDiagram.json} (100%) rename Report/graphs/{D9.json => CompositionSecondComponent.json} (100%) rename Report/graphs/{D10.json => CompositionSquareConstruction.json} (100%) rename Report/graphs/{D3b.json => EDefinitionMorphism.json} (100%) rename Report/graphs/{D3a.json => EDefinitionPullback.json} (100%) rename Report/graphs/{G1-0.json => GlobalConstructionSimple.json} (100%) rename Report/graphs/{G1.json => GlobalRecursiveConstruction.json} (100%) rename Report/graphs/{G2.json => InductionStepDiagram.json} (100%) rename Report/graphs/{D10.0.json => NaturalityDiagram.json} (100%) rename Report/graphs/{D11.json => NaturalityDoublePullbackDefinition.json} (100%) rename Report/graphs/{D8.json => PhiXYZ-1MorphismOfBi.json} (100%) rename Report/graphs/{D7.json => PhiXYZ-1Square.json} (100%) rename Report/graphs/{D6.json => PhiXYZSndComponentPullback.json} (100%) rename Report/graphs/{E2.json => ReflectionFGExtendedPullback.json} (100%) rename Report/graphs/{E3.json => ReflectionFGIsomorphismFirst.json} (100%) rename Report/graphs/{E4.json => ReflectionFGIsomorphismSecond.json} (100%) rename Report/graphs/{E1.json => ReflectionFGPullback.json} (100%) rename Report/graphs/{D4.json => TlInj1MorphismOfBi.json} (100%) rename Report/graphs/{D5.json => TlUniversalMorphismIsOfBi.json} (100%) rename Report/graphs/{D2.json => WghMorphismOfBi.json} (100%) diff --git a/Report/M2Report.tex b/Report/M2Report.tex index c61bc41..66581ce 100644 --- a/Report/M2Report.tex +++ b/Report/M2Report.tex @@ -104,9 +104,9 @@ 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)$. \begin{center} - % YADE DIAGRAM G1-0.json + % YADE DIAGRAM GlobalConstructionSimple.json % GENERATED LATEX - \input{graphs/G1-0.tex} + \input{graphs/GlobalConstructionSimple.tex} % END OF GENERATED LATEX \end{center} @@ -156,9 +156,9 @@ Here is a figure that describes the recursive construction of some of the above objects \begin{center} - % YADE DIAGRAM G1.json + % YADE DIAGRAM GlobalRecursiveConstruction.json % GENERATED LATEX - \input{graphs/G1.tex} + \input{graphs/GlobalRecursiveConstruction.tex} % END OF GENERATED LATEX \end{center} @@ -334,9 +334,9 @@ A morphism $X \to X'$ of $\BB_i$ is a morphism $f : R_{i-1}^iX \to R_{i-1}^iX'$ in $\BB_{i-1}$ such that the following diagram commutes. \begin{center} - % YADE DIAGRAM D1.json + % YADE DIAGRAM BiMorphismDiagram.json % GENERATED LATEX - \input{graphs/D1.tex} + \input{graphs/BiMorphismDiagram.tex} % END OF GENERATED LATEX \end{center} @@ -351,9 +351,9 @@ 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 + % YADE DIAGRAM InductionStepDiagram.json % GENERATED LATEX - \input{graphs/G2.tex} + \input{graphs/InductionStepDiagram.tex} % END OF GENERATED LATEX \end{center} @@ -403,9 +403,9 @@ It is indeed a morphism of $\BB_{i}$ as it makes the following diagram commute. \begin{center} - % YADE DIAGRAM D2.json + % YADE DIAGRAM WghMorphismOfBi.json % GENERATED LATEX - \input{graphs/D2.tex} + \input{graphs/WghMorphismOfBi.tex} % END OF GENERATED LATEX \end{center} @@ -420,18 +420,18 @@ Where $(A,h)$ is defined as the following pullback: \begin{center} - % YADE DIAGRAM D3a.json + % YADE DIAGRAM EDefinitionPullback.json % GENERATED LATEX - \input{graphs/D3a.tex} + \input{graphs/EDefinitionPullback.tex} % END OF GENERATED LATEX \end{center} 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} - % YADE DIAGRAM D3b.json + % YADE DIAGRAM EDefinitionMorphism.json % GENERATED LATEX - \input{graphs/D3b.tex} + \input{graphs/EDefinitionMorphism.tex} % END OF GENERATED LATEX \end{center} @@ -464,11 +464,12 @@ 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 D6.json + % YADE DIAGRAM PhiXYZSndComponentPullback.json % GENERATED LATEX - \input{graphs/D6.tex} + \input{graphs/PhiXYZSndComponentPullback.tex} % END OF GENERATED LATEX - \end{center} + +\end{center} \subsubsection{Constructing $\phi^{-1}_{XYZ}$} @@ -485,20 +486,22 @@ 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 + % YADE DIAGRAM PhiXYZ-1Square.json % GENERATED LATEX - \input{graphs/D7.tex} + \input{graphs/PhiXYZ-1Square.tex} % END OF GENERATED LATEX - \end{center} + +\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 D8.json + % YADE DIAGRAM PhiXYZ-1MorphismOfBi.json % GENERATED LATEX - \input{graphs/D8.tex} + \input{graphs/PhiXYZ-1MorphismOfBi.tex} % END OF GENERATED LATEX - \end{center} + +\end{center} In order to complete this proof, we need to show that \begin{itemize} @@ -544,9 +547,9 @@ It is a morphism of $\BB_i$ as it makes the following diagram commute: \begin{center} - % YADE DIAGRAM D4.json + % YADE DIAGRAM TlInj1MorphismOfBi.json % GENERATED LATEX - \input{graphs/D4.tex} + \input{graphs/TlInj1MorphismOfBi.tex} % END OF GENERATED LATEX \end{center} @@ -564,9 +567,9 @@ 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 + % YADE DIAGRAM TlUniversalMorphismIsOfBi.json % GENERATED LATEX - \input{graphs/D5.tex} + \input{graphs/TlUniversalMorphismIsOfBi.tex} % END OF GENERATED LATEX \end{center} @@ -774,9 +777,9 @@ A morphism from $(X,\Cstr)$ to $(X', \Cstr')$ is a morphism from $X$ to $X'$ in $\TSet$ (i.e. a natural transformation $X \implies X'$) which makes the following diagram commute, for all $a$ in $S_{i-1}$. \begin{center} - % YADE DIAGRAM D1.json + % YADE DIAGRAM BiMorphismDiagram.json % GENERATED LATEX - \input{graphs/D1.tex} + \input{graphs/BiMorphismDiagram.tex} % END OF GENERATED LATEX \end{center} @@ -840,11 +843,12 @@ The second component of $\phi_{XYZ} (\phi_{XYZ}^{-1}(g,h))$ follows the following diagram \begin{center} - % YADE DIAGRAM D9.json + % YADE DIAGRAM CompositionSecondComponent.json % GENERATED LATEX - \input{graphs/D9.tex} + \input{graphs/CompositionSecondComponent.tex} % END OF GENERATED LATEX - \end{center} + +\end{center} \todo{Justifier que la partie du haut commute, i.e. que \[ @@ -863,9 +867,9 @@ where $\square$ follows the following diagram \begin{center} - % YADE DIAGRAM D10.json + % YADE DIAGRAM CompositionSquareConstruction.json % GENERATED LATEX - \input{graphs/D10.tex} + \input{graphs/CompositionSquareConstruction.tex} % END OF GENERATED LATEX \end{center} @@ -883,9 +887,9 @@ We want to show that the following diagram commutes, for any objects $X$,$Y$,$Z$,$X'$,$Y'$,$Z'$ and morphisms $f$,$g$,$h$. \begin{center} - % YADE DIAGRAM D10.0.json + % YADE DIAGRAM NaturalityDiagram.json % GENERATED LATEX - \input{graphs/D10.0.tex} + \input{graphs/NaturalityDiagram.tex} % END OF GENERATED LATEX \end{center} @@ -904,9 +908,9 @@ The second components are defined as described by the following diagram \begin{center} - % YADE DIAGRAM D11.json + % YADE DIAGRAM NaturalityDoublePullbackDefinition.json % GENERATED LATEX - \input{graphs/D11.tex} + \input{graphs/NaturalityDoublePullbackDefinition.tex} % END OF GENERATED LATEX \end{center} @@ -934,35 +938,35 @@ Where $(A,h)$ is the pullback defined as \begin{center} - % YADE DIAGRAM E1.json + % YADE DIAGRAM ReflectionFGPullback.json % GENERATED LATEX - \input{graphs/E1.tex} + \input{graphs/ReflectionFGPullback.tex} % END OF GENERATED LATEX \end{center} We can extend this pullback with the two isomorphisms $\en_0^i$ and $H_iF_{i-1}(\inj_\tl^{i-1})$ in another pullback. This new pullback is over the injection morphism $\inj_2$ of the coproduct of $\TSet$, so the new pullback object is the second component of the $\bullet \oplus B$ i.e. $B$. \begin{center} - % YADE DIAGRAM E2.json + % YADE DIAGRAM ReflectionFGExtendedPullback.json % GENERATED LATEX - \input{graphs/E2.tex} + \input{graphs/ReflectionFGExtendedPullback.tex} % END OF GENERATED LATEX \end{center} The first component of the isomorphism is the following isomorphism, where $\eta_{i-1}^{FG}$ if the counit of the adjunction $F_{i-1} \vdash G_{i-1}$, that we know to be an isomorphism from the induction hypothesis. \begin{center} - % YADE DIAGRAM E3.json + % YADE DIAGRAM ReflectionFGIsomorphismFirst.json % GENERATED LATEX - \input{graphs/E3.tex} + \input{graphs/ReflectionFGIsomorphismFirst.tex} % END OF GENERATED LATEX \end{center} And the second component is made using the isomorphism constructed by the pullback, that makes the diagram commute. \begin{center} - % YADE DIAGRAM E4.json + % YADE DIAGRAM ReflectionFGIsomorphismSecond.json % GENERATED LATEX - \input{graphs/E4.tex} + \input{graphs/ReflectionFGIsomorphismSecond.tex} % END OF GENERATED LATEX \end{center} @@ -1073,6 +1077,26 @@ + + + + + + + + + + + + + + + + + + + + diff --git a/Report/graphs/B1.json b/Report/graphs/B1.json deleted file mode 100644 index c9f21d6..0000000 --- a/Report/graphs/B1.json +++ /dev/null @@ -1 +0,0 @@ -{"graph":{"latexPreamble":"\\newcommand\\ensuremath[1]{#1}\n\\newcommand\\BB{{\\ensuremath{\\mathcal{B}}}}\n\\newcommand\\TT{{\\ensuremath{\\mathcal{T}}}}\n\\newcommand\\UU{{\\ensuremath{\\mathcal{U}}}}\n\\newcommand\\El{{\\ensuremath{\\operatorname{\\mathcal{E}l}}}}\n\\newcommand\\ii{{\\ensuremath{\\mathbf{i}}}}\n\\newcommand\\Cstr{{\\ensuremath{\\operatorname{\\mathcal{C}str}}}}\n\\newcommand\\Set{{\\ensuremath{\\operatorname{\\mathcal{S}et}}}}\n\\newcommand\\Hom{{\\ensuremath{\\operatorname{\\mathcal{H}om}}}}\n\\newcommand\\this{{\\ensuremath{\\operatorname{\\texttt{this}}}}}\n\\newcommand\\Hbar{{\\ensuremath{\\overline{H}}}}\n\\newcommand\\dash{{\\;\\textrm{---}\\;}}\n\n\\newcommand\\inj{\\operatorname{inj}}\n\\newcommand\\id{\\operatorname{id}}","tabs":[{"active":true,"edges":[{"from":1,"id":4,"label":{"kind":"normal","label":"\\Gamma","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":0},{"from":2,"id":5,"label":{"kind":"normal","label":"A","style":{"alignment":"left","bend":0,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":1},{"from":2,"id":6,"label":{"kind":"normal","label":"\\Delta","style":{"alignment":"right","bend":0.20000000000000004,"color":"black","dashed":false,"head":"default","kind":"normal","position":0.5,"tail":"none"},"zindex":0},"to":0}],"nodes":[{"id":0,"label":{"isMath":true,"label":"\\Con","pos":[100,100],"zindex":0}},{"id":1,"label":{"isMath":true,"label":"\\Ty","pos":[300,100],"zindex":0}},{"id":2,"label":{"isMath":true,"label":"\\Tm","pos":[500,100],"zindex":0}},{"id":3,"label":{"isMath":true,"label":"\\circlearrowleft","pos":[302,76.8125],"zindex":0}}],"sizeGrid":200,"title":"1"}]},"version":12} \ No newline at end of file diff --git a/Report/graphs/D1.json b/Report/graphs/BiMorphismDiagram.json similarity index 100% rename from Report/graphs/D1.json rename to Report/graphs/BiMorphismDiagram.json diff --git a/Report/graphs/D9.json b/Report/graphs/CompositionSecondComponent.json similarity index 100% rename from Report/graphs/D9.json rename to Report/graphs/CompositionSecondComponent.json diff --git a/Report/graphs/D10.json b/Report/graphs/CompositionSquareConstruction.json similarity index 100% rename from Report/graphs/D10.json rename to Report/graphs/CompositionSquareConstruction.json diff --git a/Report/graphs/D3b.json b/Report/graphs/EDefinitionMorphism.json similarity index 100% rename from Report/graphs/D3b.json rename to Report/graphs/EDefinitionMorphism.json diff --git a/Report/graphs/D3a.json b/Report/graphs/EDefinitionPullback.json similarity index 100% rename from Report/graphs/D3a.json rename to Report/graphs/EDefinitionPullback.json diff --git a/Report/graphs/G1-0.json b/Report/graphs/GlobalConstructionSimple.json similarity index 100% rename from Report/graphs/G1-0.json rename to Report/graphs/GlobalConstructionSimple.json diff --git a/Report/graphs/G1.json b/Report/graphs/GlobalRecursiveConstruction.json similarity index 100% rename from Report/graphs/G1.json rename to Report/graphs/GlobalRecursiveConstruction.json diff --git a/Report/graphs/G2.json b/Report/graphs/InductionStepDiagram.json similarity index 100% rename from Report/graphs/G2.json rename to Report/graphs/InductionStepDiagram.json diff --git a/Report/graphs/D10.0.json b/Report/graphs/NaturalityDiagram.json similarity index 100% rename from Report/graphs/D10.0.json rename to Report/graphs/NaturalityDiagram.json diff --git a/Report/graphs/D11.json b/Report/graphs/NaturalityDoublePullbackDefinition.json similarity index 100% rename from Report/graphs/D11.json rename to Report/graphs/NaturalityDoublePullbackDefinition.json diff --git a/Report/graphs/D8.json b/Report/graphs/PhiXYZ-1MorphismOfBi.json similarity index 100% rename from Report/graphs/D8.json rename to Report/graphs/PhiXYZ-1MorphismOfBi.json diff --git a/Report/graphs/D7.json b/Report/graphs/PhiXYZ-1Square.json similarity index 100% rename from Report/graphs/D7.json rename to Report/graphs/PhiXYZ-1Square.json diff --git a/Report/graphs/D6.json b/Report/graphs/PhiXYZSndComponentPullback.json similarity index 100% rename from Report/graphs/D6.json rename to Report/graphs/PhiXYZSndComponentPullback.json diff --git a/Report/graphs/E2.json b/Report/graphs/ReflectionFGExtendedPullback.json similarity index 100% rename from Report/graphs/E2.json rename to Report/graphs/ReflectionFGExtendedPullback.json diff --git a/Report/graphs/E3.json b/Report/graphs/ReflectionFGIsomorphismFirst.json similarity index 100% rename from Report/graphs/E3.json rename to Report/graphs/ReflectionFGIsomorphismFirst.json diff --git a/Report/graphs/E4.json b/Report/graphs/ReflectionFGIsomorphismSecond.json similarity index 100% rename from Report/graphs/E4.json rename to Report/graphs/ReflectionFGIsomorphismSecond.json diff --git a/Report/graphs/E1.json b/Report/graphs/ReflectionFGPullback.json similarity index 100% rename from Report/graphs/E1.json rename to Report/graphs/ReflectionFGPullback.json diff --git a/Report/graphs/D4.json b/Report/graphs/TlInj1MorphismOfBi.json similarity index 100% rename from Report/graphs/D4.json rename to Report/graphs/TlInj1MorphismOfBi.json diff --git a/Report/graphs/D5.json b/Report/graphs/TlUniversalMorphismIsOfBi.json similarity index 100% rename from Report/graphs/D5.json rename to Report/graphs/TlUniversalMorphismIsOfBi.json diff --git a/Report/graphs/D2.json b/Report/graphs/WghMorphismOfBi.json similarity index 100% rename from Report/graphs/D2.json rename to Report/graphs/WghMorphismOfBi.json