feat: exponentiable maps are pullback-stable; comp is exponentiable

Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean

@@ -3,7 +3,7 @@ Copyright (c) 2025 Sina Hazratpour. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sina Hazratpour, Emily Riehl
 -/
-import Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq
+import Mathlib.CategoryTheory.Adjunction.Lifting.Right
 import Poly.ForMathlib.CategoryTheory.LocallyCartesianClosed.Basic
 import Poly.ForMathlib.CategoryTheory.NatTrans
 import Poly.ForMathlib.CategoryTheory.LocallyCartesianClosed.BeckChevalley
@@ -54,11 +54,25 @@ def exponentiableMorphism : ExponentiableMorphism (g f u) := by infer_instance
 
 namespace ExponentiableMorphism
 
+instance mapPullbackAdj_regularMono {C} [Category C] [HasPullbacks C] {A B : C} (F : A ⟶ B)
+    (X : Over A) : RegularMono ((mapPullbackAdj F).unit.app X) := by
+  let FU := Over.map F ⋙ Over.pullback F
+  set η := (mapPullbackAdj F).unit
+  have := congr($((whiskerLeft_comp_whiskerRight η η)).app X)
+  refine ⟨_, _, _, this, Fork.IsLimit.mk' _ fun s => ?_⟩
+  have hi := (Fork.ι s).w; simp at hi
+  have w := congr($(Fork.condition s).left ≫ pullback.fst .. ≫ pullback.snd ..); simp [η] at w
+  refine ⟨homMk (s.ι.left ≫ pullback.fst ..) (by simp [w, hi]), ?_, ?_⟩
+  · ext; simp; ext <;> simp [η]; rw [w]
+  · intro m H; ext; simpa [η] using congr(($H).left ≫ pullback.fst ..)
+
 /-- The pullback of exponentiable morphisms is exponentiable. -/
