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} [Category.{u_2, u_1} C] [Preadditive C] {X₁ X₂ X₃ X₄ : C} [Limits.HasBinaryBiproduct X₂ X₃] {f : X₁ ⟶ X₂} {g : X₁ ⟶ X₃} {inl : X₂ ⟶ X₄} {inr : X₃ ⟶ X₄} (sq : CommSq f g inl inr) : Limits.CokernelCofork (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.shortComplex {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X₁ X₂ X₃ X₄ : C} [Limits.HasBinaryBiproduct X₂ X₃] {f : X₁ ⟶ X₂} {g : X₁ ⟶ X₃} {inl : X₂ ⟶ X₄} {inr : X₃ ⟶ X₄} (sq : CommSq f g inl inr) : ShortComplex C

The short complex attached to the cokernel cofork of a commutative square.

Equations

• sq.shortComplex = { X₁ := X₁, X₂ := X₂ ⊞ X₃, X₃ := X₄, f := CategoryTheory.Limits.biprod.lift f (-g), g := CategoryTheory.Limits.biprod.desc inl inr, zero := ⋯ }

@[simp]

theorem CategoryTheory.CommSq.shortComplex_X₃ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X₁ X₂ X₃ X₄ : C} [Limits.HasBinaryBiproduct X₂ X₃] {f : X₁ ⟶ X₂} {g : X₁ ⟶ X₃} {inl : X₂ ⟶ X₄} {inr : X₃ ⟶ X₄} (sq : CommSq f g inl inr) : sq.shortComplex.X₃ = X₄

@[simp]

theorem CategoryTheory.CommSq.shortComplex_g {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X₁ X₂ X₃ X₄ : C} [Limits.HasBinaryBiproduct X₂ X₃] {f : X₁ ⟶ X₂} {g : X₁ ⟶ X₃} {inl : X₂ ⟶ X₄} {inr : X₃ ⟶ X₄} (sq : CommSq f g inl inr) : sq.shortComplex.g = Limits.biprod.desc inl inr

@[simp]

theorem CategoryTheory.CommSq.shortComplex_X₂ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X₁ X₂ X₃ X₄ : C} [Limits.HasBinaryBiproduct X₂ X₃] {f : X₁ ⟶ X₂} {g : X₁ ⟶ X₃} {inl : X₂ ⟶ X₄} {inr : X₃ ⟶ X₄} (sq : CommSq f g inl inr) : sq.shortComplex.X₂ = (X₂ ⊞ X₃)

@[simp]

theorem CategoryTheory.CommSq.shortComplex_X₁ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X₁ X₂ X₃ X₄ : C} [Limits.HasBinaryBiproduct X₂ X₃] {f : X₁ ⟶ X₂} {g : X₁ ⟶ X₃} {inl : X₂ ⟶ X₄} {inr : X₃ ⟶ X₄} (sq : CommSq f g inl inr) : sq.shortComplex.X₁ = X₁

@[simp]

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

noncomputable def CategoryTheory.CommSq.isColimitEquivIsColimitCokernelCofork {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X₁ X₂ X₃ X₄ : C} [Limits.HasBinaryBiproduct X₂ X₃] {f : X₁ ⟶ X₂} {g : X₁ ⟶ X₃} {inl : X₂ ⟶ X₄} {inr : X₃ ⟶ X₄} (sq : CommSq f g inl inr) : Limits.IsColimit (Limits.PushoutCocone.mk inl inr ⋯) ≃ 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} [Category.{u_2, u_1} C] [Preadditive C] {X₁ X₂ X₃ X₄ : C} [Limits.HasBinaryBiproduct X₂ X₃] {f : X₁ ⟶ X₂} {g : X₁ ⟶ X₃} {inl : X₂ ⟶ X₄} {inr : X₃ ⟶ X₄} (h : IsPushout f g inl inr) : Limits.IsColimit ⋯.cokernelCofork

The colimit cokernel cofork attached to a pushout square.

Equations

• h.isColimitCokernelCofork = ⋯.isColimitEquivIsColimitCokernelCofork h.isColimit

theorem CategoryTheory.IsPushout.epi_shortComplex_g {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X₁ X₂ X₃ X₄ : C} [Limits.HasBinaryBiproduct X₂ X₃] {f : X₁ ⟶ X₂} {g : X₁ ⟶ X₃} {inl : X₂ ⟶ X₄} {inr : X₃ ⟶ X₄} (h : IsPushout f g inl inr) : Epi ⋯.shortComplex.g

@[reducible, inline]

