Relation between pullback/pushout squares and kernel/cokernel sequences

Consider a commutative square in a preadditive category:

X₁ ⟶ X₂
|    |
v    v
X₃ ⟶ X₄

In this file, we show that this is a pushout square iff the object X₄ identifies to the cokernel of the difference map X₁ ⟶ X₂ ⊞ X₃ via the obvious map X₂ ⊞ X₃ ⟶ X₄.

Similarly, it is a pullback square iff the object X₁ identifies to the kernel of the difference map X₂ ⊞ X₃ ⟶ X₄ via the obvious map X₁ ⟶ X₂ ⊞ X₃.

@[reducible, inline]

noncomputable abbrev CategoryTheory.CommSq.cokernelCofork {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X₁ X₂ X₃ X₄ : C} [CategoryTheory.Limits.HasBinaryBiproduct X₂ X₃] {f : X₁ ⟶ X₂} {g : X₁ ⟶ X₃} {inl : X₂ ⟶ X₄} {inr : X₃ ⟶ X₄} (sq : CategoryTheory.CommSq f g inl inr) : CategoryTheory.Limits.CokernelCofork (CategoryTheory.Limits.biprod.lift f (-g))

The cokernel cofork attached to a commutative square in a preadditive category.

Equations

• sq.cokernelCofork = CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.Limits.biprod.desc inl inr) ⋯

noncomputable def CategoryTheory.CommSq.isColimitEquivIsColimitCokernelCofork {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X₁ X₂ X₃ X₄ : C} [CategoryTheory.Limits.HasBinaryBiproduct X₂ X₃] {f : X₁ ⟶ X₂} {g : X₁ ⟶ X₃} {inl : X₂ ⟶ X₄} {inr : X₃ ⟶ X₄} (sq : CategoryTheory.CommSq f g inl inr) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk inl inr ⋯) ≃ CategoryTheory.Limits.IsColimit sq.cokernelCofork

A commutative square in a preadditive category is a pushout square iff the corresponding diagram X₁ ⟶ X₂ ⊞ X₃ ⟶ X₄ ⟶ 0 makes X₄ a cokernel.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.IsPushout.isColimitCokernelCofork {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X₁ X₂ X₃ X₄ : C} [CategoryTheory.Limits.HasBinaryBiproduct X₂ X₃] {f : X₁ ⟶ X₂} {g : X₁ ⟶ X₃} {inl : X₂ ⟶ X₄} {inr : X₃ ⟶ X₄} (h : CategoryTheory.IsPushout f g inl inr) : CategoryTheory.Limits.IsColimit ⋯.cokernelCofork

The colimit cokernel cofork attached to a pushout square.

Equations

• h.isColimitCokernelCofork = ⋯.isColimitEquivIsColimitCokernelCofork h.isColimit

@[reducible, inline]

noncomputable abbrev CategoryTheory.CommSq.kernelFork {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X₁ X₂ X₃ X₄ : C} [CategoryTheory.Limits.HasBinaryBiproduct X₂ X₃] {fst : X₁ ⟶ X₂} {snd : X₁ ⟶ X₃} {f : X₂ ⟶ X₄} {g : X₃ ⟶ X₄} (sq : CategoryTheory.CommSq fst snd f g) : CategoryTheory.Limits.KernelFork (CategoryTheory.Limits.biprod.desc f (-g))

The kernel fork attached to a commutative square in a preadditive category.

Equations

• sq.kernelFork = CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.Limits.biprod.lift fst snd) ⋯

noncomputable def CategoryTheory.CommSq.isLimitEquivIsLimitKernelFork {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X₁ X₂ X₃ X₄ : C} [CategoryTheory.Limits.HasBinaryBiproduct X₂ X₃] {fst : X₁ ⟶ X₂} {snd : X₁ ⟶ X₃} {f : X₂ ⟶ X₄} {g : X₃ ⟶ X₄} (sq : CategoryTheory.CommSq fst snd f g) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk fst snd ⋯) ≃ CategoryTheory.Limits.IsLimit sq.kernelFork

A commutative square in a preadditive category is a pullback square iff the corresponding diagram 0 ⟶ X₁ ⟶ X₂ ⊞ X₃ ⟶ X₄ ⟶ 0 makes X₁ a kernel.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.IsPullback.isLimitKernelFork {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {X₁ X₂ X₃ X₄ : C} [CategoryTheory.Limits.HasBinaryBiproduct X₂ X₃] {fst : X₁ ⟶ X₂} {snd : X₁ ⟶ X₃} {f : X₂ ⟶ X₄} {g : X₃ ⟶ X₄} (h : CategoryTheory.IsPullback fst snd f g) : CategoryTheory.Limits.IsLimit ⋯.kernelFork

The limit kernel fork attached to a pullback square.

Equations

• h.isLimitKernelFork = ⋯.isLimitEquivIsLimitKernelFork h.isLimit