def
CategoryTheory.NatTrans.IsCartesian
{J : Type v'}
[Category.{u', v'} J]
{C : Type u}
[Category.{v, u} C]
{F G : Functor J C}
(α : F ⟶ G)
:
A natural transformation is cartesian if all its naturality squares are pullbacks.
Equations
- CategoryTheory.NatTrans.IsCartesian α = ∀ ⦃i j : J⦄ (f : i ⟶ j), CategoryTheory.IsPullback (F.map f) (α.app i) (α.app j) (G.map f)
Instances For
theorem
CategoryTheory.NatTrans.isCartesian_of_isIso
{J : Type v'}
[Category.{u', v'} J]
{C : Type u}
[Category.{v, u} C]
{F G : Functor J C}
(α : F ⟶ G)
[IsIso α]
:
theorem
CategoryTheory.NatTrans.isIso_of_isCartesian
{J : Type v'}
[Category.{u', v'} J]
{C : Type u}
[Category.{v, u} C]
[Limits.HasTerminal J]
{F G : Functor J C}
(α : F ⟶ G)
(hα : IsCartesian α)
[IsIso (α.app (⊤_ J))]
:
IsIso α
theorem
CategoryTheory.NatTrans.isCartesian_of_discrete
{C : Type u}
[Category.{v, u} C]
{ι : Type u_3}
{F G : Functor (Discrete ι) C}
(α : F ⟶ G)
:
theorem
CategoryTheory.NatTrans.isCartesian_of_isPullback_to_terminal
{J : Type v'}
[Category.{u', v'} J]
{C : Type u}
[Category.{v, u} C]
[Limits.HasTerminal J]
{F G : Functor J C}
(α : F ⟶ G)
(pb : ∀ (j : J), IsPullback (F.map (Limits.terminal.from j)) (α.app j) (α.app (⊤_ J)) (G.map (Limits.terminal.from j)))
:
theorem
CategoryTheory.NatTrans.IsCartesian.comp
{J : Type v'}
[Category.{u', v'} J]
{C : Type u}
[Category.{v, u} C]
{F G H : Functor J C}
{α : F ⟶ G}
{β : G ⟶ H}
(hα : IsCartesian α)
(hβ : IsCartesian β)
:
theorem
CategoryTheory.NatTrans.IsCartesian.whiskerRight
{J : Type v'}
[Category.{u', v'} J]
{C : Type u}
[Category.{v, u} C]
{D : Type u_2}
[Category.{u_3, u_2} D]
{F G : Functor J C}
{α : F ⟶ G}
(hα : IsCartesian α)
(H : Functor C D)
[∀ (i j : J) (f : j ⟶ i), Limits.PreservesLimit (Limits.cospan (α.app i) (G.map f)) H]
:
theorem
CategoryTheory.NatTrans.IsCartesian.whiskerLeft
{J : Type v'}
[Category.{u', v'} J]
{C : Type u}
[Category.{v, u} C]
{K : Type u_3}
[Category.{u_4, u_3} K]
{F G : Functor J C}
{α : F ⟶ G}
(hα : IsCartesian α)
(H : Functor K J)
:
IsCartesian (H.whiskerLeft α)
theorem
CategoryTheory.NatTrans.IsCartesian.hcomp
{J : Type v'}
[Category.{u', v'} J]
{C : Type u}
[Category.{v, u} C]
{K : Type u_3}
[Category.{u_4, u_3} K]
{F G : Functor J C}
{M N : Functor C K}
{α : F ⟶ G}
{β : M ⟶ N}
(hα : IsCartesian α)
(hβ : IsCartesian β)
[∀ (i j : J) (f : j ⟶ i), Limits.PreservesLimit (Limits.cospan (α.app i) (G.map f)) M]
:
IsCartesian (α ◫ β)
theorem
CategoryTheory.NatTrans.IsCartesian.vComp
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
{C₇ : Type u₇}
{C₈ : Type u₈}
[Category.{v₇, u₇} C₇]
[Category.{v₈, u₈} C₈]
{L' : Functor C₃ C₇}
{R'' : Functor C₄ C₈}
{B'' : Functor C₇ C₈}
{w : TwoSquare T L R B}
{w' : TwoSquare B L' R'' B''}
[∀ (i j : C₁) (f : j ⟶ i), Limits.PreservesLimit (Limits.cospan (w.app i) ((L.comp B).map f)) R'']
:
IsCartesian w → IsCartesian w' → IsCartesian (w.vComp w')
theorem
CategoryTheory.NatTrans.IsCartesian.hComp
{C₁ : Type u₁}
{C₂ : Type u₂}
{C₃ : Type u₃}
{C₄ : Type u₄}
[Category.{v₁, u₁} C₁]
[Category.{v₂, u₂} C₂]
[Category.{v₃, u₃} C₃]
[Category.{v₄, u₄} C₄]
{T : Functor C₁ C₂}
{L : Functor C₁ C₃}
{R : Functor C₂ C₄}
{B : Functor C₃ C₄}
{C₅ : Type u₅}
{C₆ : Type u₆}
[Category.{v₅, u₅} C₅]
[Category.{v₆, u₆} C₆]
{T' : Functor C₂ C₅}
{R' : Functor C₅ C₆}
{B' : Functor C₄ C₆}
{w : TwoSquare T L R B}
{w' : TwoSquare T' R R' B'}
[∀ (i j : C₁) (f : j ⟶ i), Limits.PreservesLimit (Limits.cospan (w.app i) ((L.comp B).map f)) B']
:
IsCartesian w → IsCartesian w' → IsCartesian (w.hComp w')