noncomputable abbrev CategoryTheory.CommSq.kernelFork {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X₁ X₂ X₃ X₄ : C} [Limits.HasBinaryBiproduct X₂ X₃] {fst : X₁ ⟶ X₂} {snd : X₁ ⟶ X₃} {f : X₂ ⟶ X₄} {g : X₃ ⟶ X₄} (sq : CommSq fst snd f g) : Limits.KernelFork (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.shortComplex' {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X₁ X₂ X₃ X₄ : C} [Limits.HasBinaryBiproduct X₂ X₃] {fst : X₁ ⟶ X₂} {snd : X₁ ⟶ X₃} {f : X₂ ⟶ X₄} {g : X₃ ⟶ X₄} (sq : CommSq fst snd f g) : ShortComplex C

The short complex attached to the kernel fork of a commutative square. (This is similar to CommSq.shortComplex, but with different signs.)

Equations

• sq.shortComplex' = { X₁ := X₁, X₂ := X₂ ⊞ X₃, X₃ := X₄, f := CategoryTheory.Limits.biprod.lift fst snd, g := CategoryTheory.Limits.biprod.desc f (-g), zero := ⋯ }

@[simp]

theorem CategoryTheory.CommSq.shortComplex'_X₃ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X₁ X₂ X₃ X₄ : C} [Limits.HasBinaryBiproduct X₂ X₃] {fst : X₁ ⟶ X₂} {snd : X₁ ⟶ X₃} {f : X₂ ⟶ X₄} {g : X₃ ⟶ X₄} (sq : CommSq fst snd f g) : sq.shortComplex'.X₃ = X₄

@[simp]

theorem CategoryTheory.CommSq.shortComplex'_f {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X₁ X₂ X₃ X₄ : C} [Limits.HasBinaryBiproduct X₂ X₃] {fst : X₁ ⟶ X₂} {snd : X₁ ⟶ X₃} {f : X₂ ⟶ X₄} {g : X₃ ⟶ X₄} (sq : CommSq fst snd f g) : sq.shortComplex'.f = Limits.biprod.lift fst snd

@[simp]

theorem CategoryTheory.CommSq.shortComplex'_X₁ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X₁ X₂ X₃ X₄ : C} [Limits.HasBinaryBiproduct X₂ X₃] {fst : X₁ ⟶ X₂} {snd : X₁ ⟶ X₃} {f : X₂ ⟶ X₄} {g : X₃ ⟶ X₄} (sq : CommSq fst snd f g) : sq.shortComplex'.X₁ = X₁

@[simp]

theorem CategoryTheory.CommSq.shortComplex'_g {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X₁ X₂ X₃ X₄ : C} [Limits.HasBinaryBiproduct X₂ X₃] {fst : X₁ ⟶ X₂} {snd : X₁ ⟶ X₃} {f : X₂ ⟶ X₄} {g : X₃ ⟶ X₄} (sq : CommSq fst snd f g) : sq.shortComplex'.g = Limits.biprod.desc f (-g)

@[simp]

theorem CategoryTheory.CommSq.shortComplex'_X₂ {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X₁ X₂ X₃ X₄ : C} [Limits.HasBinaryBiproduct X₂ X₃] {fst : X₁ ⟶ X₂} {snd : X₁ ⟶ X₃} {f : X₂ ⟶ X₄} {g : X₃ ⟶ X₄} (sq : CommSq fst snd f g) : sq.shortComplex'.X₂ = (X₂ ⊞ X₃)

noncomputable def CategoryTheory.CommSq.isLimitEquivIsLimitKernelFork {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X₁ X₂ X₃ X₄ : C} [Limits.HasBinaryBiproduct X₂ X₃] {fst : X₁ ⟶ X₂} {snd : X₁ ⟶ X₃} {f : X₂ ⟶ X₄} {g : X₃ ⟶ X₄} (sq : CommSq fst snd f g) : Limits.IsLimit (Limits.PullbackCone.mk fst snd ⋯) ≃ 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} [Category.{u_2, u_1} C] [Preadditive C] {X₁ X₂ X₃ X₄ : C} [Limits.HasBinaryBiproduct X₂ X₃] {fst : X₁ ⟶ X₂} {snd : X₁ ⟶ X₃} {f : X₂ ⟶ X₄} {g : X₃ ⟶ X₄} (h : IsPullback fst snd f g) : Limits.IsLimit ⋯.kernelFork

The limit kernel fork attached to a pullback square.

Equations

• h.isLimitKernelFork = ⋯.isLimitEquivIsLimitKernelFork h.isLimit

theorem CategoryTheory.IsPullback.mono_shortComplex'_f {C : Type u_1} [Category.{u_2, u_1} C] [Preadditive C] {X₁ X₂ X₃ X₄ : C} [Limits.HasBinaryBiproduct X₂ X₃] {fst : X₁ ⟶ X₂} {snd : X₁ ⟶ X₃} {f : X₂ ⟶ X₄} {g : X₃ ⟶ X₄} (h : IsPullback fst snd f g) : Mono ⋯.shortComplex'.f