Preservations of pullback/pushout squares #
If a functor F : C ⥤ D preserves suitable cospans (resp. spans),
and sq : Square C is a pullback square (resp. a pushout square)
then so is the squaresq.map F.
The lemma Square.isPullback_iff_map_coyoneda_isPullback also
shows that a square is a pullback square iff it is so after the
application of the functor coyoneda.obj X for all X : Cᵒᵖ.
Similarly, a square is a pushout square iff the opposite
square becomes a pullback square after the application of the
functor yoneda.obj X for all X : C.
theorem
CategoryTheory.Square.IsPullback.map
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
{sq : CategoryTheory.Square C}
(h : sq.IsPullback)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan sq.f₂₄ sq.f₃₄) F]
:
(sq.map F).IsPullback
theorem
CategoryTheory.Square.IsPullback.of_map
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
{sq : CategoryTheory.Square C}
(F : CategoryTheory.Functor C D)
[CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Limits.cospan sq.f₂₄ sq.f₃₄) F]
(h : (sq.map F).IsPullback)
:
sq.IsPullback
theorem
CategoryTheory.Square.IsPullback.map_iff
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
(sq : CategoryTheory.Square C)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan sq.f₂₄ sq.f₃₄) F]
[CategoryTheory.Limits.ReflectsLimit (CategoryTheory.Limits.cospan sq.f₂₄ sq.f₃₄) F]
:
(sq.map F).IsPullback ↔ sq.IsPullback
theorem
CategoryTheory.Square.IsPushout.map
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
{sq : CategoryTheory.Square C}
(h : sq.IsPushout)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span sq.f₁₂ sq.f₁₃) F]
:
(sq.map F).IsPushout
theorem
CategoryTheory.Square.IsPushout.of_map
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
{sq : CategoryTheory.Square C}
(F : CategoryTheory.Functor C D)
[CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Limits.span sq.f₁₂ sq.f₁₃) F]
(h : (sq.map F).IsPushout)
:
sq.IsPushout
theorem
CategoryTheory.Square.IsPushout.map_iff
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{D : Type u'}
[CategoryTheory.Category.{v', u'} D]
(sq : CategoryTheory.Square C)
(F : CategoryTheory.Functor C D)
[CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.span sq.f₁₂ sq.f₁₃) F]
[CategoryTheory.Limits.ReflectsColimit (CategoryTheory.Limits.span sq.f₁₂ sq.f₁₃) F]
:
(sq.map F).IsPushout ↔ sq.IsPushout
theorem
CategoryTheory.Square.isPullback_iff_map_coyoneda_isPullback
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(sq : CategoryTheory.Square C)
:
theorem
CategoryTheory.Square.isPushout_iff_op_map_yoneda_isPullback
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(sq : CategoryTheory.Square C)
:
sq.IsPushout ↔ ∀ (X : C), (sq.op.map (CategoryTheory.yoneda.obj X)).IsPullback
theorem
CategoryTheory.Square.IsPullback.iff_of_equiv
(sq₁ : CategoryTheory.Square (Type v))
(sq₂ : CategoryTheory.Square (Type u))
(e₁ : sq₁.X₁ ≃ sq₂.X₁)
(e₂ : sq₁.X₂ ≃ sq₂.X₂)
(e₃ : sq₁.X₃ ≃ sq₂.X₃)
(e₄ : sq₁.X₄ ≃ sq₂.X₄)
(comm₁₂ : ⇑e₂ ∘ sq₁.f₁₂ = sq₂.f₁₂ ∘ ⇑e₁)
(comm₁₃ : ⇑e₃ ∘ sq₁.f₁₃ = sq₂.f₁₃ ∘ ⇑e₁)
(comm₂₄ : ⇑e₄ ∘ sq₁.f₂₄ = sq₂.f₂₄ ∘ ⇑e₂)
(comm₃₄ : ⇑e₄ ∘ sq₁.f₃₄ = sq₂.f₃₄ ∘ ⇑e₃)
:
sq₁.IsPullback ↔ sq₂.IsPullback
theorem
CategoryTheory.Square.IsPullback.of_equiv
{sq₁ : CategoryTheory.Square (Type v)}
{sq₂ : CategoryTheory.Square (Type u)}
(e₁ : sq₁.X₁ ≃ sq₂.X₁)
(e₂ : sq₁.X₂ ≃ sq₂.X₂)
(e₃ : sq₁.X₃ ≃ sq₂.X₃)
(e₄ : sq₁.X₄ ≃ sq₂.X₄)
(comm₁₂ : ⇑e₂ ∘ sq₁.f₁₂ = sq₂.f₁₂ ∘ ⇑e₁)
(comm₁₃ : ⇑e₃ ∘ sq₁.f₁₃ = sq₂.f₁₃ ∘ ⇑e₁)
(comm₂₄ : ⇑e₄ ∘ sq₁.f₂₄ = sq₂.f₂₄ ∘ ⇑e₂)
(comm₃₄ : ⇑e₄ ∘ sq₁.f₃₄ = sq₂.f₃₄ ∘ ⇑e₃)
(h₁ : sq₁.IsPullback)
:
sq₂.IsPullback