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} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) : Prop

• condition : ∃ h, CategoryTheory.Limits.IsZero h.left.H

  the condition that there exists an homology data whose left.H field is zero

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

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

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

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

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

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

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

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

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

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

theorem CategoryTheory.ShortComplex.exact_iff_homology_iso_zero {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] (S : CategoryTheory.ShortComplex C) [CategoryTheory.ShortComplex.HasHomology S] [CategoryTheory.Limits.HasZeroObject C] : CategoryTheory.ShortComplex.Exact S ↔ Nonempty (CategoryTheory.ShortComplex.homology S ≅ 0)

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

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

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

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

theorem CategoryTheory.ShortComplex.HomologyData.exact_iff_i_p_zero {C : Type u_1} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Limits.HasZeroMorphisms C] {S : CategoryTheory.ShortComplex C} (h : CategoryTheory.ShortComplex.HomologyData S) : CategoryTheory.ShortComplex.Exact S ↔ CategoryTheory.CategoryStruct.comp h.left.i h.right.p = 0

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

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

@[simp]

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

@[simp]

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