Commutative squares that are pushout or pullback squares #
In this file, we translate the IsPushout and IsPullback
API for the objects of the category Square C of commutative
squares in a category C. We also obtain lemmas which states
in this language that a pullback of a monomorphism is
a monomorphism (and similarly for pushouts of epimorphisms).
@[reducible, inline]
abbrev
CategoryTheory.Square.pullbackCone
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(sq : CategoryTheory.Square C)
:
CategoryTheory.Limits.PullbackCone sq.f₂₄ sq.f₃₄
The pullback cone attached to a commutative square.
Equations
- sq.pullbackCone = CategoryTheory.Limits.PullbackCone.mk sq.f₁₂ sq.f₁₃ ⋯
@[reducible, inline]
abbrev
CategoryTheory.Square.pushoutCocone
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(sq : CategoryTheory.Square C)
:
CategoryTheory.Limits.PushoutCocone sq.f₁₂ sq.f₁₃
The pushout cocone attached to a commutative square.
Equations
- sq.pushoutCocone = CategoryTheory.Limits.PushoutCocone.mk sq.f₂₄ sq.f₃₄ ⋯
def
CategoryTheory.Square.IsPullback
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(sq : CategoryTheory.Square C)
:
The condition that a commutative square is a pullback square.
Equations
- sq.IsPullback = CategoryTheory.IsPullback sq.f₁₂ sq.f₁₃ sq.f₂₄ sq.f₃₄
def
CategoryTheory.Square.IsPushout
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(sq : CategoryTheory.Square C)
:
The condition that a commutative square is a pushout square.
Equations
- sq.IsPushout = CategoryTheory.IsPushout sq.f₁₂ sq.f₁₃ sq.f₂₄ sq.f₃₄
theorem
CategoryTheory.Square.isPullback_iff
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(sq : CategoryTheory.Square C)
:
sq.IsPullback ↔ Nonempty (CategoryTheory.Limits.IsLimit sq.pullbackCone)
theorem
CategoryTheory.Square.isPushout_iff
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(sq : CategoryTheory.Square C)
:
sq.IsPushout ↔ Nonempty (CategoryTheory.Limits.IsColimit sq.pushoutCocone)
theorem
CategoryTheory.Square.IsPullback.mk
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(sq : CategoryTheory.Square C)
(h : CategoryTheory.Limits.IsLimit sq.pullbackCone)
:
sq.IsPullback
theorem
CategoryTheory.Square.IsPushout.mk
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(sq : CategoryTheory.Square C)
(h : CategoryTheory.Limits.IsColimit sq.pushoutCocone)
:
sq.IsPushout
noncomputable def
CategoryTheory.Square.IsPullback.isLimit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{sq : CategoryTheory.Square C}
(h : sq.IsPullback)
:
CategoryTheory.Limits.IsLimit sq.pullbackCone
If a commutative square sq is a pullback square,
then sq.pullbackCone is limit.
Equations
- h.isLimit = CategoryTheory.IsPullback.isLimit h
noncomputable def
CategoryTheory.Square.IsPushout.isColimit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{sq : CategoryTheory.Square C}
(h : sq.IsPushout)
:
CategoryTheory.Limits.IsColimit sq.pushoutCocone
If a commutative square sq is a pushout square,
then sq.pushoutCocone is colimit.
Equations
- h.isColimit = CategoryTheory.IsPushout.isColimit h
theorem
CategoryTheory.Square.IsPullback.of_iso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{sq₁ sq₂ : CategoryTheory.Square C}
(h : sq₁.IsPullback)
(e : sq₁ ≅ sq₂)
:
sq₂.IsPullback
theorem
CategoryTheory.Square.IsPullback.iff_of_iso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{sq₁ sq₂ : CategoryTheory.Square C}
(e : sq₁ ≅ sq₂)
:
sq₁.IsPullback ↔ sq₂.IsPullback
theorem
CategoryTheory.Square.IsPushout.of_iso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{sq₁ sq₂ : CategoryTheory.Square C}
(h : sq₁.IsPushout)
(e : sq₁ ≅ sq₂)
:
sq₂.IsPushout
theorem
CategoryTheory.Square.IsPushout.iff_of_iso
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{sq₁ sq₂ : CategoryTheory.Square C}
(e : sq₁ ≅ sq₂)
:
sq₁.IsPushout ↔ sq₂.IsPushout
theorem
CategoryTheory.Square.IsPushout.op
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{sq : CategoryTheory.Square C}
(h : sq.IsPushout)
:
sq.op.IsPullback
theorem
CategoryTheory.Square.IsPushout.unop
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{sq : CategoryTheory.Square Cᵒᵖ}
(h : sq.IsPushout)
:
sq.unop.IsPullback
theorem
CategoryTheory.Square.IsPullback.op
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{sq : CategoryTheory.Square C}
(h : sq.IsPullback)
:
sq.op.IsPushout
theorem
CategoryTheory.Square.IsPullback.unop
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{sq : CategoryTheory.Square Cᵒᵖ}
(h : sq.IsPullback)
:
sq.unop.IsPushout
theorem
CategoryTheory.Square.IsPullback.flip
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{sq : CategoryTheory.Square C}
(h : sq.IsPullback)
:
sq.flip.IsPullback
theorem
CategoryTheory.Square.IsPullback.mono_f₁₃
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{sq : CategoryTheory.Square C}
(h : sq.IsPullback)
[CategoryTheory.Mono sq.f₂₄]
:
CategoryTheory.Mono sq.f₁₃
theorem
CategoryTheory.Square.IsPullback.mono_f₁₂
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{sq : CategoryTheory.Square C}
(h : sq.IsPullback)
[CategoryTheory.Mono sq.f₃₄]
:
CategoryTheory.Mono sq.f₁₂
theorem
CategoryTheory.Square.IsPushout.flip
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{sq : CategoryTheory.Square C}
(h : sq.IsPushout)
:
sq.flip.IsPushout
theorem
CategoryTheory.Square.IsPushout.epi_f₂₄
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{sq : CategoryTheory.Square C}
(h : sq.IsPushout)
[CategoryTheory.Epi sq.f₁₃]
:
CategoryTheory.Epi sq.f₂₄
theorem
CategoryTheory.Square.IsPushout.epi_f₃₄
{C : Type u}
[CategoryTheory.Category.{v, u} C]
{sq : CategoryTheory.Square C}
(h : sq.IsPushout)
[CategoryTheory.Epi sq.f₁₂]
:
CategoryTheory.Epi sq.f₃₄