restructring MvPoly

Author: sinhp

Poly.lean

@@ -7,3 +7,4 @@ import Poly.ForMathlib.CategoryTheory.LocallyCartesianClosed.Presheaf
 -- import Poly.Type.Univariate
 -- import Poly.Exponentiable
 import Poly.UvPoly.Basic
+import Poly.MvPoly.Basic

Poly/MvPoly.lean Poly/MvPoly/Basic.leanPoly/MvPoly.lean renamed to Poly/MvPoly/Basic.lean

@@ -24,6 +24,8 @@ import Mathlib.CategoryTheory.Extensive
 
 noncomputable section
 
+namespace CategoryTheory
+
 open CategoryTheory Category Limits Functor Adjunction ExponentiableMorphism
 
 variable {C : Type*} [Category C] [HasPullbacks C] [HasTerminal C] [HasFiniteWidePullbacks C]
@@ -67,7 +69,7 @@ instance [HasInitial C] (X : C) : ExponentiableMorphism (initial.to X) := 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 :=
-  ⟨⊥_ C, prod O A, initial.to I , initial.to _, inferInstance, prod.fst⟩
+  ⟨⊥_ C, Limits.prod O A, initial.to I , initial.to _, inferInstance, prod.fst⟩
 
 /-- The monomial polynomial in many variables. -/
 def monomial {I O E : C} (i : E ⟶ I) (p : E ⟶ O) [ExponentiableMorphism p]: MvPoly I O :=
@@ -79,10 +81,7 @@ 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 := sorry
   o := coprod.desc P.o Q.o
 
 /-- The product of two polynomials in many variables. -/
@@ -246,6 +245,6 @@ def functorIsoFunctor' [HasBinaryProducts C] (P : UvPoly E B) : P.functor ≅ P.
 
 end UvPoly
 
-
+end CategroyTheory
 
 end

blueprint/src/chapter/mvpoly.tex

@@ -10,12 +10,11 @@
   \end{definition}
 
 
-% \begin{definition}[multivariable polynomial functors]
-%   \label{defPolynomialFunctor}
-%   \label{defExtension}
-%   \index{polynomial!functor@{---} functor}
-%   \index{polynomial!extension of a {---}}
-%   The \textbf{extension} of a polynomial $F : \declpoly IBAJsft$ in a locally cartesian closed category $\mathcal{E}$ is the functor $\upP_F = \upSigma_t \upPi_f \upDelta_s : \mathcal{E} \slice{I} \to \mathcal{E} \slice{J}$. Internally, we can define $\upP_F$ by
-%   $$\upP_F \seqbn{X_i}{i \in I} = \seqbn{\sum_{a \in A_j} \prod_{b \in B_a} X_{s(b)}}{j \in J}$$
-%   A \textbf{polynomial functor} is a functor that is naturally isomorphic to the extension of a polynomial.
-%   \end{definition}
+\begin{definition}[extension of polynomial functors]
+  \label{defn:extension}
+  \lean{CategoryTheory.MvPoly.functor} \leanok
+  The \textbf{extension} of a polynomial $\polyspan IBAJipo$ is the functor
+  $\upP = o_! \, f_* \, i^* \colon \catC / I \to \catC/ O$. Internally, we can define $\upP$ by
+  $$\upP \seqbn{X_i}{i \in I} = \seqbn{\sum_{a \in A_j} \prod_{b \in B_a} X_{s(b)}}{j \in J}$$
+  A \textbf{polynomial functor} is a functor that is naturally isomorphic to the extension of a polynomial.
+  \end{definition}

blueprint/src/macros/common.tex

@@ -79,7 +79,9 @@
 \newcommand{\Two}{\bullet+\bullet}
 
 %%% Polynomials
+\newcommand{\polyspan}[7]{#1 \xleftarrow{#5} #2 \xrightarrow{#6} #3 \xrightarrow{#7} #4}
 \newcommand{\PolyComp}{\lhd}
+\newcommand{\upP}{\mathrm{P}}
 \newcommand{\Poly}[1]{P_{#1}}
 \newcommand{\Star}[1]{{#1}^{\star}}
 
@@ -141,6 +143,13 @@
 \newcommand{\Si}{\Sigma}
 \newcommand{\Om}{\Omega}
 
+% % Families
+\newcommand{\setbn}[2]{\left\{\left. #1 \ \middle\rvert\ #2 \right.\right\}}
+\newcommand{\seqbn}[2]{\left(\left. #1 \ \middle\rvert\ #2 \right.\right)}
+\newcommand{\sqseqbn}[2]{\left[\left. #1 \ \middle\rvert\ #2 \right.\right]}
+\newcommand{\append}{\mathbin{^\frown}}
+
+
 % % Misc
 % \newenvironment{bprooftree}
 %   {\leavevmode\hbox\bgroup}