Cartesian natural transformation (#31)

* feat: start proving that cartesian NTs are cartesian

* feat: counit of mapPullbackAdj is cartesian

* chore: cleanup

* fix: stray typeclass

* feat: finish proof

* doc: consistent TwoSquare convention

Author: Vtec234

Poly/ForMathlib/CategoryTheory/CommSq.lean

@@ -0,0 +1,21 @@
+/-
+Copyright (c) 2025 Wojciech Nawrocki. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Nawrocki
+-/
+import Mathlib.CategoryTheory.CommSq
+
+namespace CategoryTheory.Functor
+
+theorem reflect_commSq
+    {C D : Type*} [Category C] [Category D]
+    (F : C ⥤ D) [Functor.Faithful F]
+    {X Y Z W : C} {f : X ⟶ Y} {g : X ⟶ Z} {h : Y ⟶ W} {i : Z ⟶ W} :
+    CommSq (F.map f) (F.map g) (F.map h) (F.map i) →
+    CommSq f g h i := by
+  intro cs
+  constructor
+  apply Functor.map_injective F
+  simpa [← Functor.map_comp] using cs.w
+
+end CategoryTheory.Functor

Poly/ForMathlib/CategoryTheory/Comma/Over/Basic.lean

@@ -35,6 +35,10 @@ lemma homMk_comp'_assoc {X Y Z W : T} (f : X ⟶ Y) (g : Y ⟶ Z) (h : Z ⟶ W)
 lemma homMk_id {X B : T} (f : X ⟶ B) (h : 𝟙 X ≫ f = f) : homMk (𝟙 X) h = 𝟙 (mk f) :=
   rfl
 
+@[simp]
+theorem mkIdTerminal_from_left {B : T} (U : Over B) : (mkIdTerminal.from U).left = U.hom := by
+  simp [mkIdTerminal, CostructuredArrow.mkIdTerminal, Limits.IsTerminal.from, Functor.preimage]
+
 /-- `Over.Sigma Y U` is a shorthand for `(Over.map Y.hom).obj U`.
 This is a category-theoretic analogue of `Sigma` for types. -/
 abbrev Sigma {X : T} (Y : Over X) (U : Over (Y.left)) : Over X :=

Poly/ForMathlib/CategoryTheory/Comma/Over/Pullback.lean

@@ -8,7 +8,8 @@ import Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
 import Mathlib.CategoryTheory.Limits.Constructions.Over.Basic
 import Mathlib.CategoryTheory.Monad.Products
 import Poly.ForMathlib.CategoryTheory.Comma.Over.Basic
-
+import Poly.ForMathlib.CategoryTheory.NatTrans
+import Poly.ForMathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq
 
 noncomputable section
 
@@ -24,6 +25,19 @@ variable {C : Type u₁} [Category.{v₁} C]
 
 namespace Over
 
+theorem isCartesian_mapPullbackAdj_counit [HasPullbacks C] {X Y : C} (f : X ⟶ Y) :
+    NatTrans.IsCartesian (Over.mapPullbackAdj f).counit := by
+  intro A B U
+  apply IsPullback.of_right
+    (h₁₂ := Over.homMk (V := Over.mk f) (pullback.snd B.hom f) <| by simp)
+    (v₁₃ := Over.mkIdTerminal.from _)
+    (h₂₂ := Over.mkIdTerminal.from _)
+  case p => ext; simp
+  . apply (Over.forget Y).reflect_isPullback
+    convert (IsPullback.of_hasPullback A.hom f).flip using 1 <;> simp
+  . apply (Over.forget Y).reflect_isPullback
+    convert (IsPullback.of_hasPullback B.hom f).flip using 1 <;> simp
+
 /-- The reindexing of `Z : Over X` along `Y : Over X`, defined by pulling back `Z` along
 `Y.hom : Y.left ⟶ X`. -/
 abbrev Reindex [HasPullbacks C] {X : C} (Y : Over X) (Z : Over X) : Over Y.left :=

Poly/ForMathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean

@@ -0,0 +1,30 @@
+/-
+Copyright (c) 2025 Wojciech Nawrocki. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Wojciech Nawrocki
+-/
+import Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq
+import Poly.ForMathlib.CategoryTheory.CommSq
+
+namespace CategoryTheory.Functor
+open Limits
+
+theorem reflect_isPullback
+    {C D : Type*} [Category C] [Category D] (F : C ⥤ D)
+    {X Y Z W : C} (f : X ⟶ Y) (g : X ⟶ Z) (h : Y ⟶ W) (i : Z ⟶ W)
+    [rl : ReflectsLimit (cospan h i) F] [Functor.Faithful F] :
+    IsPullback (F.map f) (F.map g) (F.map h) (F.map i) →
+    IsPullback f g h i := by
+  intro pb
+  have sq := F.reflect_commSq pb.toCommSq
+  apply IsPullback.mk sq
+  apply rl.reflects
+  let i := cospanCompIso F h i
+  apply IsLimit.equivOfNatIsoOfIso i.symm pb.cone _ _ pb.isLimit
+  let j :
+      ((Cones.postcompose i.symm.hom).obj pb.cone).pt ≅
+      (F.mapCone <| PullbackCone.mk f g sq.w).pt :=
+    Iso.refl _
+  apply WalkingCospan.ext j <;> simp +zetaDelta
+
+end CategoryTheory.Functor

Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/BeckChevalley.lean

@@ -80,41 +80,48 @@ def mapIsoSquare {X Y Z W : C} {h : X ⟶ Z} {f : X ⟶ Y}  {g : Z ⟶ W} {k : Y
     Over.map h ⋙ Over.map g ≅ Over.map f ⋙ Over.map k :=
   eqToIso (map_square_eq sq)
 
-variable [HasBinaryProducts C] [HasPullbacks C]
+variable [HasPullbacks C]
 
 variable {X Y Z W : C} (h : X ⟶ Z) (f : X ⟶ Y) (g : Z ⟶ W) (k : Y ⟶ W)
-(sq : CommSq h f g k)
+  (sq : CommSq h f g k)
 
 /-- The Beck-Chevalley natural transformation `pullback f ⋙ map h ⟶ map k ⋙ pullback g`
 constructed as a mate of `mapIsoSquare`:
 ```
-          Over X -- .map h -> Over Z
-             ↑                  ↑
-.pullback f  |         ↘        | .pullback g
-             |                  |
-          Over Y -- .map k -> Over W
+    Over Y - pullback f → Over X
+      |                     |
+map k |          ↙          | map h
+      ↓                     ↓
+    Over W - pullback g → Over Z
 ```
 -/
 --pullbackBeckChevalleySquare
 def pullbackMapTwoSquare : TwoSquare (pullback f) (map k) (map h) (pullback g) :=
   mateEquiv (mapPullbackAdj f) (mapPullbackAdj g) (mapIsoSquare sq).hom
 
 /--
-The natural transformation `pullback f ⋙ forget X ⟶ forget Y ⋙ 𝟭 C` as the mate the isomorphism
-`mapForget f`:
+The natural transformation `pullback f ⋙ forget X ⟶ forget Y ⋙ 𝟭 C`
+as the mate of the isomorphism `mapForget f`:
 ```
-          Over X --.forget X -> C
-             ↑                  |
-.pullback f  |         ↘        | 𝟭
-             |                  |
-          Over Y --.forget Y -> C
+       Over Y - pullback f → Over X
+         |                     |
+forget Y |          ↙          | forget X
+         ↓                     ↓
+         C ======== 𝟭 ======== C
 ```
 -/
---pullbackForgetBeckChevalleySquare
-def pullbackForgetTwoSquare : TwoSquare (pullback f) (forget Y) (forget X) (𝟭 C) := by
-  let iso := (mapForget f).inv
-  rw [← Functor.comp_id (forget X)] at iso
-  exact (mateEquiv (mapPullbackAdj f) (Adjunction.id)) iso
+def pullbackForgetTwoSquare : TwoSquare (pullback f) (forget Y) (forget X) (𝟭 C) :=
+  mateEquiv (mapPullbackAdj f) Adjunction.id (mapForget f).inv
+
+theorem isCartesian_pullbackForgetTwoSquare {X Y : C} (f : X ⟶ Y) :
+    NatTrans.IsCartesian (pullbackForgetTwoSquare f) := by
+  unfold pullbackForgetTwoSquare
+  simp only [mateEquiv_apply]
+  repeat apply IsCartesian.comp; apply isCartesian_of_isIso
+  apply IsCartesian.comp
+  . apply IsCartesian.whiskerRight
+    apply isCartesian_mapPullbackAdj_counit
+  . apply isCartesian_of_isIso
 
 /-- The natural transformation `pullback f ⋙ forget X ⟶ forget Y`, a variant of
 `pullbackForgetTwoSquare`. -/
@@ -130,7 +137,7 @@ def pullbackMapTriangle (h' : Y ⟶ Z) (w : f ≫ h' = h) :
   let iso := (mapComp f h').hom
   rw [w] at iso
   rw [← Functor.comp_id (map h)] at iso
-  exact (mateEquiv (mapPullbackAdj f) (Adjunction.id)) iso
+  exact (mateEquiv (mapPullbackAdj f) Adjunction.id) iso
 
 /-- The isomorphism between the pullbacks along a commutative square.  This is constructed as the
 conjugate of the `mapIsoSquare`.
@@ -151,11 +158,11 @@ def pullbackIsoSquare : pullback k ⋙ pullback f ≅ pullback g ⋙ pullback h
 `pushforward g ⋙ pullback k ⟶ pullback h ⋙ pushforward f` constructed as a mate of
 `pullbackMapTwoSquare`.
 ```
-              Over X ←-.pullback h-- Over Z
-                |                     |
-.pushforward f  |          ↖          | .pushforward g
-                ↓                     ↓
-              Over Y ←-.pullback k-- Over W
+         Over Z - pushforward g → Over W
+           |                        |
+pullback h |           ↙            | pullback k
+           ↓                        ↓
+         Over X - pushforward f → Over Y
 ```
 -/
 --pushforwardBeckChevalleySquare
@@ -169,12 +176,11 @@ def pushforwardPullbackTwoSquare
 A variant of `pushforwardTwoSquare` involving `star` instead of `pullback`.
 -/
 --pushforwardStarBeckChevalleySquare
-def starPushforwardTriangle
-    [ExponentiableMorphism f]  :
+def starPushforwardTriangle [HasBinaryProducts C] [ExponentiableMorphism f]  :
     star Y ⟶ star X ⋙ pushforward f := by
   let iso := (starPullbackIsoStar f).hom
   rw [← Functor.id_comp (star X)] at iso
-  exact (mateEquiv (Adjunction.id) (adj f)) iso
+  exact (mateEquiv Adjunction.id (adj f)) iso
 
 /-- The conjugate isomorphism between the pushforwards along a commutative square.
 ```

Poly/ForMathlib/CategoryTheory/LocallyCartesianClosed/Distributivity.lean

@@ -92,8 +92,8 @@ def cellLeftTriangle : e f u ≫ u = w f u := by
 def cellLeft : pullback (e f u) ⋙ map (w f u) ⟶ map u :=
   pullbackMapTriangle _ _ _ (cellLeftTriangle f u)
 
-lemma cellLeftCartesian : cartesian (cellLeft f u) := by
-  unfold cartesian
+lemma isCartesian_cellLeft : IsCartesian (cellLeft f u) := by
+  unfold IsCartesian
   simp only [id_obj, mk_left, comp_obj, pullback_obj_left, Functor.comp_map]
   unfold cellLeft
   intros i j f'
@@ -107,8 +107,8 @@ def cellRightCommSq : CommSq (g f u) (w f u) (v f u) f :=
 def cellRight' : pushforward (g f u) ⋙ map (v f u)
   ≅ map (w f u) ⋙ pushforward f := sorry
 
-lemma cellRightCartesian : cartesian (cellRight' f u).hom :=
-  cartesian_of_isIso ((cellRight' f u).hom)
+lemma isCartesian_cellRight' : IsCartesian (cellRight' f u).hom :=
+  isCartesian_of_isIso ((cellRight' f u).hom)
 
 def pasteCell1 : pullback (e f u) ⋙ pushforward (g f u) ⋙ map (v f u) ⟶
   pullback (e f u) ⋙ map (w f u) ⋙ pushforward f := by
@@ -122,19 +122,19 @@ def pasteCell2 : (pullback (e f u) ⋙ map (w f u)) ⋙ pushforward f
 
 def pasteCell := pasteCell1 f u ≫ pasteCell2 f u
 
-def paste : cartesian (pasteCell f u) := by
-  apply cartesian.comp
+def paste : IsCartesian (pasteCell f u) := by
+  apply IsCartesian.comp
   · unfold pasteCell1
-    apply cartesian.whiskerLeft (cellRightCartesian f u)
+    apply (isCartesian_cellRight' f u).whiskerLeft
   · unfold pasteCell2
-    apply cartesian.whiskerRight (cellLeftCartesian f u)
+    apply (isCartesian_cellLeft f u).whiskerRight
 
 -- use `pushforwardPullbackTwoSquare` to construct this iso.
 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)
+  have := isCartesian_of_isPullback_to_terminal (pasteCell f u)
   letI : IsIso ((pasteCell f u).app (⊤_ Over ((𝟭 (Over B)).obj (Over.mk u)).left)) := sorry
-  have := isIso_of_cartesian (pasteCell f u) (paste f u)
+  have := isIso_of_isCartesian (pasteCell f u) (paste f u)
   exact (asIso (pasteCell f u)).symm
 
 end CategoryTheory