Documentation

Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square

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₁₃ ⋯

Instances For

@[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₃₄ ⋯

Instances For

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₃₄

Instances For

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₃₄

Instances For

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

Instances For

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

Instances For

theorem CategoryTheory.Square.IsPullback.of_iso {C : Type u} [CategoryTheory.Category.{v, u} C] {sq₁ : CategoryTheory.Square C} {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₁ : CategoryTheory.Square C} {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₁ : CategoryTheory.Square C} {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₁ : CategoryTheory.Square C} {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₃₄