Cartesian natural transformation

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,10 +80,10 @@ 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`:
@@ -100,21 +100,28 @@ 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
+  V                        V
+  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`.
@@ -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

Poly/ForMathlib/CategoryTheory/NatTrans.lean

@@ -5,6 +5,7 @@ Authors: Sina Hazratpour
 -/
 
 import Mathlib.CategoryTheory.NatTrans
+import Mathlib.CategoryTheory.Functor.TwoSquare
 import Mathlib.CategoryTheory.Limits.Shapes.Pullback.CommSq
 
 open CategoryTheory Limits IsPullback
@@ -20,75 +21,93 @@ namespace NatTrans
 
 open Functor
 
-/-- A natural transformation is cartesian if every commutative square of the following form is
-a pullback.
-```
-F(X) → F(Y)
- ↓      ↓
-G(X) → G(Y)
-```
--/
-def cartesian {F G : J ⥤ C} (α : F ⟶ G) : Prop :=
+/-- A natural transformation is *cartesian*
+if all its naturality squares are pullbacks. -/
+def IsCartesian {F G : J ⥤ C} (α : F ⟶ G) : Prop :=
   ∀ ⦃i j : J⦄ (f : i ⟶ j), IsPullback (F.map f) (α.app i) (α.app j) (G.map f)
 
-theorem cartesian_of_isIso {F G : J ⥤ C} (α : F ⟶ G) [IsIso α] : cartesian α :=
+theorem isCartesian_of_isIso {F G : J ⥤ C} (α : F ⟶ G) [IsIso α] : IsCartesian α :=
   fun _ _ f => IsPullback.of_vert_isIso ⟨NatTrans.naturality _ f⟩
 
-theorem isIso_of_cartesian [HasTerminal J] {F G : J ⥤ C} (α : F ⟶ G) (hα : cartesian α)
+theorem isIso_of_isCartesian [HasTerminal J] {F G : J ⥤ C} (α : F ⟶ G) (hα : IsCartesian α)
     [IsIso (α.app (⊤_ J))] : IsIso α := by
   refine @NatIso.isIso_of_isIso_app _ _ _ _ _ _ α
     (fun j ↦ isIso_snd_of_isIso <| hα <| terminal.from j)
 
-theorem cartesian.comp {F G H : J ⥤ C} {α : F ⟶ G} {β : G ⟶ H} (hα : cartesian α)
-    (hβ : cartesian β) : cartesian (α ≫ β) :=
-  fun _ _ f => (hα f).paste_vert (hβ f)
-
-theorem cartesian.whiskerRight {F G : J ⥤ C} {α : F ⟶ G} (hα : cartesian α)
-    (H : C ⥤ D) [∀ (i j : J) (f : j ⟶ i), PreservesLimit (cospan (α.app i) (G.map f)) H] :
-    cartesian (whiskerRight α H) :=
-  fun _ _ f => (hα f).map H
-
-theorem cartesian.whiskerLeft {K : Type*} [Category K]  {F G : J ⥤ C} {α : F ⟶ G}
-    (hα : cartesian α) (H : K ⥤ J) : cartesian (whiskerLeft H α) :=
-  fun _ _ f => hα (H.map f)
-
-theorem cartesian.comp_horizz {M N K : Type*}
-  [Category M] [Category N] [Category K] {F G : J ⥤ C} {M N : C ⥤ K} {α : F ⟶ G} {β : M ⟶ N}
-  (hα : cartesian α) (hβ : cartesian β)
-  [∀ (i j : J) (f : j ⟶ i), PreservesLimit (cospan (α.app i) (G.map f)) M] :
-    cartesian (NatTrans.hcomp α β) := by {
-      have ha := cartesian.whiskerRight hα M
-      have hb := cartesian.whiskerLeft hβ G
-      have hc := cartesian.comp ha hb
-      unfold cartesian
-      intros i j f
-      specialize hc f
-      simp only [Functor.comp_obj, Functor.comp_map, comp_app,
-        whiskerRight_app, whiskerLeft_app,
-        naturality] at hc
-      exact hc
-    }
-
-theorem cartesian_of_discrete {ι : Type*} {F G : Discrete ι ⥤ C}
-    (α : F ⟶ G) : cartesian α := by
+theorem isCartesian_of_discrete {ι : Type*} {F G : Discrete ι ⥤ C}
+    (α : F ⟶ G) : IsCartesian α := by
   rintro ⟨i⟩ ⟨j⟩ ⟨⟨rfl : i = j⟩⟩
   simp only [Discrete.functor_map_id]
   exact IsPullback.of_horiz_isIso ⟨by rw [Category.id_comp, Category.comp_id]⟩
 