-def pullback {I J K : C} (f : I ⟶ J) (g : K ⟶ J)
-    [gexp : ExponentiableMorphism g] :
-    ExponentiableMorphism (pullback.fst f g ) :=
-  sorry
+theorem of_isPullback {C' : Type u} [Category.{v} C'] [HasPullbacks C'] [HasTerminal C']
+  {P I J K : C'} {fst : P ⟶ I} {snd : P ⟶ K} {f : I ⟶ J} {g : K ⟶ J}
+    (H : IsPullback fst snd f g) [ExponentiableMorphism g] : ExponentiableMorphism fst :=
+  have : IsLeftAdjoint _ :=
+    ⟨_, ⟨(mapPullbackAdj f).comp (adj g) |>.ofNatIsoLeft (pullbackMapIsoSquare H.flip).symm⟩⟩
+  isLeftAdjoint_triangle_lift (Over.pullback fst) (mapPullbackAdj snd)
 
 end ExponentiableMorphism
 

Poly/UvPoly/Basic.lean

@@ -5,6 +5,7 @@ Authors: Sina Hazratpour, Wojciech Nawrocki
 -/
 
 import Poly.ForMathlib.CategoryTheory.LocallyCartesianClosed.BeckChevalley -- LCCC.BeckChevalley
+import Poly.ForMathlib.CategoryTheory.LocallyCartesianClosed.Distributivity
 import Mathlib.CategoryTheory.Functor.TwoSquare
 import Poly.ForMathlib.CategoryTheory.PartialProduct
 import Poly.ForMathlib.CategoryTheory.NatTrans
@@ -36,7 +37,7 @@ noncomputable section
 
 namespace CategoryTheory
 
-open CategoryTheory Category Limits Functor Adjunction Over ExponentiableMorphism
+open Category Limits Functor Adjunction Over ExponentiableMorphism
   LocallyCartesianClosed
 
 variable {C : Type*} [Category C] [HasPullbacks C]
@@ -52,7 +53,7 @@ namespace UvPoly
 
 open TwoSquare
 
-variable {C : Type*} [Category C] [HasTerminal C] [HasPullbacks C]
+variable [HasTerminal C]
 
 instance : HasBinaryProducts C :=
   hasBinaryProducts_of_hasTerminal_and_pullbacks C
@@ -74,7 +75,7 @@ def prod {E' B'} (P : UvPoly E B) (Q : UvPoly E' B') [HasBinaryCoproducts C] :
 /-- For a category `C` with binary products, `P.functor : C ⥤ C` is the functor associated
 to a single variable polynomial `P : UvPoly E B`. -/
 def functor (P : UvPoly E B) : C ⥤ C :=
-  star E ⋙ pushforward P.p ⋙ forget B
+  star E ⋙ pushforward P.p ⋙ Over.forget B
 
 /-- The evaluation function of a polynomial `P` at an object `X`. -/
 def apply (P : UvPoly E B) : C → C := (P.functor).obj
@@ -93,8 +94,8 @@ variable (B)
 def id : UvPoly B B := ⟨𝟙 B, by infer_instance⟩
 
 /-- The functor associated to the identity polynomial is isomorphic to the identity functor. -/
-def idIso : (UvPoly.id B).functor ≅ star B ⋙ forget B :=
-  isoWhiskerRight (isoWhiskerLeft _ (pushforwardIdIso B)) (forget B)
+def idIso : (UvPoly.id B).functor ≅ star B ⋙ Over.forget B :=
+  isoWhiskerRight (isoWhiskerLeft _ (pushforwardIdIso B)) (Over.forget B)
 
 /-- Evaluating the identity polynomial at an object `X` is isomorphic to `B × X`. -/
 def idApplyIso (X : C) : (id B) @ X ≅ B ⨯ X := sorry
@@ -136,7 +137,7 @@ def verticalNatTrans {F : C} (P : UvPoly E B) (Q : UvPoly F B) (ρ : E ⟶ F) (h
   let cellLeft := (Over.starPullbackIsoStar ρ).hom
   let cellMid := (pushforwardPullbackTwoSquare ρ P.p Q.p (𝟙 _) sq)
   let cellLeftMidPasted := TwoSquare.whiskerRight (cellLeft ≫ₕ cellMid) (Over.pullbackId).inv
-  simpa using (cellLeftMidPasted ≫ₕ (vId (forget B)))
+  simpa using (cellLeftMidPasted ≫ₕ (vId (Over.forget B)))
 
 /-- A cartesian map of polynomials
 ```
@@ -166,7 +167,7 @@ def cartesianNatTrans {D F : C} (P : UvPoly E B) (Q : UvPoly F D)
     (Over.starPullbackIsoStar φ).inv
   let cellMid :  TwoSquare (pullback φ) (pushforward Q.p) (pushforward P.p) (pullback δ) :=
     (pushforwardPullbackIsoSquare pb.flip).inv
-  let cellRight : TwoSquare (pullback δ) (forget D) (forget B) (𝟭 C) :=
+  let cellRight : TwoSquare (pullback δ) (Over.forget D) (Over.forget B) (𝟭 C) :=
     pullbackForgetTwoSquare δ
   let := cellLeft ≫ᵥ cellMid ≫ᵥ cellRight
   this
@@ -217,9 +218,10 @@ def comp {E B F D N M : C} {P : UvPoly E B} {Q : UvPoly F D} {R : UvPoly N M}
 
 end Hom
 
+variable (C) in
 /-- Bundling up the the polynomials over different bases to form the underlying type of the
 category of polynomials. -/
-structure Total (C : Type*) [Category C] [HasPullbacks C] where
+structure Total where
   {E B : C}
   (poly : UvPoly E B)
 
@@ -248,7 +250,7 @@ def Total.ofHom {E' B' : C} (P : UvPoly E B) (Q : UvPoly E' B') (α : P.Hom Q) :
 
 namespace UvPoly
 
-variable {C : Type u} [Category.{v} C] [HasTerminal C] [HasPullbacks C]
+variable [HasTerminal C]
 
 instance : SMul C (Total C) where
   smul S P := Total.of (smul S P.poly)
@@ -275,7 +277,7 @@ def ε (P : UvPoly E B) (X : C) : pullback (P.fstProj X) P.p ⟶ E ⨯ X :=
 
 /-- The partial product fan associated to a polynomial `P : UvPoly E B` and an object `X : C`. -/
 @[simps -isSimp]
-def fan (P : UvPoly E B) (X : C) : Fan P.p X where
+def fan (P : UvPoly E B) (X : C) : PartialProduct.Fan P.p X where
   pt := P @ X
   fst := P.fstProj X
   snd := ε P X ≫ prod.snd -- ((forgetAdjStar E).counit).app X
@@ -286,12 +288,12 @@ attribute [simp] fan_pt fan_fst
 `P.PartialProduct.fan` is in fact a limit fan; this provides the univeral mapping property of the
 polynomial functor.
 -/
-def isLimitFan (P : UvPoly E B) (X : C) : IsLimit (fan P X) where
+def isLimitFan (P : UvPoly E B) (X : C) : PartialProduct.IsLimit (PartialProduct.fan P X) where
   lift c := (pushforwardCurry <| overPullbackToStar c.fst c.snd).left
   fac_left := by aesop_cat (add norm fstProj)
   fac_right := by
     intro c
-    simp only [fan_snd, pullbackMap, ε, ev, ← assoc, ← comp_left]
+    simp only [fan_snd, PartialProduct.pullbackMap, ε, ev, ← assoc, ← comp_left]
     simp_rw [homMk_eta]
     erw [← homEquiv_counit]
     simp [← ExponentiableMorphism.homEquiv_apply_eq, overPullbackToStar_prod_snd]
@@ -302,7 +304,7 @@ def isLimitFan (P : UvPoly E B) (X : C) : IsLimit (fan P X) where
     rw [← homMk_left m (U := Over.mk c.fst) (V := Over.mk (P.fstProj X))]
     congr 1
     apply (Adjunction.homEquiv_apply_eq (adj P.p) (overPullbackToStar c.fst c.snd) (Over.homMk m)).mpr
-    simp [overPullbackToStar, Fan.overPullbackToStar, Fan.over]
+    simp [overPullbackToStar, PartialProduct.Fan.overPullbackToStar, PartialProduct.Fan.over]
     apply (Adjunction.homEquiv_apply_eq _ _ _).mpr
     rw [← h_right]
     simp [forgetAdjStar, comp_homEquiv, Comonad.adj]
@@ -326,13 +328,13 @@ theorem lift_fst {Γ X : C} {P : UvPoly E B} {b : Γ ⟶ B} {e : pullback b P.p
 
 @[reassoc]
 theorem lift_snd {Γ X : C} {P : UvPoly E B} {b : Γ ⟶ B} {e : pullback b P.p ⟶ X} :
-    comparison (c := fan P X) (P.lift b e) ≫ (fan P X).snd =
+    PartialProduct.comparison (c := PartialProduct.fan P X) (P.lift b e) ≫ (fan P X).snd =
     (pullback.congrHom (partialProd.lift_fst b e) rfl).hom ≫ e := partialProd.lift_snd ..
 
 theorem hom_ext {Γ X : C} {P : UvPoly E B} {f g : Γ ⟶ P @ X}
     (h₁ : f ≫ P.fstProj X = g ≫ P.fstProj X)
-    (h₂ : comparison f ≫ (fan P X).snd =
-      (pullback.congrHom (by exact h₁) rfl).hom ≫ comparison g ≫ (fan P X).snd) :
+    (h₂ : PartialProduct.comparison f ≫ (fan P X).snd =
+      (pullback.congrHom (by exact h₁) rfl).hom ≫ PartialProduct.comparison g ≫ (fan P X).snd) :
     f = g := partialProd.hom_ext ⟨fan P X, isLimitFan P X⟩ h₁ h₂
 
 /-- A morphism `f : Γ ⟶ P @ X` projects to a morphism `b : Γ ⟶ B` and a morphism
@@ -361,7 +363,10 @@ def compDom {E B D A : C} (P : UvPoly E B) (Q : UvPoly D A) :=
 def comp [HasPullbacks C] [HasTerminal C]
     {E B D A : C} (P : UvPoly E B) (Q : UvPoly D A) : UvPoly (compDom P Q) (P @ A) where
   p := pullback.snd Q.p (fan P A).snd ≫ pullback.fst (fan P A).fst P.p
-  exp := sorry
+  exp :=
+    haveI := ExponentiableMorphism.of_isPullback (.flip <| .of_hasPullback Q.p (fan P A).snd)
+    haveI := ExponentiableMorphism.of_isPullback (.of_hasPullback (fan P A).fst P.p)
+    inferInstance
 
 /-- The associated functor of the composition of two polynomials is isomorphic to the composition of the associated functors. -/
 def compFunctorIso [HasPullbacks C] [HasTerminal C]