Documentation

Mathlib.Algebra.Homology.ShortComplex.Exact

Exact short complexes #

When S : ShortComplex C, this file defines a structure S.Exact which expresses the exactness of S, i.e. there exists a homology data h : S.HomologyData such that h.left.H is zero. When [S.HasHomology], it is equivalent to the assertion IsZero S.homology.

Almost by construction, this notion of exactness is self dual, see Exact.op and Exact.unop.

structure CategoryTheory.ShortComplex.Exact {C : Type u_1} [Category.{u_3, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) :

The assertion that the short complex S : ShortComplex C is exact.

condition : ∃ (h : S.HomologyData), Limits.IsZero h.left.H
the condition that there exists an homology data whose left.H field is zero

Instances For

theorem CategoryTheory.ShortComplex.Exact.hasHomology {C : Type u_1} [Category.{u_3, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.Exact) :

theorem CategoryTheory.ShortComplex.Exact.hasZeroObject {C : Type u_1} [Category.{u_3, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.Exact) :

Limits.HasZeroObject C

theorem CategoryTheory.ShortComplex.exact_iff_isZero_homology {C : Type u_1} [Category.{u_3, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasHomology] :

S.Exact ↔ Limits.IsZero S.homology

theorem CategoryTheory.ShortComplex.LeftHomologyData.exact_iff {C : Type u_1} [Category.{u_3, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} [S.HasHomology] (h : S.LeftHomologyData) :

S.Exact ↔ Limits.IsZero h.H

theorem CategoryTheory.ShortComplex.RightHomologyData.exact_iff {C : Type u_1} [Category.{u_3, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} [S.HasHomology] (h : S.RightHomologyData) :

S.Exact ↔ Limits.IsZero h.H

theorem CategoryTheory.ShortComplex.exact_iff_isZero_leftHomology {C : Type u_1} [Category.{u_3, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasHomology] :

S.Exact ↔ Limits.IsZero S.leftHomology

theorem CategoryTheory.ShortComplex.exact_iff_isZero_rightHomology {C : Type u_1} [Category.{u_3, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasHomology] :

S.Exact ↔ Limits.IsZero S.rightHomology

theorem CategoryTheory.ShortComplex.HomologyData.exact_iff {C : Type u_1} [Category.{u_3, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.HomologyData) :

S.Exact ↔ Limits.IsZero h.left.H

theorem CategoryTheory.ShortComplex.HomologyData.exact_iff' {C : Type u_1} [Category.{u_3, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.HomologyData) :

S.Exact ↔ Limits.IsZero h.right.H

theorem CategoryTheory.ShortComplex.exact_iff_homology_iso_zero {C : Type u_1} [Category.{u_3, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasHomology] [Limits.HasZeroObject C] :

S.Exact ↔ Nonempty (S.homology ≅ 0)

theorem CategoryTheory.ShortComplex.exact_of_iso {C : Type u_1} [Category.{u_3, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (e : S₁ ≅ S₂) (h : S₁.Exact) :

S₂.Exact

theorem CategoryTheory.ShortComplex.exact_iff_of_iso {C : Type u_1} [Category.{u_3, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (e : S₁ ≅ S₂) :

S₁.Exact ↔ S₂.Exact

theorem CategoryTheory.ShortComplex.exact_and_mono_f_iff_of_iso {C : Type u_1} [Category.{u_3, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (e : S₁ ≅ S₂) :

S₁.Exact ∧ Mono S₁.f ↔ S₂.Exact ∧ Mono S₂.f

theorem CategoryTheory.ShortComplex.exact_and_epi_g_iff_of_iso {C : Type u_1} [Category.{u_3, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (e : S₁ ≅ S₂) :

S₁.Exact ∧ Epi S₁.g ↔ S₂.Exact ∧ Epi S₂.g

theorem CategoryTheory.ShortComplex.exact_of_isZero_X₂ {C : Type u_1} [Category.{u_3, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) (h : Limits.IsZero S.X₂) :

theorem CategoryTheory.ShortComplex.exact_iff_of_epi_of_isIso_of_mono {C : Type u_1} [Category.{u_3, u_1} C] [Limits.HasZeroMorphisms C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) [Epi φ.τ₁] [IsIso φ.τ₂] [Mono φ.τ₃] :

S₁.Exact ↔ S₂.Exact

theorem CategoryTheory.ShortComplex.HomologyData.exact_iff_i_p_zero {C : Type u_1} [Category.{u_3, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.HomologyData) :

S.Exact ↔ CategoryStruct.comp h.left.i h.right.p = 0

theorem CategoryTheory.ShortComplex.exact_iff_i_p_zero {C : Type u_1} [Category.{u_3, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasHomology] (h₁ : S.LeftHomologyData) (h₂ : S.RightHomologyData) :

S.Exact ↔ CategoryStruct.comp h₁.i h₂.p = 0

theorem CategoryTheory.ShortComplex.exact_iff_iCycles_pOpcycles_zero {C : Type u_1} [Category.{u_3, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasHomology] :

S.Exact ↔ CategoryStruct.comp S.iCycles S.pOpcycles = 0

theorem CategoryTheory.ShortComplex.exact_iff_kernel_ι_comp_cokernel_π_zero {C : Type u_1} [Category.{u_3, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) [S.HasHomology] [Limits.HasKernel S.g] [Limits.HasCokernel S.f] :

S.Exact ↔ CategoryStruct.comp (Limits.kernel.ι S.g) (Limits.cokernel.π S.f) = 0

theorem CategoryTheory.ShortComplex.Exact.op {C : Type u_1} [Category.{u_3, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.Exact) :

theorem CategoryTheory.ShortComplex.Exact.unop {C : Type u_1} [Category.{u_3, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex Cᵒᵖ} (h : S.Exact) :

@[simp]

theorem CategoryTheory.ShortComplex.exact_op_iff {C : Type u_1} [Category.{u_3, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex C) :

S.op.Exact ↔ S.Exact

@[simp]

theorem CategoryTheory.ShortComplex.exact_unop_iff {C : Type u_1} [Category.{u_3, u_1} C] [Limits.HasZeroMorphisms C] (S : ShortComplex Cᵒᵖ) :

S.unop.Exact ↔ S.Exact

theorem CategoryTheory.ShortComplex.LeftHomologyData.exact_map_iff {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {S : ShortComplex C} (h : S.LeftHomologyData) (F : Functor C D) [F.PreservesZeroMorphisms] [h.IsPreservedBy F] [(S.map F).HasHomology] :

(S.map F).Exact ↔ Limits.IsZero (F.obj h.H)

theorem CategoryTheory.ShortComplex.RightHomologyData.exact_map_iff {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {S : ShortComplex C} (h : S.RightHomologyData) (F : Functor C D) [F.PreservesZeroMorphisms] [h.IsPreservedBy F] [(S.map F).HasHomology] :

(S.map F).Exact ↔ Limits.IsZero (F.obj h.H)

theorem CategoryTheory.ShortComplex.Exact.map_of_preservesLeftHomologyOf {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {S : ShortComplex C} (h : S.Exact) (F : Functor C D) [F.PreservesZeroMorphisms] [F.PreservesLeftHomologyOf S] [(S.map F).HasHomology] :

(S.map F).Exact

theorem CategoryTheory.ShortComplex.Exact.map_of_preservesRightHomologyOf {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {S : ShortComplex C} (h : S.Exact) (F : Functor C D) [F.PreservesZeroMorphisms] [F.PreservesRightHomologyOf S] [(S.map F).HasHomology] :

(S.map F).Exact

theorem CategoryTheory.ShortComplex.Exact.map {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] {S : ShortComplex C} (h : S.Exact) (F : Functor C D) [F.PreservesZeroMorphisms] [F.PreservesLeftHomologyOf S] [F.PreservesRightHomologyOf S] :

(S.map F).Exact

theorem CategoryTheory.ShortComplex.exact_map_iff_of_faithful {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [Limits.HasZeroMorphisms C] [Limits.HasZeroMorphisms D] (S : ShortComplex C) [S.HasHomology] (F : Functor C D) [F.PreservesZeroMorphisms] [F.PreservesLeftHomologyOf S] [F.PreservesRightHomologyOf S] [F.Faithful] :

(S.map F).Exact ↔ S.Exact

theorem CategoryTheory.ShortComplex.Exact.comp_eq_zero {C : Type u_1} [Category.{u_3, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.Exact) {X Y : C} {a : X ⟶ S.X₂} (ha : CategoryStruct.comp a S.g = 0) {b : S.X₂ ⟶ Y} (hb : CategoryStruct.comp S.f b = 0) :

CategoryStruct.comp a b = 0

theorem CategoryTheory.ShortComplex.Exact.comp_eq_zero_assoc {C : Type u_1} [Category.{u_3, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (h : S.Exact) {X Y : C} {a : X ⟶ S.X₂} (ha : CategoryStruct.comp a S.g = 0) {b : S.X₂ ⟶ Y} (hb : CategoryStruct.comp S.f b = 0) {Z : C} (h✝ : Y ⟶ Z) :

CategoryStruct.comp a (CategoryStruct.comp b h✝) = CategoryStruct.comp 0 h✝

theorem CategoryTheory.ShortComplex.Exact.isZero_of_both_zeros {C : Type u_1} [Category.{u_3, u_1} C] [Limits.HasZeroMorphisms C] {S : ShortComplex C} (ex : S.Exact) (hf : S.f = 0) (hg : S.g = 0) :

Limits.IsZero S.X₂

theorem CategoryTheory.ShortComplex.exact_iff_mono {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] (S : ShortComplex C) [Limits.HasZeroObject C] (hf : S.f = 0) :

S.Exact ↔ Mono S.g

theorem CategoryTheory.ShortComplex.exact_iff_epi {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] (S : ShortComplex C) [Limits.HasZeroObject C] (hg : S.g = 0) :

S.Exact ↔ Epi S.f

theorem CategoryTheory.ShortComplex.Exact.epi_f' {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (hS : S.Exact) (h : S.LeftHomologyData) :

theorem CategoryTheory.ShortComplex.Exact.mono_g' {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (hS : S.Exact) (h : S.RightHomologyData) :

theorem CategoryTheory.ShortComplex.Exact.epi_toCycles {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (hS : S.Exact) [S.HasLeftHomology] :

theorem CategoryTheory.ShortComplex.Exact.mono_fromOpcycles {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (hS : S.Exact) [S.HasRightHomology] :

Mono S.fromOpcycles

theorem CategoryTheory.ShortComplex.LeftHomologyData.exact_iff_epi_f' {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} [S.HasHomology] (h : S.LeftHomologyData) :

S.Exact ↔ Epi h.f'

theorem CategoryTheory.ShortComplex.RightHomologyData.exact_iff_mono_g' {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} [S.HasHomology] (h : S.RightHomologyData) :

S.Exact ↔ Mono h.g'

noncomputable def CategoryTheory.ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (hS : S.Exact) [Limits.HasZeroObject C] (kf : Limits.KernelFork S.g) (hkf : Limits.IsLimit kf) :

S.LeftHomologyData

Given an exact short complex S and a limit kernel fork kf for S.g, this is the left homology data for S with K := kf.pt and H := 0.

Equations

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

Instances For

@[simp]

theorem CategoryTheory.ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork_H {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (hS : S.Exact) [Limits.HasZeroObject C] (kf : Limits.KernelFork S.g) (hkf : Limits.IsLimit kf) :

(hS.leftHomologyDataOfIsLimitKernelFork kf hkf).H = 0

@[simp]

theorem CategoryTheory.ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork_K {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (hS : S.Exact) [Limits.HasZeroObject C] (kf : Limits.KernelFork S.g) (hkf : Limits.IsLimit kf) :

(hS.leftHomologyDataOfIsLimitKernelFork kf hkf).K = kf.pt

@[simp]

theorem CategoryTheory.ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork_π {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (hS : S.Exact) [Limits.HasZeroObject C] (kf : Limits.KernelFork S.g) (hkf : Limits.IsLimit kf) :

(hS.leftHomologyDataOfIsLimitKernelFork kf hkf).π = 0

@[simp]

theorem CategoryTheory.ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork_i {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (hS : S.Exact) [Limits.HasZeroObject C] (kf : Limits.KernelFork S.g) (hkf : Limits.IsLimit kf) :

(hS.leftHomologyDataOfIsLimitKernelFork kf hkf).i = Limits.Fork.ι kf

noncomputable def CategoryTheory.ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (hS : S.Exact) [Limits.HasZeroObject C] (cc : Limits.CokernelCofork S.f) (hcc : Limits.IsColimit cc) :

S.RightHomologyData

Given an exact short complex S and a colimit cokernel cofork cc for S.f, this is the right homology data for S with Q := cc.pt and H := 0.

Equations

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

Instances For

@[simp]

theorem CategoryTheory.ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_ι {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (hS : S.Exact) [Limits.HasZeroObject C] (cc : Limits.CokernelCofork S.f) (hcc : Limits.IsColimit cc) :

(hS.rightHomologyDataOfIsColimitCokernelCofork cc hcc).ι = 0

@[simp]

theorem CategoryTheory.ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_H {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (hS : S.Exact) [Limits.HasZeroObject C] (cc : Limits.CokernelCofork S.f) (hcc : Limits.IsColimit cc) :

(hS.rightHomologyDataOfIsColimitCokernelCofork cc hcc).H = 0

@[simp]

theorem CategoryTheory.ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_p {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (hS : S.Exact) [Limits.HasZeroObject C] (cc : Limits.CokernelCofork S.f) (hcc : Limits.IsColimit cc) :

(hS.rightHomologyDataOfIsColimitCokernelCofork cc hcc).p = Limits.Cofork.π cc

@[simp]

theorem CategoryTheory.ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork_Q {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (hS : S.Exact) [Limits.HasZeroObject C] (cc : Limits.CokernelCofork S.f) (hcc : Limits.IsColimit cc) :

(hS.rightHomologyDataOfIsColimitCokernelCofork cc hcc).Q = cc.pt

theorem CategoryTheory.ShortComplex.exact_iff_epi_toCycles {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] (S : ShortComplex C) [S.HasHomology] :

S.Exact ↔ Epi S.toCycles

theorem CategoryTheory.ShortComplex.exact_iff_mono_fromOpcycles {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] (S : ShortComplex C) [S.HasHomology] :

S.Exact ↔ Mono S.fromOpcycles

theorem CategoryTheory.ShortComplex.exact_iff_epi_kernel_lift {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] (S : ShortComplex C) [S.HasHomology] [Limits.HasKernel S.g] :

S.Exact ↔ Epi (Limits.kernel.lift S.g S.f ⋯)

theorem CategoryTheory.ShortComplex.exact_iff_mono_cokernel_desc {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] (S : ShortComplex C) [S.HasHomology] [Limits.HasCokernel S.f] :

S.Exact ↔ Mono (Limits.cokernel.desc S.f S.g ⋯)

theorem CategoryTheory.ShortComplex.QuasiIso.exact_iff {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) [S₁.HasHomology] [S₂.HasHomology] [QuasiIso φ] :

S₁.Exact ↔ S₂.Exact

theorem CategoryTheory.ShortComplex.exact_of_f_is_kernel {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] (S : ShortComplex C) (hS : Limits.IsLimit (Limits.KernelFork.ofι S.f ⋯)) [S.HasHomology] :

theorem CategoryTheory.ShortComplex.exact_of_g_is_cokernel {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] (S : ShortComplex C) (hS : Limits.IsColimit (Limits.CokernelCofork.ofπ S.g ⋯)) [S.HasHomology] :

theorem CategoryTheory.ShortComplex.Exact.mono_g {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (hS : S.Exact) (hf : S.f = 0) :

theorem CategoryTheory.ShortComplex.Exact.epi_f {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (hS : S.Exact) (hg : S.g = 0) :

theorem CategoryTheory.ShortComplex.Exact.mono_g_iff {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (hS : S.Exact) :

Mono S.g ↔ S.f = 0

theorem CategoryTheory.ShortComplex.Exact.epi_f_iff {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (hS : S.Exact) :

Epi S.f ↔ S.g = 0

theorem CategoryTheory.ShortComplex.Exact.isZero_X₂ {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (hS : S.Exact) (hf : S.f = 0) (hg : S.g = 0) :

Limits.IsZero S.X₂

theorem CategoryTheory.ShortComplex.Exact.isZero_X₂_iff {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (hS : S.Exact) :

Limits.IsZero S.X₂ ↔ S.f = 0 ∧ S.g = 0

structure CategoryTheory.ShortComplex.Splitting {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] (S : ShortComplex C) :

Type u_3

A splitting for a short complex S consists of the data of a retraction r : X₂ ⟶ X₁ of S.f and section s : X₃ ⟶ X₂ of S.g which satisfy r ≫ S.f + S.g ≫ s = 𝟙 _

r : S.X₂ ⟶ S.X₁
a retraction of S.f
s : S.X₃ ⟶ S.X₂
a section of S.g
f_r : CategoryStruct.comp S.f self.r = CategoryStruct.id S.X₁
the condition that r is a retraction of S.f
s_g : CategoryStruct.comp self.s S.g = CategoryStruct.id S.X₃
the condition that s is a section of S.g
id : CategoryStruct.comp self.r S.f + CategoryStruct.comp S.g self.s = CategoryStruct.id S.X₂
the compatibility between the given section and retraction

Instances For

@[simp]

theorem CategoryTheory.ShortComplex.Splitting.s_g_assoc {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (self : S.Splitting) {Z : C} (h : S.X₃ ⟶ Z) :

CategoryStruct.comp self.s (CategoryStruct.comp S.g h) = h

@[simp]

theorem CategoryTheory.ShortComplex.Splitting.f_r_assoc {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (self : S.Splitting) {Z : C} (h : S.X₁ ⟶ Z) :

CategoryStruct.comp S.f (CategoryStruct.comp self.r h) = h

theorem CategoryTheory.ShortComplex.Splitting.r_f {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (s : S.Splitting) :

CategoryStruct.comp s.r S.f = CategoryStruct.id S.X₂ - CategoryStruct.comp S.g s.s

theorem CategoryTheory.ShortComplex.Splitting.r_f_assoc {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (s : S.Splitting) {Z : C} (h : S.X₂ ⟶ Z) :

CategoryStruct.comp s.r (CategoryStruct.comp S.f h) = CategoryStruct.comp (CategoryStruct.id S.X₂ - CategoryStruct.comp S.g s.s) h

theorem CategoryTheory.ShortComplex.Splitting.g_s {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (s : S.Splitting) :

CategoryStruct.comp S.g s.s = CategoryStruct.id S.X₂ - CategoryStruct.comp s.r S.f

theorem CategoryTheory.ShortComplex.Splitting.g_s_assoc {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (s : S.Splitting) {Z : C} (h : S.X₂ ⟶ Z) :

CategoryStruct.comp S.g (CategoryStruct.comp s.s h) = CategoryStruct.comp (CategoryStruct.id S.X₂ - CategoryStruct.comp s.r S.f) h

def CategoryTheory.ShortComplex.Splitting.splitMono_f {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (s : S.Splitting) :

Given a splitting of a short complex S, this shows that S.f is a split monomorphism.

Equations

s.splitMono_f = { retraction := s.r, id := ⋯ }

Instances For

@[simp]

theorem CategoryTheory.ShortComplex.Splitting.splitMono_f_retraction {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (s : S.Splitting) :

s.splitMono_f.retraction = s.r

theorem CategoryTheory.ShortComplex.Splitting.isSplitMono_f {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (s : S.Splitting) :

IsSplitMono S.f

theorem CategoryTheory.ShortComplex.Splitting.mono_f {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (s : S.Splitting) :

def CategoryTheory.ShortComplex.Splitting.splitEpi_g {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (s : S.Splitting) :

Given a splitting of a short complex S, this shows that S.g is a split epimorphism.

Equations

s.splitEpi_g = { section_ := s.s, id := ⋯ }

Instances For

@[simp]

theorem CategoryTheory.ShortComplex.Splitting.splitEpi_g_section_ {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (s : S.Splitting) :

s.splitEpi_g.section_ = s.s

theorem CategoryTheory.ShortComplex.Splitting.isSplitEpi_g {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (s : S.Splitting) :

theorem CategoryTheory.ShortComplex.Splitting.epi_g {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (s : S.Splitting) :

@[simp]

theorem CategoryTheory.ShortComplex.Splitting.s_r {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (s : S.Splitting) :

CategoryStruct.comp s.s s.r = 0

@[simp]

theorem CategoryTheory.ShortComplex.Splitting.s_r_assoc {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (s : S.Splitting) {Z : C} (h : S.X₁ ⟶ Z) :

CategoryStruct.comp s.s (CategoryStruct.comp s.r h) = CategoryStruct.comp 0 h

theorem CategoryTheory.ShortComplex.Splitting.ext_r {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (s s' : S.Splitting) (h : s.r = s'.r) :

s = s'

theorem CategoryTheory.ShortComplex.Splitting.ext_s {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (s s' : S.Splitting) (h : s.s = s'.s) :

s = s'

noncomputable def CategoryTheory.ShortComplex.Splitting.leftHomologyData {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} [Limits.HasZeroObject C] (s : S.Splitting) :

S.LeftHomologyData

The left homology data on a short complex equipped with a splitting.

Equations

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

Instances For

@[simp]

theorem CategoryTheory.ShortComplex.Splitting.leftHomologyData_K {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} [Limits.HasZeroObject C] (s : S.Splitting) :

s.leftHomologyData.K = S.X₁

@[simp]

theorem CategoryTheory.ShortComplex.Splitting.leftHomologyData_i {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} [Limits.HasZeroObject C] (s : S.Splitting) :

s.leftHomologyData.i = S.f

@[simp]

theorem CategoryTheory.ShortComplex.Splitting.leftHomologyData_π {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} [Limits.HasZeroObject C] (s : S.Splitting) :

s.leftHomologyData.π = 0

@[simp]

theorem CategoryTheory.ShortComplex.Splitting.leftHomologyData_H {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} [Limits.HasZeroObject C] (s : S.Splitting) :

s.leftHomologyData.H = 0

noncomputable def CategoryTheory.ShortComplex.Splitting.rightHomologyData {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} [Limits.HasZeroObject C] (s : S.Splitting) :

S.RightHomologyData

The right homology data on a short complex equipped with a splitting.

Equations

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

Instances For

@[simp]

theorem CategoryTheory.ShortComplex.Splitting.rightHomologyData_H {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} [Limits.HasZeroObject C] (s : S.Splitting) :

s.rightHomologyData.H = 0

@[simp]

theorem CategoryTheory.ShortComplex.Splitting.rightHomologyData_p {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} [Limits.HasZeroObject C] (s : S.Splitting) :

s.rightHomologyData.p = S.g

@[simp]

theorem CategoryTheory.ShortComplex.Splitting.rightHomologyData_ι {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} [Limits.HasZeroObject C] (s : S.Splitting) :

s.rightHomologyData.ι = 0

@[simp]

theorem CategoryTheory.ShortComplex.Splitting.rightHomologyData_Q {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} [Limits.HasZeroObject C] (s : S.Splitting) :

s.rightHomologyData.Q = S.X₃

noncomputable def CategoryTheory.ShortComplex.Splitting.homologyData {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} [Limits.HasZeroObject C] (s : S.Splitting) :

The homology data on a short complex equipped with a splitting.

Equations

s.homologyData = { left := s.leftHomologyData, right := s.rightHomologyData, iso := CategoryTheory.Iso.refl 0, comm := ⋯ }

Instances For

@[simp]

theorem CategoryTheory.ShortComplex.Splitting.homologyData_right {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} [Limits.HasZeroObject C] (s : S.Splitting) :

s.homologyData.right = s.rightHomologyData

@[simp]

theorem CategoryTheory.ShortComplex.Splitting.homologyData_iso {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} [Limits.HasZeroObject C] (s : S.Splitting) :

s.homologyData.iso = Iso.refl 0

@[simp]

theorem CategoryTheory.ShortComplex.Splitting.homologyData_left {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} [Limits.HasZeroObject C] (s : S.Splitting) :

s.homologyData.left = s.leftHomologyData

theorem CategoryTheory.ShortComplex.Splitting.exact {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} [Limits.HasZeroObject C] (s : S.Splitting) :

A short complex equipped with a splitting is exact.

noncomputable def CategoryTheory.ShortComplex.Splitting.fIsKernel {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} [Limits.HasZeroObject C] (s : S.Splitting) :

Limits.IsLimit (Limits.KernelFork.ofι S.f ⋯)

If a short complex S is equipped with a splitting, then S.X₁ is the kernel of S.g.

Equations

s.fIsKernel = s.homologyData.left.hi

Instances For

noncomputable def CategoryTheory.ShortComplex.Splitting.gIsCokernel {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} [Limits.HasZeroObject C] (s : S.Splitting) :

Limits.IsColimit (Limits.CokernelCofork.ofπ S.g ⋯)

If a short complex S is equipped with a splitting, then S.X₃ is the cokernel of S.f.

Equations

s.gIsCokernel = s.homologyData.right.hp

Instances For

def CategoryTheory.ShortComplex.Splitting.map {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [Preadditive C] [Preadditive D] {S : ShortComplex C} (s : S.Splitting) (F : Functor C D) [F.Additive] :

(S.map F).Splitting

If a short complex S has a splitting and F is an additive functor, then S.map F also has a splitting.

Equations

s.map F = { r := F.map s.r, s := F.map s.s, f_r := ⋯, s_g := ⋯, id := ⋯ }

Instances For

@[simp]

theorem CategoryTheory.ShortComplex.Splitting.map_s {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [Preadditive C] [Preadditive D] {S : ShortComplex C} (s : S.Splitting) (F : Functor C D) [F.Additive] :

(s.map F).s = F.map s.s

@[simp]

theorem CategoryTheory.ShortComplex.Splitting.map_r {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [Preadditive C] [Preadditive D] {S : ShortComplex C} (s : S.Splitting) (F : Functor C D) [F.Additive] :

(s.map F).r = F.map s.r

def CategoryTheory.ShortComplex.Splitting.ofIso {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} (s : S₁.Splitting) (e : S₁ ≅ S₂) :

A splitting on a short complex induces splittings on isomorphic short complexes.

Equations

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

Instances For

@[simp]

theorem CategoryTheory.ShortComplex.Splitting.ofIso_s {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} (s : S₁.Splitting) (e : S₁ ≅ S₂) :

(s.ofIso e).s = CategoryStruct.comp e.inv.τ₃ (CategoryStruct.comp s.s e.hom.τ₂)

@[simp]

theorem CategoryTheory.ShortComplex.Splitting.ofIso_r {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S₁ S₂ : ShortComplex C} (s : S₁.Splitting) (e : S₁ ≅ S₂) :

(s.ofIso e).r = CategoryStruct.comp e.inv.τ₂ (CategoryStruct.comp s.r e.hom.τ₁)

noncomputable def CategoryTheory.ShortComplex.Splitting.ofHasBinaryBiproduct {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] (X₁ X₂ : C) [Limits.HasBinaryBiproduct X₁ X₂] :

{ X₁ := X₁, X₂ := X₁ ⊞ X₂, X₃ := X₂, f := Limits.biprod.inl, g := Limits.biprod.snd, zero := ⋯ }.Splitting

The obvious splitting of the short complex X₁ ⟶ X₁ ⊞ X₂ ⟶ X₂.

Equations

CategoryTheory.ShortComplex.Splitting.ofHasBinaryBiproduct X₁ X₂ = { r := CategoryTheory.Limits.biprod.fst, s := CategoryTheory.Limits.biprod.inr, f_r := ⋯, s_g := ⋯, id := ⋯ }

Instances For

noncomputable def CategoryTheory.ShortComplex.Splitting.ofIsZeroOfIsIso {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] (S : ShortComplex C) (hf : Limits.IsZero S.X₁) (hg : IsIso S.g) :

The obvious splitting of a short complex when S.X₁ is zero and S.g is an isomorphism.

Equations

CategoryTheory.ShortComplex.Splitting.ofIsZeroOfIsIso S hf hg = { r := 0, s := CategoryTheory.inv S.g, f_r := ⋯, s_g := ⋯, id := ⋯ }

Instances For

noncomputable def CategoryTheory.ShortComplex.Splitting.ofIsIsoOfIsZero {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] (S : ShortComplex C) (hf : IsIso S.f) (hg : Limits.IsZero S.X₃) :

The obvious splitting of a short complex when S.f is an isomorphism and S.X₃ is zero.

Equations

CategoryTheory.ShortComplex.Splitting.ofIsIsoOfIsZero S hf hg = { r := CategoryTheory.inv S.f, s := 0, f_r := ⋯, s_g := ⋯, id := ⋯ }

Instances For

def CategoryTheory.ShortComplex.Splitting.op {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (h : S.Splitting) :

The splitting of the short complex S.op deduced from a splitting of S.

Equations

h.op = { r := h.s.op, s := h.r.op, f_r := ⋯, s_g := ⋯, id := ⋯ }

Instances For

@[simp]

theorem CategoryTheory.ShortComplex.Splitting.op_s {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (h : S.Splitting) :

h.op.s = h.r.op

@[simp]

theorem CategoryTheory.ShortComplex.Splitting.op_r {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (h : S.Splitting) :

h.op.r = h.s.op

def CategoryTheory.ShortComplex.Splitting.unop {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex Cᵒᵖ} (h : S.Splitting) :

S.unop.Splitting

The splitting of the short complex S.unop deduced from a splitting of S.

Equations

h.unop = { r := h.s.unop, s := h.r.unop, f_r := ⋯, s_g := ⋯, id := ⋯ }

Instances For

@[simp]

theorem CategoryTheory.ShortComplex.Splitting.unop_s {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex Cᵒᵖ} (h : S.Splitting) :

h.unop.s = h.r.unop

@[simp]

theorem CategoryTheory.ShortComplex.Splitting.unop_r {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex Cᵒᵖ} (h : S.Splitting) :

h.unop.r = h.s.unop

noncomputable def CategoryTheory.ShortComplex.Splitting.isoBinaryBiproduct {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (h : S.Splitting) [Limits.HasBinaryBiproduct S.X₁ S.X₃] :

S.X₂ ≅ S.X₁ ⊞ S.X₃

The isomorphism S.X₂ ≅ S.X₁ ⊞ S.X₃ induced by a splitting of the short complex S.

Equations

h.isoBinaryBiproduct = { hom := CategoryTheory.Limits.biprod.lift h.r S.g, inv := CategoryTheory.Limits.biprod.desc S.f h.s, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Instances For

@[simp]

theorem CategoryTheory.ShortComplex.Splitting.isoBinaryBiproduct_inv {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (h : S.Splitting) [Limits.HasBinaryBiproduct S.X₁ S.X₃] :

h.isoBinaryBiproduct.inv = Limits.biprod.desc S.f h.s

@[simp]

theorem CategoryTheory.ShortComplex.Splitting.isoBinaryBiproduct_hom {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} (h : S.Splitting) [Limits.HasBinaryBiproduct S.X₁ S.X₃] :

h.isoBinaryBiproduct.hom = Limits.biprod.lift h.r S.g

theorem CategoryTheory.ShortComplex.Exact.isIso_f' {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} [Balanced C] (hS : S.Exact) (h : S.LeftHomologyData) [Mono S.f] :

theorem CategoryTheory.ShortComplex.Exact.isIso_toCycles {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} [Balanced C] (hS : S.Exact) [Mono S.f] [S.HasLeftHomology] :

IsIso S.toCycles

theorem CategoryTheory.ShortComplex.Exact.isIso_g' {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} [Balanced C] (hS : S.Exact) (h : S.RightHomologyData) [Epi S.g] :

theorem CategoryTheory.ShortComplex.Exact.isIso_fromOpcycles {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} [Balanced C] (hS : S.Exact) [Epi S.g] [S.HasRightHomology] :

IsIso S.fromOpcycles

noncomputable def CategoryTheory.ShortComplex.Exact.fIsKernel {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} [Balanced C] (hS : S.Exact) [Mono S.f] :

Limits.IsLimit (Limits.KernelFork.ofι S.f ⋯)

In a balanced category, if a short complex S is exact and S.f is a mono, then S.X₁ is the kernel of S.g.

Equations

hS.fIsKernel = S.cyclesIsKernel.ofIsoLimit (CategoryTheory.Limits.Fork.ext (CategoryTheory.asIso S.toCycles).symm ⋯)

Instances For

theorem CategoryTheory.ShortComplex.Exact.map_of_mono_of_preservesKernel {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [Preadditive C] [Preadditive D] {S : ShortComplex C} [Balanced C] (hS : S.Exact) (F : Functor C D) [F.PreservesZeroMorphisms] [(S.map F).HasHomology] :

Mono S.f → Limits.PreservesLimit (Limits.parallelPair S.g 0) F → (S.map F).Exact

noncomputable def CategoryTheory.ShortComplex.Exact.gIsCokernel {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} [Balanced C] (hS : S.Exact) [Epi S.g] :

Limits.IsColimit (Limits.CokernelCofork.ofπ S.g ⋯)

In a balanced category, if a short complex S is exact and S.g is an epi, then S.X₃ is the cokernel of S.g.

Equations

hS.gIsCokernel = S.opcyclesIsCokernel.ofIsoColimit (CategoryTheory.Limits.Cofork.ext (CategoryTheory.asIso S.fromOpcycles) ⋯)

Instances For

theorem CategoryTheory.ShortComplex.Exact.map_of_epi_of_preservesCokernel {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] [Preadditive C] [Preadditive D] {S : ShortComplex C} [Balanced C] (hS : S.Exact) (F : Functor C D) [F.PreservesZeroMorphisms] [(S.map F).HasHomology] :

Epi S.g → Limits.PreservesColimit (Limits.parallelPair S.f 0) F → (S.map F).Exact

noncomputable def CategoryTheory.ShortComplex.Exact.lift {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} [Balanced C] (hS : S.Exact) {A : C} (k : A ⟶ S.X₂) (hk : CategoryStruct.comp k S.g = 0) [Mono S.f] :

If a short complex S in a balanced category is exact and such that S.f is a mono, then a morphism k : A ⟶ S.X₂ such that k ≫ S.g = 0 lifts to a morphism A ⟶ S.X₁.

Equations

hS.lift k hk = hS.fIsKernel.lift (CategoryTheory.Limits.KernelFork.ofι k hk)

Instances For

@[simp]

theorem CategoryTheory.ShortComplex.Exact.lift_f {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} [Balanced C] (hS : S.Exact) {A : C} (k : A ⟶ S.X₂) (hk : CategoryStruct.comp k S.g = 0) [Mono S.f] :

CategoryStruct.comp (hS.lift k hk) S.f = k

@[simp]

theorem CategoryTheory.ShortComplex.Exact.lift_f_assoc {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} [Balanced C] (hS : S.Exact) {A : C} (k : A ⟶ S.X₂) (hk : CategoryStruct.comp k S.g = 0) [Mono S.f] {Z : C} (h : S.X₂ ⟶ Z) :

CategoryStruct.comp (hS.lift k hk) (CategoryStruct.comp S.f h) = CategoryStruct.comp k h

theorem CategoryTheory.ShortComplex.Exact.lift' {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} [Balanced C] (hS : S.Exact) {A : C} (k : A ⟶ S.X₂) (hk : CategoryStruct.comp k S.g = 0) [Mono S.f] :

∃ (l : A ⟶ S.X₁), CategoryStruct.comp l S.f = k

noncomputable def CategoryTheory.ShortComplex.Exact.desc {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} [Balanced C] (hS : S.Exact) {A : C} (k : S.X₂ ⟶ A) (hk : CategoryStruct.comp S.f k = 0) [Epi S.g] :

If a short complex S in a balanced category is exact and such that S.g is an epi, then a morphism k : S.X₂ ⟶ A such that S.f ≫ k = 0 descends to a morphism S.X₃ ⟶ A.

Equations

hS.desc k hk = hS.gIsCokernel.desc (CategoryTheory.Limits.CokernelCofork.ofπ k hk)

Instances For

@[simp]

theorem CategoryTheory.ShortComplex.Exact.g_desc {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} [Balanced C] (hS : S.Exact) {A : C} (k : S.X₂ ⟶ A) (hk : CategoryStruct.comp S.f k = 0) [Epi S.g] :

CategoryStruct.comp S.g (hS.desc k hk) = k

@[simp]

theorem CategoryTheory.ShortComplex.Exact.g_desc_assoc {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} [Balanced C] (hS : S.Exact) {A : C} (k : S.X₂ ⟶ A) (hk : CategoryStruct.comp S.f k = 0) [Epi S.g] {Z : C} (h : A ⟶ Z) :

CategoryStruct.comp S.g (CategoryStruct.comp (hS.desc k hk) h) = CategoryStruct.comp k h

theorem CategoryTheory.ShortComplex.Exact.desc' {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] {S : ShortComplex C} [Balanced C] (hS : S.Exact) {A : C} (k : S.X₂ ⟶ A) (hk : CategoryStruct.comp S.f k = 0) [Epi S.g] :

∃ (l : S.X₃ ⟶ A), CategoryStruct.comp S.g l = k

theorem CategoryTheory.ShortComplex.mono_τ₂_of_exact_of_mono {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Balanced C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h₁ : S₁.Exact) [Mono S₁.f] [Mono S₂.f] [Mono φ.τ₁] [Mono φ.τ₃] :

theorem CategoryTheory.ShortComplex.epi_τ₂_of_exact_of_epi {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Balanced C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (h₂ : S₂.Exact) [Epi S₁.g] [Epi S₂.g] [Epi φ.τ₁] [Epi φ.τ₃] :

theorem CategoryTheory.ShortComplex.exact_and_mono_f_iff_f_is_kernel {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] (S : ShortComplex C) [Balanced C] [S.HasHomology] :

S.Exact ∧ Mono S.f ↔ Nonempty (Limits.IsLimit (Limits.KernelFork.ofι S.f ⋯))

theorem CategoryTheory.ShortComplex.exact_and_epi_g_iff_g_is_cokernel {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] (S : ShortComplex C) [Balanced C] [S.HasHomology] :

S.Exact ∧ Epi S.g ↔ Nonempty (Limits.IsColimit (Limits.CokernelCofork.ofπ S.g ⋯))

theorem CategoryTheory.ShortComplex.quasiIso_iff_of_zeros {C : Type u_1} [Category.{u_3, u_1} C] [Abelian C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (hf₁ : S₁.f = 0) (hg₁ : S₁.g = 0) (hf₂ : S₂.f = 0) :

QuasiIso φ ↔ { X₁ := S₁.X₂, X₂ := S₂.X₂, X₃ := S₂.X₃, f := φ.τ₂, g := S₂.g, zero := ⋯ }.Exact ∧ Mono φ.τ₂

Given a morphism of short complexes φ : S₁ ⟶ S₂ in an abelian category, if S₁.f and S₁.g are zero (e.g. when S₁ is of the form 0 ⟶ S₁.X₂ ⟶ 0) and S₂.f = 0 (e.g when S₂ is of the form 0 ⟶ S₂.X₂ ⟶ S₂.X₃), then φ is a quasi-isomorphism iff the obvious short complex S₁.X₂ ⟶ S₂.X₂ ⟶ S₂.X₃ is exact and φ.τ₂ is a mono).

theorem CategoryTheory.ShortComplex.quasiIso_iff_of_zeros' {C : Type u_1} [Category.{u_3, u_1} C] [Abelian C] {S₁ S₂ : ShortComplex C} (φ : S₁ ⟶ S₂) (hg₁ : S₁.g = 0) (hf₂ : S₂.f = 0) (hg₂ : S₂.g = 0) :

QuasiIso φ ↔ { X₁ := S₁.X₁, X₂ := S₁.X₂, X₃ := S₂.X₂, f := S₁.f, g := φ.τ₂, zero := ⋯ }.Exact ∧ Epi φ.τ₂

Given a morphism of short complexes φ : S₁ ⟶ S₂ in an abelian category, if S₁.g = 0 (e.g when S₁ is of the form S₁.X₁ ⟶ S₁.X₂ ⟶ 0) and both S₂.f and S₂.g are zero (e.g when S₂ is of the form 0 ⟶ S₂.X₂ ⟶ 0), then φ is a quasi-isomorphism iff the obvious short complex S₁.X₂ ⟶ S₁.X₂ ⟶ S₂.X₂ is exact and φ.τ₂ is an epi).

noncomputable def CategoryTheory.ShortComplex.Exact.descToInjective {C : Type u_1} [Category.{u_3, u_1} C] [Abelian C] {S : ShortComplex C} (hS : S.Exact) {J : C} (f : S.X₂ ⟶ J) [Injective J] (hf : CategoryStruct.comp S.f f = 0) :

If S is an exact short complex and f : S.X₂ ⟶ J is a morphism to an injective object J such that S.f ≫ f = 0, this is a morphism φ : S.X₃ ⟶ J such that S.g ≫ φ = f.

Equations

hS.descToInjective f hf = CategoryTheory.Injective.factorThru (S.descOpcycles f hf) S.fromOpcycles

Instances For

@[simp]

theorem CategoryTheory.ShortComplex.Exact.comp_descToInjective {C : Type u_1} [Category.{u_3, u_1} C] [Abelian C] {S : ShortComplex C} (hS : S.Exact) {J : C} (f : S.X₂ ⟶ J) [Injective J] (hf : CategoryStruct.comp S.f f = 0) :

CategoryStruct.comp S.g (hS.descToInjective f hf) = f

@[simp]

theorem CategoryTheory.ShortComplex.Exact.comp_descToInjective_assoc {C : Type u_1} [Category.{u_3, u_1} C] [Abelian C] {S : ShortComplex C} (hS : S.Exact) {J : C} (f : S.X₂ ⟶ J) [Injective J] (hf : CategoryStruct.comp S.f f = 0) {Z : C} (h : J ⟶ Z) :

CategoryStruct.comp S.g (CategoryStruct.comp (hS.descToInjective f hf) h) = CategoryStruct.comp f h

noncomputable def CategoryTheory.ShortComplex.Exact.liftFromProjective {C : Type u_1} [Category.{u_3, u_1} C] [Abelian C] {S : ShortComplex C} (hS : S.Exact) {P : C} (f : P ⟶ S.X₂) [Projective P] (hf : CategoryStruct.comp f S.g = 0) :

If S is an exact short complex and f : P ⟶ S.X₂ is a morphism from a projective object P such that f ≫ S.g = 0, this is a morphism φ : P ⟶ S.X₁ such that φ ≫ S.f = f.

Equations

hS.liftFromProjective f hf = CategoryTheory.Projective.factorThru (S.liftCycles f hf) S.toCycles

Instances For

@[simp]

theorem CategoryTheory.ShortComplex.Exact.liftFromProjective_comp {C : Type u_1} [Category.{u_3, u_1} C] [Abelian C] {S : ShortComplex C} (hS : S.Exact) {P : C} (f : P ⟶ S.X₂) [Projective P] (hf : CategoryStruct.comp f S.g = 0) :

CategoryStruct.comp (hS.liftFromProjective f hf) S.f = f

@[simp]

theorem CategoryTheory.ShortComplex.Exact.liftFromProjective_comp_assoc {C : Type u_1} [Category.{u_3, u_1} C] [Abelian C] {S : ShortComplex C} (hS : S.Exact) {P : C} (f : P ⟶ S.X₂) [Projective P] (hf : CategoryStruct.comp f S.g = 0) {Z : C} (h : S.X₂ ⟶ Z) :

CategoryStruct.comp (hS.liftFromProjective f hf) (CategoryStruct.comp S.f h) = CategoryStruct.comp f h

instance CategoryTheory.Functor.instPreservesMonomorphisms {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (F : Functor C D) [Preadditive C] [Preadditive D] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [F.PreservesZeroMorphisms] [F.PreservesHomology] :

F.PreservesMonomorphisms

instance CategoryTheory.Functor.instPreservesEpimorphisms {C : Type u_1} {D : Type u_2} [Category.{u_3, u_1} C] [Category.{u_4, u_2} D] (F : Functor C D) [Preadditive C] [Preadditive D] [Limits.HasZeroObject C] [Limits.HasZeroObject D] [F.PreservesZeroMorphisms] [F.PreservesHomology] :

F.PreservesEpimorphisms

noncomputable def CategoryTheory.ShortComplex.Splitting.ofExactOfSection {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Balanced C] (S : ShortComplex C) (hS : S.Exact) (s : S.X₃ ⟶ S.X₂) (s_g : CategoryStruct.comp s S.g = CategoryStruct.id S.X₃) (hf : Mono S.f) :

This is the splitting of a short complex S in a balanced category induced by a section of the morphism S.g : S.X₂ ⟶ S.X₃

Equations

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

Instances For

noncomputable def CategoryTheory.ShortComplex.Splitting.ofExactOfRetraction {C : Type u_1} [Category.{u_3, u_1} C] [Preadditive C] [Balanced C] (S : ShortComplex C) (hS : S.Exact) (r : S.X₂ ⟶ S.X₁) (f_r : CategoryStruct.comp S.f r = CategoryStruct.id S.X₁) (hg : Epi S.g) :

This is the splitting of a short complex S in a balanced category induced by a retraction of the morphism S.f : S.X₁ ⟶ S.X₂

Equations

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

Instances For