-theorem cartesian_of_isPullback_to_terminal [HasTerminal J] {F G : J ⥤ C} (α : F ⟶ G)
+theorem isCartesian_of_isPullback_to_terminal [HasTerminal J] {F G : J ⥤ C} (α : F ⟶ G)
     (pb : ∀ j,
     IsPullback (F.map (terminal.from j)) (α.app j) (α.app (⊤_ J)) (G.map (terminal.from j))) :
-    cartesian α := by
+    IsCartesian α := by
   intro i j f
   apply IsPullback.of_right (h₁₂ := F.map (terminal.from j)) (h₂₂ := G.map (terminal.from j))
   simpa [← F.map_comp, ← G.map_comp]  using (pb i)
   exact α.naturality f
   exact pb j
 
+namespace IsCartesian
 
-end NatTrans
+theorem comp {F G H : J ⥤ C} {α : F ⟶ G} {β : G ⟶ H} (hα : IsCartesian α) (hβ : IsCartesian β) :
+    IsCartesian (α ≫ β) :=
+  fun _ _ f => (hα f).paste_vert (hβ f)
+
+theorem whiskerRight {F G : J ⥤ C} {α : F ⟶ G} (hα : IsCartesian α) (H : C ⥤ D)
+    [∀ (i j : J) (f : j ⟶ i), PreservesLimit (cospan (α.app i) (G.map f)) H] :
+    IsCartesian (whiskerRight α H) :=
+  fun _ _ f => (hα f).map H
 
-open NatTrans
+theorem whiskerLeft {K : Type*} [Category K] {F G : J ⥤ C}
+    {α : F ⟶ G} (hα : IsCartesian α) (H : K ⥤ J) : IsCartesian (whiskerLeft H α) :=
+  fun _ _ f => hα (H.map f)
 
-theorem mapPair_cartesian {F F' : Discrete WalkingPair ⥤ C} (α : F ⟶ F') : cartesian α :=
-  cartesian_of_discrete α
+theorem hcomp {K : Type*} [Category K] {F G : J ⥤ C} {M N : C ⥤ K} {α : F ⟶ G} {β : M ⟶ N}
+    (hα : IsCartesian α) (hβ : IsCartesian β)
+    [∀ (i j : J) (f : j ⟶ i), PreservesLimit (cospan (α.app i) (G.map f)) M] :
+    IsCartesian (NatTrans.hcomp α β) := by
+  have ha := hα.whiskerRight M
+  have hb := hβ.whiskerLeft G
+  have hc := ha.comp hb
+  unfold IsCartesian
+  intros i j f
+  specialize hc f
+  simp only [Functor.comp_obj, Functor.comp_map, comp_app,
+    whiskerRight_app, whiskerLeft_app,
+    naturality] at hc
+  exact hc
+
+open TwoSquare
+
+variable {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄}
+  [Category.{v₁} C₁] [Category.{v₂} C₂] [Category.{v₃} C₃] [Category.{v₄} C₄]
+  {T : C₁ ⥤ C₂} {L : C₁ ⥤ C₃} {R : C₂ ⥤ C₄} {B : C₃ ⥤ C₄}
+variable {C₅ : Type u₅} {C₆ : Type u₆} {C₇ : Type u₇} {C₈ : Type u₈}
+  [Category.{v₅} C₅] [Category.{v₆} C₆] [Category.{v₇} C₇] [Category.{v₈} C₈]
+  {T' : C₂ ⥤ C₅} {R' : C₅ ⥤ C₆} {B' : C₄ ⥤ C₆} {L' : C₃ ⥤ C₇} {R'' : C₄ ⥤ C₈} {B'' : C₇ ⥤ C₈}
+
+theorem vComp {w : TwoSquare T L R B} {w' : TwoSquare B L' R'' B''}
+    [∀ (i j : C₁) (f : j ⟶ i), PreservesLimit (cospan (w.app i) ((L ⋙ B).map f)) R''] :
+    IsCartesian w → IsCartesian w' → IsCartesian (w ≫ᵥ w') :=
+  fun cw cw' =>
+    (isCartesian_of_isIso _).comp <|
+    (cw.whiskerRight _).comp <|
+    (isCartesian_of_isIso _).comp <|
+    (cw'.whiskerLeft _).comp <|
+    (isCartesian_of_isIso _)
+
+theorem hComp {w : TwoSquare T L R B} {w' : TwoSquare T' R R' B'}
+    [∀ (i j : C₁) (f : j ⟶ i), PreservesLimit (cospan (w.app i) ((L ⋙ B).map f)) B'] :
+    IsCartesian w → IsCartesian w' → IsCartesian (w ≫ₕ w') :=
+  fun cw cw' =>
+    (isCartesian_of_isIso _).comp <|
+    (cw'.whiskerLeft _).comp <|
+    (isCartesian_of_isIso _).comp <|
+    (cw.whiskerRight _).comp <|
+    (isCartesian_of_isIso _)
+
+end IsCartesian
+end NatTrans