Homology and exactness of short complexes of abelian groups

In this file, the homology of a short complex S of abelian groups is identified with the quotient of AddMonoidHom.ker S.g by the image of the morphism S.abToCycles : S.X₁ →+ AddMonoidHom.ker S.g induced by S.f.

The definitions are made in the ShortComplex namespace so as to enable dot notation. The names contain the prefix ab in order to allow similar constructions for other categories like ModuleCat.

Main definitions

• ShortComplex.abHomologyIso identifies the homology of a short complex of abelian groups to an explicit quotient.
• ShortComplex.ab_exact_iff expresses that a short complex of abelian groups S is exact iff any element in the kernel of S.g belongs to the image of S.f.

@[simp]

theorem CategoryTheory.ShortComplex.ab_zero_apply (S : CategoryTheory.ShortComplex Ab) (x : ↑S.X₁) : S.g (S.f x) = 0

@[simp]

theorem CategoryTheory.ShortComplex.abToCycles_apply_coe (S : CategoryTheory.ShortComplex Ab) (x : ↑S.X₁) : ↑((CategoryTheory.ShortComplex.abToCycles S) x) = S.f x

def CategoryTheory.ShortComplex.abToCycles (S : CategoryTheory.ShortComplex Ab) : ↑S.X₁ →+ ↥(AddMonoidHom.ker S.g)

The canonical additive morphism S.X₁ →+ AddMonoidHom.ker S.g induced by S.f.

Equations

• CategoryTheory.ShortComplex.abToCycles S = AddMonoidHom.mk' (fun (x : ↑S.X₁) => { val := S.f x, property := ⋯ }) ⋯

@[simp]

theorem CategoryTheory.ShortComplex.abLeftHomologyData_K (S : CategoryTheory.ShortComplex Ab) : (CategoryTheory.ShortComplex.abLeftHomologyData S).K = AddCommGroupCat.of ↥(AddMonoidHom.ker S.g)

@[simp]

theorem CategoryTheory.ShortComplex.abLeftHomologyData_H (S : CategoryTheory.ShortComplex Ab) : (CategoryTheory.ShortComplex.abLeftHomologyData S).H = AddCommGroupCat.of (↥(AddMonoidHom.ker S.g) ⧸ AddMonoidHom.range (CategoryTheory.ShortComplex.abToCycles S))

@[simp]

theorem CategoryTheory.ShortComplex.abLeftHomologyData_π (S : CategoryTheory.ShortComplex Ab) : (CategoryTheory.ShortComplex.abLeftHomologyData S).π = QuotientAddGroup.mk' (AddMonoidHom.range (CategoryTheory.ShortComplex.abToCycles S))

@[simp]

theorem CategoryTheory.ShortComplex.abLeftHomologyData_i (S : CategoryTheory.ShortComplex Ab) : (CategoryTheory.ShortComplex.abLeftHomologyData S).i = AddSubgroup.subtype (AddMonoidHom.ker S.g)

def CategoryTheory.ShortComplex.abLeftHomologyData (S : CategoryTheory.ShortComplex Ab) : CategoryTheory.ShortComplex.LeftHomologyData S

The explicit left homology data of a short complex of abelian group that is given by a kernel and a quotient given by the AddMonoidHom API.

Equations

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

@[simp]

theorem CategoryTheory.ShortComplex.abLeftHomologyData_f' (S : CategoryTheory.ShortComplex Ab) : CategoryTheory.ShortComplex.LeftHomologyData.f' (CategoryTheory.ShortComplex.abLeftHomologyData S) = CategoryTheory.ShortComplex.abToCycles S

noncomputable def CategoryTheory.ShortComplex.abCyclesIso (S : CategoryTheory.ShortComplex Ab) : CategoryTheory.ShortComplex.cycles S ≅ AddCommGroupCat.of ↥(AddMonoidHom.ker S.g)

Given a short complex S of abelian groups, this is the isomorphism between the abstract S.cycles of the homology API and the more concrete description as AddMonoidHom.ker S.g.

Equations

• CategoryTheory.ShortComplex.abCyclesIso S = CategoryTheory.ShortComplex.LeftHomologyData.cyclesIso (CategoryTheory.ShortComplex.abLeftHomologyData S)

@[simp]

theorem CategoryTheory.ShortComplex.abCyclesIso_inv_apply_iCycles (S : CategoryTheory.ShortComplex Ab) (x : ↥(AddMonoidHom.ker S.g)) : (CategoryTheory.ShortComplex.iCycles S) ((CategoryTheory.ShortComplex.abCyclesIso S).inv x) = ↑x

noncomputable def CategoryTheory.ShortComplex.abHomologyIso (S : CategoryTheory.ShortComplex Ab) : CategoryTheory.ShortComplex.homology S ≅ AddCommGroupCat.of (↥(AddMonoidHom.ker S.g) ⧸ AddMonoidHom.range (CategoryTheory.ShortComplex.abToCycles S))

Given a short complex S of abelian groups, this is the isomorphism between the abstract S.homology of the homology API and the more explicit quotient of AddMonoidHom.ker S.g by the image of S.abToCycles : S.X₁ →+ AddMonoidHom.ker S.g.

Equations

• CategoryTheory.ShortComplex.abHomologyIso S = CategoryTheory.ShortComplex.LeftHomologyData.homologyIso (CategoryTheory.ShortComplex.abLeftHomologyData S)

theorem CategoryTheory.ShortComplex.exact_iff_surjective_abToCycles (S : CategoryTheory.ShortComplex Ab) : CategoryTheory.ShortComplex.Exact S ↔ Function.Surjective ⇑(CategoryTheory.ShortComplex.abToCycles S)

theorem CategoryTheory.ShortComplex.ab_exact_iff (S : CategoryTheory.ShortComplex Ab) : CategoryTheory.ShortComplex.Exact S ↔ ∀ (x₂ : ↑S.X₂), S.g x₂ = 0 → ∃ (x₁ : ↑S.X₁), S.f x₁ = x₂

theorem CategoryTheory.ShortComplex.ab_exact_iff_ker_le_range (S : CategoryTheory.ShortComplex Ab) : CategoryTheory.ShortComplex.Exact S ↔ AddMonoidHom.ker S.g ≤ AddMonoidHom.range S.f

theorem CategoryTheory.ShortComplex.ab_exact_iff_range_eq_ker (S : CategoryTheory.ShortComplex Ab) : CategoryTheory.ShortComplex.Exact S ↔ AddMonoidHom.range S.f = AddMonoidHom.ker S.g

theorem CategoryTheory.ShortComplex.ShortExact.ab_injective_f (S : CategoryTheory.ShortComplex Ab) (hS : CategoryTheory.ShortComplex.ShortExact S) : Function.Injective ⇑S.f

theorem CategoryTheory.ShortComplex.ShortExact.ab_surjective_g (S : CategoryTheory.ShortComplex Ab) (hS : CategoryTheory.ShortComplex.ShortExact S) : Function.Surjective ⇑S.g