Relation between pullback/pushout squares and kernel/cokernel sequences

This file is the bundled counterpart of Algebra.Homology.CommSq. The same results are obtained here for squares sq : Square C where C is an additive category.

@[reducible, inline]

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

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

Equations

• sq.cokernelCofork = CategoryTheory.Limits.CokernelCofork.ofπ (CategoryTheory.Limits.biprod.desc sq.f₂₄ sq.f₃₄) ⋯

noncomputable def CategoryTheory.Square.isPushoutEquivIsColimitCokernelCofork {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (sq : CategoryTheory.Square C) [CategoryTheory.Limits.HasBinaryBiproduct sq.X₂ sq.X₃] : sq.IsPushout ≃ 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

• sq.isPushoutEquivIsColimitCokernelCofork = { toFun := fun (h : sq.IsPushout) => h.isColimit, invFun := ⋯, left_inv := ⋯, right_inv := ⋯ }.trans ⋯.isColimitEquivIsColimitCokernelCofork

noncomputable def CategoryTheory.Square.IsPushout.isColimitCokernelCofork {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {sq : CategoryTheory.Square C} [CategoryTheory.Limits.HasBinaryBiproduct sq.X₂ sq.X₃] (h : sq.IsPushout) : CategoryTheory.Limits.IsColimit sq.cokernelCofork

The colimit cokernel cofork attached to a pushout square.

Equations

• h.isColimitCokernelCofork = ⋯.isColimitEquivIsColimitCokernelCofork h.isColimit

@[reducible, inline]

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

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

Equations

• sq.kernelFork = CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.Limits.biprod.lift sq.f₁₂ sq.f₁₃) ⋯

noncomputable def CategoryTheory.Square.isPullbackEquivIsLimitKernelFork {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] (sq : CategoryTheory.Square C) [CategoryTheory.Limits.HasBinaryBiproduct sq.X₂ sq.X₃] : sq.IsPullback ≃ 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

• sq.isPullbackEquivIsLimitKernelFork = { toFun := fun (h : sq.IsPullback) => h.isLimit, invFun := ⋯, left_inv := ⋯, right_inv := ⋯ }.trans ⋯.isLimitEquivIsLimitKernelFork

noncomputable def CategoryTheory.Square.IsPullback.isLimitKernelFork {C : Type u_1} [CategoryTheory.Category.{u_2, u_1} C] [CategoryTheory.Preadditive C] {sq : CategoryTheory.Square C} [CategoryTheory.Limits.HasBinaryBiproduct sq.X₂ sq.X₃] (h : sq.IsPullback) : CategoryTheory.Limits.IsLimit sq.kernelFork

The limit kernel fork attached to a pullback square.

Equations

• h.isLimitKernelFork = ⋯.isLimitEquivIsLimitKernelFork h.isLimit