Cycles and homology of homological complexes of modules

For a homological complex K of modules over a ring, the inclusion of the degree-n cycles into K.X n is injective and the class map from the cycles onto the degree-n homology is surjective. These are the elementwise forms of the facts that K.iCycles n is a monomorphism and K.homologyπ n is an epimorphism. Conversely, an element of K.X n killed by the differential is a cycle, HomologicalComplex.moduleCatCyclesMk. This constructor directly returns an element of K.cycles n for modules over a ring in any universe, whereas Mathlib's HomologicalComplex.cyclesMk returns an element of (forget₂ C Ab).obj (K.cycles n).

theorem HomologicalComplex.moduleCat_iCycles_injective {R : Type u_1} [Ring R] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex (ModuleCat R) c) (n : ι) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (K.iCycles n))

The inclusion of the degree-n cycles of a homological complex of modules into its degree-n term is injective.

theorem HomologicalComplex.moduleCat_homologyπ_surjective {R : Type u_1} [Ring R] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex (ModuleCat R) c) (n : ι) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (K.homologyπ n))

The class map from the degree-n cycles of a homological complex of modules onto its degree-n homology is surjective.

noncomputable def HomologicalComplex.moduleCatCyclesMk {R : Type u_1} [Ring R] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex (ModuleCat R) c) {n : ι} (x : ↑(K.X n)) (m : ι) (hm : c.next n = m) (hx : (CategoryTheory.ConcreteCategory.hom (K.d n m)) x = 0) : ↑(K.cycles n)

An element x of K.X n killed by the differential K.d n m out of degree n, as a cycle of degree n.

Equations

• K.moduleCatCyclesMk x m hm hx = (CategoryTheory.ConcreteCategory.hom (K.sc n).moduleCatCyclesIso.inv) ⟨x, ⋯⟩

@[simp]

theorem HomologicalComplex.iCycles_moduleCatCyclesMk {R : Type u_1} [Ring R] {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex (ModuleCat R) c) (n : ι) (x : ↑(K.X n)) (m : ι) (hm : c.next n = m) (hx : (CategoryTheory.ConcreteCategory.hom (K.d n m)) x = 0) : (CategoryTheory.ConcreteCategory.hom (K.iCycles n)) (K.moduleCatCyclesMk x m hm hx) = x

The cycle K.moduleCatCyclesMk x m hm hx has underlying element x.