From 1757fd1823f4d88a1690eda75ae6e582b7c8a279 Mon Sep 17 00:00:00 2001 From: mkaratarakis Date: Wed, 19 Mar 2025 21:59:33 +0100 Subject: [PATCH 01/13] fix build --- .../Distributivity.lean | 21 ++++++++++--------- 1 file changed, 11 insertions(+), 10 deletions(-) diff --git a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean index d2b7952..018c62f 100644 --- a/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean +++ b/Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean @@ -97,10 +97,11 @@ lemma cellLeftCartesian : cartesian (cellLeft f u) := by simp only [id_obj, mk_left, comp_obj, pullback_obj_left, Functor.comp_map] unfold cellLeft intros i j f' - have α := pullbackMapTriangle (w f u) (e f u) + have α := pullbackMapTriangle (w f u) (e f u) u (cellLeftTriangle f u) simp only [id_obj, mk_left] at α u sorry + def cellRightCommSq : CommSq (g f u) (w f u) (v f u) f := IsPullback.toCommSq (IsPullback.of_hasPullback _ _) @@ -110,24 +111,20 @@ def cellRight' : pushforward (g f u) ⋙ map (v f u) lemma cellRightCartesian : cartesian (cellRight' f u).hom := cartesian_of_isIso ((cellRight' f u).hom) -def pasteCell1 : pullback (e f u) ⋙ pushforward (g f u) ⋙ map (v f u) ⟶ +abbrev pasteCell1 : pullback (e f u) ⋙ pushforward (g f u) ⋙ map (v f u) ⟶ pullback (e f u) ⋙ map (w f u) ⋙ pushforward f := by apply whiskerLeft exact (cellRight' f u).hom -def pasteCell2 : (pullback (e f u) ⋙ map (w f u)) ⋙ pushforward f - ⟶ (map u) ⋙ pushforward f := by - apply whiskerRight - exact cellLeft f u +abbrev pasteCell2 : (pullback (e f u) ⋙ map (w f u)) ⋙ pushforward f + ⟶ (map u) ⋙ pushforward f := whiskerRight (cellLeft f u) _ def pasteCell := pasteCell1 f u ≫ pasteCell2 f u def paste : cartesian (pasteCell f u) := by apply cartesian.comp - · unfold pasteCell1 - apply cartesian.whiskerLeft (cellRightCartesian f u) - · unfold pasteCell2 - apply cartesian.whiskerRight (cellLeftCartesian f u) + · exact cartesian.whiskerLeft (cellRightCartesian f u) _ + · exact cartesian.whiskerRight (cellLeftCartesian f u) _ #check pushforwardPullbackTwoSquare @@ -136,6 +133,10 @@ def pentagonIso : map u ⋙ pushforward f ≅ pullback (e f u) ⋙ pushforward (g f u) ⋙ map (v f u) := by have := cartesian_of_isPullback_to_terminal (pasteCell f u) letI : IsIso ((pasteCell f u).app (⊤_ Over ((𝟭 (Over B)).obj (Over.mk u)).left)) := sorry + -- by { + -- have : TwoSquare (pushforward (g f u)) (Over.pullback _) (Over.pullback _) (pushforward f) := by + -- apply pushforwardPullbackTwoSquare _ _ _ f u + -- } have := isIso_of_cartesian (pasteCell f u) (paste f u) exact (asIso (pasteCell f u)).symm From 18d81a0052634eb59121dff584542e90f6c764b8 Mon Sep 17 00:00:00 2001 From: mkaratarakis Date: Sat, 5 Apr 2025 01:12:14 +0200 Subject: [PATCH 02/13] test blueprint --- Poly/MvPoly.lean | 53 +++++++++++++++++++++++++++++------ blueprint/src/chapter/all.tex | 2 ++ 2 files changed, 46 insertions(+), 9 deletions(-) diff --git a/Poly/MvPoly.lean b/Poly/MvPoly.lean index d438e89..b994196 100644 --- a/Poly/MvPoly.lean +++ b/Poly/MvPoly.lean @@ -79,28 +79,63 @@ def sum {I O : C} [HasBinaryCoproducts C] (P Q : MvPoly I O) : MvPoly I O where B := P.B ⨿ Q.B i := coprod.desc P.i Q.i p := coprod.map P.p Q.p - exp := by { sorry - -- functor := sorry -- prove that the sum of exponentiables is exponentiable. - -- adj := sorry - } + exp := by { + refine { exists_rightAdjoint := by { + have F : Over (P.E ⨿ Q.E) ⥤ Over (P.B ⨿ Q.B) := sorry + use F + haveI : HasBinaryCoproducts (Over (P.E ⨿ Q.E)) := by { + sorry + } + have hf : PreservesPullbacksOfInclusions F := by { + sorry + } + sorry + + + + + + + } + }} o := coprod.desc P.o Q.o +--#check PreservesPullbacksOfInclusions + +--#check PreservesPullbacksOfInclusions.preservesPullbackInl + + +/-For sums: assuming extensiveness, you can express the slice over +the sum as the product of slices. Then you can calculate pullback + as the product of two functors, amd then you take the products of their adjoints-/ /-- The product of two polynomials in many variables. -/ -def prod {I O : C} [HasBinaryProducts C] [FinitaryExtensive C] (P Q : MvPoly I O) : MvPoly I O where +def prod {I O : C} [HasBinaryProducts C] [FinitaryExtensive C] (P Q : MvPoly I O) : + MvPoly I O where E := (pullback (P.p ≫ P.o) Q.o) ⨿ (pullback P.o (Q.p ≫ Q.o)) B := pullback P.o Q.o i := coprod.desc (pullback.fst _ _ ≫ P.i) (pullback.snd _ _ ≫ Q.i) - p := coprod.desc (pullback.map _ _ _ _ P.p (𝟙 _) (𝟙 _) (by aesop) (by aesop)) (pullback.map _ _ _ _ (𝟙 _) Q.p (𝟙 _) (by aesop) (by aesop)) - exp := sorry -- by extensivity -- PreservesPullbacksOfInclusions - o := pullback.fst (P.o) Q.o ≫ P.o + p := coprod.desc (pullback.map _ _ _ _ P.p (𝟙 _) (𝟙 _) + (comp_id _) (by rw [comp_id, id_comp])) + (pullback.map _ _ _ _ (𝟙 _) Q.p (𝟙 _) + (by rw [comp_id, id_comp]) (comp_id _)) + exp := by { + refine { exists_rightAdjoint := by {sorry + + } + + } + } -- by extensivity -- PreservesPullbacksOfInclusions + o := pullback.fst (P.o) Q.o ≫ P.o +#exit protected def functor {I O : C} (P : MvPoly I O) : Over I ⥤ Over O := (Over.pullback P.i) ⋙ (pushforward P.p) ⋙ (Over.map P.o) variable (I O : C) (P : MvPoly I O) -def apply {I O : C} (P : MvPoly I O) [ExponentiableMorphism P.p] : Over I → Over O := (P.functor).obj +def apply {I O : C} (P : MvPoly I O) [ExponentiableMorphism P.p] : + Over I → Over O := (P.functor).obj /-TODO: write a coercion from `MvPoly` to a functor for evaluation of polynomials at a given object.-/ diff --git a/blueprint/src/chapter/all.tex b/blueprint/src/chapter/all.tex index bf24d5b..e106a43 100644 --- a/blueprint/src/chapter/all.tex +++ b/blueprint/src/chapter/all.tex @@ -14,6 +14,8 @@ \chapter{Univaiate Polynomial Functors} \input{chapter/uvpoly} \chapter{Multivariate Polynomial Functors} \input{chapter/mvpoly} +\chapter{Test} +\input{chapter/mvpoly} % \bibliography{refs.bib}{} % \bibliographystyle{alpha} From 46a5df7053434fd2df4da9058d2db076fb2484a2 Mon Sep 17 00:00:00 2001 From: mkaratarakis Date: Mon, 7 Apr 2025 15:51:38 +0200 Subject: [PATCH 03/13] blueprint stuff --- Poly/MvPoly.lean | 2 +- blueprint/src/chapter/mvpoly.tex | 139 ++++++++++++++++++++++++++++++- 2 files changed, 139 insertions(+), 2 deletions(-) diff --git a/Poly/MvPoly.lean b/Poly/MvPoly.lean index b994196..3ff43d7 100644 --- a/Poly/MvPoly.lean +++ b/Poly/MvPoly.lean @@ -127,7 +127,7 @@ def prod {I O : C} [HasBinaryProducts C] [FinitaryExtensive C] (P Q : MvPoly I O } } -- by extensivity -- PreservesPullbacksOfInclusions o := pullback.fst (P.o) Q.o ≫ P.o -#exit + protected def functor {I O : C} (P : MvPoly I O) : Over I ⥤ Over O := (Over.pullback P.i) ⋙ (pushforward P.p) ⋙ (Over.map P.o) diff --git a/blueprint/src/chapter/mvpoly.tex b/blueprint/src/chapter/mvpoly.tex index efe7e7f..c324f63 100644 --- a/blueprint/src/chapter/mvpoly.tex +++ b/blueprint/src/chapter/mvpoly.tex @@ -1 +1,138 @@ -To be written +\begin{definition} + We define a \myemph{polynomial} over $\catE$ to be a diagram $F$ in $\catE$ of shape + \begin{equation} + \lean{MvPoly} + \label{equ:poly} + \xymatrix{ + I & B \ar[l]_s \ar[r]^f & A \ar[r]^t & J \, . } + \end{equation} + We define $\poly{F}:\slice I \to \slice J$ as the composite + \[ + \xymatrix{ + \slice{I} \ar[r]^{\pbk{s}} & \slice{B} \ar[r]^{\radj{f}} & \slice{A} \ar[r]^{\ladj{t}} & \slice{J} \, . } + \] + We refer to $\poly{F}$ as the \myemph{polynomial functor} associated to $F$, or + the \myemph{extension} of $F$, and say that $F$ \myemph{represents} $\poly F$. +\end{definition} + +\begin{definition} +\lean{MvPoly.sum} +\uses{structure:MvPoly} +The sum of two polynomials in many variables. +\end{definition} + +\begin{definition} +\lean{MvPoly.prod} +\uses{structure:MvPoly} +The product of two polynomials in many variables. +\end{definition} + +\begin{para}\label{para:BC-distr} + We shall make frequent use of the Beck-Chevalley isomorphisms and + of the distributivity law of dependent sums over dependent + products~\cite{MoerdijkI:weltc}. Given a cartesian square + \[ + \xymatrix { + \cdot \drpullback \ar[r]^g \ar[d]_u & \cdot \ar[d]^v \\ + \cdot \ar[r]_f & \cdot + } + \] + the Beck-Chevalley isomorphisms are + \[ + \ladj g \, \pbk u \iso \pbk v \, \ladj f \qquad \text{and} \qquad + \radj g \, \pbk u \iso \pbk v \, \radj f \,. + \] + + Given maps $C \stackrel u \longrightarrow B \stackrel f \longrightarrow A$, + we can construct the diagram + \begin{equation}\label{distr-diag} + \xymatrixrowsep{40pt} + \xymatrixcolsep{27pt} + \vcenter{\hbox{ + \xymatrix @!=0pt { + &N \drpullback \ar[rr]^g \ar[ld]_e \ar[dd]^{w=\pbk f(v)}&& M \ar[dd]^{v=\radj f (u)} \\ + C \ar[rd]_u && & \\ + &B \ar[rr]_f && A\,, + }}} + \end{equation} + where $w = \pbk f\, \radj f(u)$ and $e$ is the counit + of $\pbk{f} \adjoint \radj{f}$. + For such diagrams the following + distributive law holds: + \begin{equation}\label{distr-law} + \radj f \, \ladj u \iso \ladj v \, \radj g \, \pbk e \,. + \end{equation} + +\begin{para} +\label{para:comp} +\lean{MvPoly.comp} +\uses{structure:MvPoly} +We now define the operation of substitution of polynomials, and show that the + extension of substitution is composition of polynomial functors, as expected. + In particular, the composite of two polynomial functors is again polynomial. + Given polynomials +\[ +\xymatrix{ + & B \ar[r]^f \ar[dl]_{s} & A \ar[dr]^{t} & \\ + I \ar@{}[rrr]|{F} & & & J } \qquad +\xymatrix{ + & D \ar[r]^g \ar[dl]_{u} & C \ar[dr]^{v} \\ +J \ar@{}[rrr]|{G}& & & K } +\] +we say that $F$ is a polynomial \myemph{from} $I$ \myemph{to} $J$ (and $G$ from +$J$ to $K$), and +we define $G\circ F$, the \myemph{substitution} of $F$ into $G$, to be the polynomial +$I \leftarrow N \to M \to K$ constructed via this diagram: +\begin{equation} +\label{equ:compspan} +\xycenter{ + & & & N \ar[dl]_{n} \ar[rr]^{p} \ar@{}[dr] |{(iv)} +& & D' +\ar[dl]^{\varepsilon} \ar[r]^{q} \ar@{}[ddr] |{(ii)} & +M \ar[dd]^{w} & \\ + & & B' \ar[dl]_{m} \ar[rr]^{r} \ar@{} [dr]|{(iii)} +& & A' \ar[dr]^{k} \ar[dl]_{h} +\ar@{} [dd] |{(i)} +& & & \\ + & B \ar[rr]^f \ar[dl]_{s} & & A \ar[dr]_{t} & & D \ar[dl]^{u} +\ar[r]^{g} & C \ar[dr]^{v} & \\ +I & & & & J & & & K } +\end{equation} +Square $(i)$ is cartesian, and $(ii)$ is a distributivity diagram +like \eqref{distr-diag}: $w$ is obtained +by applying $\radj{g}$ to $k$, and $D'$ is the pullback of $M$ along $g$. +The arrow $\varepsilon: D' \to A'$ is the $k$-component of the counit of +the adjunction $\ladj g \adjoint \pbk g$. +Finally, the squares $(iii)$ and $(iv)$ are +cartesian. +\end{para} + +\begin{proposition}\label{thm:subst} +\lean{MvPoly.comp.functor} +\uses{structure:MvPoly, def:MvPoly.comp} +There is a natural isomorphism + $$ + \poly{G\circ F} \iso \poly{G} \circ \poly{F} . + $$ +\end{proposition} + +\begin{proof} + Referring to Diagram~\eqref{equ:compspan} we have + the following chain of natural isomorphisms: +\begin{eqnarray*} +\extension{G} \circ \extension{F} & = & \ladj{v} \, \radj{g} \, \pbk{u} \; \ladj{t} \, \radj{f} +\, \pbk{s} \\ +& \iso & \ladj{v} \, \radj{g} \, \ladj{k} \, \pbk{h} \, \radj{f} \, \pbk{s}\\ + & \iso & +\ladj{v} \, \ladj{w} \, \radj{q} \, \pbk{\varepsilon} \, \pbk{h} \, \radj{f} \, \pbk{s}\\ +& \iso & +\ladj{v} \, \ladj{w} \, \radj{q} \, \radj{p} \, \pbk{n} \, \pbk{m} \, \pbk{s}\\ +& \iso & +\ladj{(v\, w)} \, \radj{(q \, p)} \, \pbk{(s\, m\, n)}\, \\ +& = & \extension{G \circ F}\,. +\end{eqnarray*} +Here we used the Beck-Chevalley isomorphism for the cartesian square +$(i)$, the distributivity law for $(ii)$, Beck-Chevalley isomorphism +for the cartesian squares $(iii)$ and $(iv)$, and finally pseudo-functoriality +of the pullback functors and their adjoints. +\end{proof} From 084597086419d500b1a675ca829a000353d494a6 Mon Sep 17 00:00:00 2001 From: mkaratarakis Date: Mon, 7 Apr 2025 15:52:27 +0200 Subject: [PATCH 04/13] def --- blueprint/src/chapter/mvpoly.tex | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/blueprint/src/chapter/mvpoly.tex b/blueprint/src/chapter/mvpoly.tex index c324f63..5f73460 100644 --- a/blueprint/src/chapter/mvpoly.tex +++ b/blueprint/src/chapter/mvpoly.tex @@ -1,4 +1,4 @@ -\begin{definition} +\begin{def} We define a \myemph{polynomial} over $\catE$ to be a diagram $F$ in $\catE$ of shape \begin{equation} \lean{MvPoly} @@ -13,19 +13,19 @@ \] We refer to $\poly{F}$ as the \myemph{polynomial functor} associated to $F$, or the \myemph{extension} of $F$, and say that $F$ \myemph{represents} $\poly F$. -\end{definition} +\end{def} -\begin{definition} +\begin{def} \lean{MvPoly.sum} \uses{structure:MvPoly} The sum of two polynomials in many variables. -\end{definition} +\end{def} -\begin{definition} +\begin{def} \lean{MvPoly.prod} \uses{structure:MvPoly} The product of two polynomials in many variables. -\end{definition} +\end{def} \begin{para}\label{para:BC-distr} We shall make frequent use of the Beck-Chevalley isomorphisms and From cc3001450c89ee519a3c3e447b26f531d0ac0631 Mon Sep 17 00:00:00 2001 From: mkaratarakis Date: Mon, 7 Apr 2025 15:53:16 +0200 Subject: [PATCH 05/13] etc --- blueprint/src/chapter/mvpoly.tex | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/blueprint/src/chapter/mvpoly.tex b/blueprint/src/chapter/mvpoly.tex index 5f73460..20f836b 100644 --- a/blueprint/src/chapter/mvpoly.tex +++ b/blueprint/src/chapter/mvpoly.tex @@ -1,5 +1,5 @@ \begin{def} - We define a \myemph{polynomial} over $\catE$ to be a diagram $F$ in $\catE$ of shape + We define a polynomial} over $\catE$ to be a diagram $F$ in $\catE$ of shape \begin{equation} \lean{MvPoly} \label{equ:poly} @@ -11,8 +11,8 @@ \xymatrix{ \slice{I} \ar[r]^{\pbk{s}} & \slice{B} \ar[r]^{\radj{f}} & \slice{A} \ar[r]^{\ladj{t}} & \slice{J} \, . } \] - We refer to $\poly{F}$ as the \myemph{polynomial functor} associated to $F$, or - the \myemph{extension} of $F$, and say that $F$ \myemph{represents} $\poly F$. + We refer to $\poly{F}$ as the polynomial functor associated to $F$, or + the extension of $F$, and say that $F$ represents $\poly F$. \end{def} \begin{def} @@ -79,9 +79,9 @@ & D \ar[r]^g \ar[dl]_{u} & C \ar[dr]^{v} \\ J \ar@{}[rrr]|{G}& & & K } \] -we say that $F$ is a polynomial \myemph{from} $I$ \myemph{to} $J$ (and $G$ from +we say that $F$ is a polynomial from $I$ to $J$ (and $G$ from $J$ to $K$), and -we define $G\circ F$, the \myemph{substitution} of $F$ into $G$, to be the polynomial +we define $G\circ F$, the substitution of $F$ into $G$, to be the polynomial $I \leftarrow N \to M \to K$ constructed via this diagram: \begin{equation} \label{equ:compspan} From 497c3872df9f9824aab94f25610aebb86c25b72c Mon Sep 17 00:00:00 2001 From: mkaratarakis Date: Mon, 7 Apr 2025 15:54:01 +0200 Subject: [PATCH 06/13] f --- blueprint/src/chapter/mvpoly.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/blueprint/src/chapter/mvpoly.tex b/blueprint/src/chapter/mvpoly.tex index 20f836b..0788c06 100644 --- a/blueprint/src/chapter/mvpoly.tex +++ b/blueprint/src/chapter/mvpoly.tex @@ -1,5 +1,5 @@ \begin{def} - We define a polynomial} over $\catE$ to be a diagram $F$ in $\catE$ of shape + We define a polynomial over $\catE$ to be a diagram $F$ in $\catE$ of shape \begin{equation} \lean{MvPoly} \label{equ:poly} From aa3ae6b105b077e9e4ec645e1c7acb870298a1fb Mon Sep 17 00:00:00 2001 From: mkaratarakis Date: Mon, 7 Apr 2025 15:54:41 +0200 Subject: [PATCH 07/13] C --- blueprint/src/chapter/mvpoly.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/blueprint/src/chapter/mvpoly.tex b/blueprint/src/chapter/mvpoly.tex index 0788c06..c07852d 100644 --- a/blueprint/src/chapter/mvpoly.tex +++ b/blueprint/src/chapter/mvpoly.tex @@ -1,5 +1,5 @@ \begin{def} - We define a polynomial over $\catE$ to be a diagram $F$ in $\catE$ of shape + We define a polynomial over C to be a diagram $F$ in C of shape \begin{equation} \lean{MvPoly} \label{equ:poly} From 68be167aa8e27c5f33da834151ec5177ac076cc0 Mon Sep 17 00:00:00 2001 From: mkaratarakis Date: Tue, 8 Apr 2025 01:14:11 +0200 Subject: [PATCH 08/13] blueprint --- blueprint/src/chapter/mvpoly.tex | 1 + 1 file changed, 1 insertion(+) diff --git a/blueprint/src/chapter/mvpoly.tex b/blueprint/src/chapter/mvpoly.tex index c07852d..a014053 100644 --- a/blueprint/src/chapter/mvpoly.tex +++ b/blueprint/src/chapter/mvpoly.tex @@ -21,6 +21,7 @@ The sum of two polynomials in many variables. \end{def} + \begin{def} \lean{MvPoly.prod} \uses{structure:MvPoly} From 4ebeeb66a4160b9dfc92c878dbd9b720189c80ea Mon Sep 17 00:00:00 2001 From: mkaratarakis Date: Tue, 8 Apr 2025 14:30:09 +0200 Subject: [PATCH 09/13] blueprint --- blueprint/src/chapter/mvpoly.tex | 1 - 1 file changed, 1 deletion(-) diff --git a/blueprint/src/chapter/mvpoly.tex b/blueprint/src/chapter/mvpoly.tex index a014053..c07852d 100644 --- a/blueprint/src/chapter/mvpoly.tex +++ b/blueprint/src/chapter/mvpoly.tex @@ -21,7 +21,6 @@ The sum of two polynomials in many variables. \end{def} - \begin{def} \lean{MvPoly.prod} \uses{structure:MvPoly} From 202cdb3bcdebfb5b59bd0c8751f4313308620a9a Mon Sep 17 00:00:00 2001 From: mkaratarakis Date: Tue, 8 Apr 2025 14:36:06 +0200 Subject: [PATCH 10/13] blueprint? --- blueprint/src/chapter/mvpoly.tex | 1 + 1 file changed, 1 insertion(+) diff --git a/blueprint/src/chapter/mvpoly.tex b/blueprint/src/chapter/mvpoly.tex index f0fbdb3..662d98c 100644 --- a/blueprint/src/chapter/mvpoly.tex +++ b/blueprint/src/chapter/mvpoly.tex @@ -64,6 +64,7 @@ \radj f \, \ladj u \iso \ladj v \, \radj g \, \pbk e \,. \end{equation} + \begin{para} \label{para:comp} \lean{MvPoly.comp} From f0581a24ca19f597403411c7956368f7b29496d4 Mon Sep 17 00:00:00 2001 From: mkaratarakis Date: Tue, 8 Apr 2025 14:42:48 +0200 Subject: [PATCH 11/13] fix build --- Poly/MvPoly/Basic.lean | 4 ---- 1 file changed, 4 deletions(-) diff --git a/Poly/MvPoly/Basic.lean b/Poly/MvPoly/Basic.lean index 82d1e48..b65f5ee 100644 --- a/Poly/MvPoly/Basic.lean +++ b/Poly/MvPoly/Basic.lean @@ -81,7 +81,6 @@ def sum {I O : C} [HasBinaryCoproducts C] (P Q : MvPoly I O) : MvPoly I O where B := P.B ⨿ Q.B i := coprod.desc P.i Q.i p := coprod.map P.p Q.p -<<<<<<< HEAD:Poly/MvPoly.lean exp := by { refine { exists_rightAdjoint := by { have F : Over (P.E ⨿ Q.E) ⥤ Over (P.B ⨿ Q.B) := sorry @@ -101,9 +100,6 @@ def sum {I O : C} [HasBinaryCoproducts C] (P Q : MvPoly I O) : MvPoly I O where } }} -======= - exp := sorry ->>>>>>> refs/remotes/origin/master:Poly/MvPoly/Basic.lean o := coprod.desc P.o Q.o --#check PreservesPullbacksOfInclusions From 1edd7cb1cdaf19797bcfb9343da939f28a615043 Mon Sep 17 00:00:00 2001 From: mkaratarakis Date: Tue, 8 Apr 2025 14:57:15 +0200 Subject: [PATCH 12/13] fix --- Poly/MvPoly/Basic.lean | 5 ----- 1 file changed, 5 deletions(-) diff --git a/Poly/MvPoly/Basic.lean b/Poly/MvPoly/Basic.lean index b65f5ee..bd47bb5 100644 --- a/Poly/MvPoly/Basic.lean +++ b/Poly/MvPoly/Basic.lean @@ -61,11 +61,6 @@ example [HasInitial C] {X Y : C} (f : Y ⟶ X) : /-- Given an object `X`, The unique map `initial.to X : ⊥_ C ⟶ X ` is exponentiable. -/ instance [HasInitial C] (X : C) : ExponentiableMorphism (initial.to X) := sorry - -- functor := { - -- obj := sorry - -- map := sorry - -- } - -- adj := sorry /-- The constant polynomial in many variables: for this we need the initial object. -/ def const {I O : C} [HasInitial C] (A : C) [HasBinaryProduct O A] : MvPoly I O := From 6b010195b93fe5166e1436801e2048f2cd49610c Mon Sep 17 00:00:00 2001 From: mkaratarakis Date: Tue, 8 Apr 2025 14:58:05 +0200 Subject: [PATCH 13/13] etc