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. Chain maps commute with the differentials and the square of
the differential vanishes, on elements (HomologicalComplex.Hom.comm_apply,
HomologicalComplex.d_comp_d_apply), cycles have zero boundary, on elements
(HomologicalComplex.iCycles_d_apply), and an element killed by the differential to degree
c.next i is killed by every differential out of degree i
(HomologicalComplex.d_apply_eq_zero_of_d_next_apply_eq_zero). 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).
A linear map into K.X n whose values are cycles induces a class map into the homology,
HomologicalComplex.moduleCatHomologyClass; it is surjective when every cycle is a value, its
kernel consists of the elements sent to boundaries, and chain maps act on it compatibly.
Consequently, when K is the union of subcomplexes L i, every homology class of K comes from
some L i (HomologicalComplex.exists_homologyMap_eq_of_injective), and a class of L i that
vanishes in K already vanishes in a larger subcomplex containing every boundary it needs
(HomologicalComplex.exists_homologyMap_eq_zero_of_injective). Two cycles whose difference
is a boundary have the same homology class
(HomologicalComplex.moduleCat_homologyπ_eq_of_iCycles_sub_eq_d); conversely, cycles with the same
class differ by the boundary of an element of degree c.prev n
(HomologicalComplex.moduleCat_homologyπ_eq_iff), and a cycle has zero homology class exactly
when it is a boundary (HomologicalComplex.moduleCat_homologyπ_eq_zero_iff); where no
differential enters, such as in degree zero of a cochain complex, a cycle with zero class is zero
(HomologicalComplex.moduleCat_eq_zero_of_homologyπ_eq_zero).
When the homology is finitely generated, finitely many cycles generate all cycles modulo
boundaries (HomologicalComplex.exists_fin_moduleCat_cycles_generating).
Cycles are elements of the kernel of the outgoing differential
(HomologicalComplex.moduleCatCyclesToKer), that kernel has a homology class map
(HomologicalComplex.moduleCatKerHomologyClass), surjective and compatible with chain maps
(HomologicalComplex.homologyMap_moduleCatKerHomologyClass), and the image of the incoming
differential, the kernel and the homology form an exact sequence
(HomologicalComplex.exact_inclusion_moduleCatKerHomologyClass).
Given concrete cocycle and coboundary submodules identified with the terms of a cochain complex,
HomologicalComplex.moduleCatCohomologyClassOfIso specializes this class map to the cocycles,
with its surjectivity and its kernel described by the coboundaries. When the differential is a
linear map δ under these identifications, the kernels of δ and the coboundaries 0, im δ, …
satisfy the hypotheses of this construction (HomologicalComplex.moduleCat_d_inv_eq_zero_iff,
HomologicalComplex.moduleCat_mem_iff_exists_d_eq_inv). At a degree where the complex
is exact, the image of the incoming differential, the term and the image of the outgoing
differential form a short exact sequence (HomologicalComplex.exact_subtype_rangeRestrict).
A chain map restricts to a map between the images of the differentials
(HomologicalComplex.Hom.boundaryMap), functorially in the chain map
(HomologicalComplex.Hom.boundaryMap_comp), zero on the image of a zero differential
(HomologicalComplex.Hom.boundaryMap_eq_zero), and injective where the chain map is; for a
degreewise short exact sequence of complexes whose third term is exact, these maps form a sequence
exact in the middle (HomologicalComplex.Hom.exact_boundaryMap). A family of chain endomorphisms
that is locally nilpotent on the degree-n term is locally nilpotent on the degree-n homology
(HomologicalComplex.iSup_wordKer_homologyMap_eq_top), since the homology is a quotient of the
cycles, a submodule of the term.
For a short exact sequence 0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0 of complexes of modules, the connecting map
sends the class of a cycle of X₃ with lift x₂ to the class of the cycle of X₁ mapping to
d x₂ (CategoryTheory.ShortComplex.ShortExact.moduleCat_δ_homologyπ). Conversely, if a cycle
z₁ of X₁ represents the image of a class x₃ under the connecting map, then x₃ is
represented by the image of an element x₂ of X₂ whose differential is exactly the image of
z₁ (CategoryTheory.ShortComplex.ShortExact.moduleCat_exists_d_eq_of_δ_eq), and such x₂ is
unique up to boundaries and images of cycles of X₁
(CategoryTheory.ShortComplex.ShortExact.moduleCat_exists_sub_eq_d_add). For the chains of a
pair of spaces, this produces chains relative to a subspace with a prescribed boundary in the
subspace, such as fundamental chains of a manifold with boundary.
Homology maps commute with the class map from cycles, on elements of complexes of modules.
Not @[simp]: it would make the existing simp lemmas
ChainComplex.homologyMap_linearYonedaObjMap_homologyπ_apply and
TopCat.singularCohomologyMap_homologyπ_constSingularCocycle fail simpNF.
A chain map of complexes of modules sends cycles to cycles, on elements.
In a complex of modules the differential of a differential vanishes, on elements.
In a complex of modules a cycle has zero boundary, on elements.
In a complex of modules, an element killed by the differential to degree c.next i is killed
by every differential out of degree i.
At a degree j where a complex of modules is exact, the inclusion of the image of the incoming
differential K.X i ⟶ K.X j and the corestriction of the outgoing differential K.X j ⟶ K.X k to
its image form a short exact sequence.
A chain map of complexes of modules sends the image of the differential K.X i ⟶ K.X j into
the image of the differential L.X i ⟶ L.X j.
Instances For
The map on boundaries induced by a chain map is the restriction of the chain map.
The identity chain map induces the identity on boundaries.
The map on boundaries induced by a composite of chain maps is the composite of the induced maps.
If the differential K.X i ⟶ K.X j vanishes, the map on its image induced by a chain map is
zero.
A chain map that is injective in degree j is injective on the boundaries of degree j.
Let K ⟶ L ⟶ M be chain maps of complexes of modules, let h = c.prev i and
j = c.next i. If the sequence K ⟶ L ⟶ M is exact in degree i, L ⟶ M is
surjective in degree h and M is exact in degree i, then the induced maps on the images of
the differentials K.X i ⟶ K.X j, L.X i ⟶ L.X j and M.X i ⟶ M.X j form a sequence that is
exact in the middle.
The inclusion of the degree-n cycles of a homological complex of modules into its degree-n
term is injective.
The class map from the degree-n cycles of a homological complex of modules onto its
degree-n homology is surjective.
The differential out of degree n of a complex of modules kills every cycle of degree n, on
elements.
The underlying element of the cycle K.toCycles m n y is the image K.d m n y, on
elements of complexes of modules.
A chain map of complexes of modules acts on cycles as it does on the underlying elements.
A degree-n cycle of a homological complex of modules has zero homology class exactly when it
is a boundary, the image of an element of the term of degree c.prev n.
A degree-n cycle of a homological complex of modules with zero homology class vanishes when
no differential enters degree n, for instance in degree zero of an ℕ-indexed cochain complex:
there are no boundaries.
Two degree-n cycles of a complex of modules have the same homology class exactly when the
difference of their underlying elements is a boundary, the image of an element of the term of
degree c.prev 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.
Instances For
The cycle K.moduleCatCyclesMk x m hm hx has underlying element x.
The homology class map of a linear map j into the degree-n term of a complex of modules
whose values are cycles. The source of j need not be a submodule of a module identified with the
term, so subcomplexes are covered.
Instances For
The class of z is the homology class of the cycle j z.
If every degree-n cycle is a value of j, then every homology class is the class of an
element.
The class of z vanishes exactly when j z is a boundary, the image of an element of the
term of degree c.prev n.
A chain map φ sends the class of z to the class of g z when it carries j z to
j' (g z).
In a complex of modules the image of the incoming differential K.d p n is contained in the
kernel of the outgoing differential K.d n m.
A degree-n cycle of a complex of modules, as an element of the kernel of the differential
K.d n m.
Instances For
The element of the kernel of K.d n m given by a cycle y is K.iCycles n y.
The homology class of an element of the kernel of the outgoing differential K.d n m.
Instances For
The kernel class map is the homology class map of the kernel's inclusion into the term.
The homology class of the kernel element given by a cycle y is the class of y.
Every homology class is the class of an element of the kernel of the outgoing differential.
A chain map φ sends the homology class of an element z of the kernel of K.d n m to the
homology class of φ z.
The boundaries, the cycles and the homology in degree n form an exact sequence: the kernel
of the homology class map on the kernel of K.d n m is the image of the incoming differential.
If the differential is δ under the identifications e of the terms, then an element of
V n is killed by δ n exactly when the differential kills its transport into the complex.
If the differential is δ under the identifications e of the terms, and B consists of
0 in degree zero and of the image of δ n in degree n + 1, then B consists exactly of the
elements whose transport into the complex is in the image of the incoming differential.
The linear map sending a cocycle of a cochain complex of modules to its cohomology class, the homology class map of the cocycles transported through the chosen identifications of the terms.
Instances For
The class of a cocycle is the homology class of the cocycle transported into the complex.
The class of a cocycle z is the homology class of any cycle whose underlying element
corresponds to z under the identification of the term.
Every cohomology class of a cochain complex of modules is represented by a cocycle.
A cocycle has zero class exactly when its underlying element is in the image of the incoming differential from the degree preceding it.
The class of a cocycle is zero exactly when its underlying element is a coboundary.
Two cocycles represent the same cohomology class exactly when their difference is a coboundary.
Every degree-n homology class of a complex of modules is the class of an element killed by
the differential out of degree n.
If the degree-n homology of a complex of modules is finitely generated, there are finitely
many cycles v i of degree n such that every cycle of degree n is a linear combination of
them up to a boundary, the image of an element of the term of degree p = c.prev n.
A finite sum of cycles built by moduleCatCyclesMk is the cycle built from the sum.
Two degree-n cycles of a complex of modules whose difference is a boundary have the same
homology class.
Homology classes of a union of subcomplexes. Let φ i : L i ⟶ K be chain maps of
complexes of modules that are injective in degree c.next n, and suppose every element of K.X n
comes from some L i. Then every degree-n homology class of K comes from some L i.
Vanishing of homology classes in a union of subcomplexes. Let φ j : L j ⟶ K be chain maps
of complexes of modules that are injective in degree n, and let ψ j : L i ⟶ L j be chain maps
compatible with them, defined for the indices j satisfying P j. Suppose every element of the
term of degree c.prev n of K comes from some L j with P j. Then a degree-n homology class
of L i that vanishes in K already vanishes in some L j with P j.
A chain map of complexes of modules sends the class of a cycle to the class of its image.
Local nilpotence passes to homology. Let φ be a family of chain endomorphisms of a
complex of modules. If every element of the degree-n term is killed by all sufficiently long
composites of the maps (φ i).f n, then every degree-n homology class is killed by all
sufficiently long composites of the induced maps homologyMap (φ i) n.
The connecting map of a short exact sequence of complexes of modules, on classes. Let z₃
be a cycle of S.X₃ in degree i, x₂ an element of S.X₂ in degree i lifting it, and z₁ a
cycle of S.X₁ in degree j whose image in S.X₂ is the differential of x₂. Then the
connecting map sends the class of z₃ to the class of z₁.
Lifting a class along a prescribed boundary. Let x₃ be a degree-i homology class of
S.X₃ and z₁ a degree-j cycle of S.X₁ whose class is the image of x₃ under the connecting
map. Then some element x₂ of S.X₂ in degree i has differential the image of z₁, and maps
onto a cycle of S.X₃ representing x₃. This is the converse of moduleCat_δ_homologyπ: the
boundary of the lift is prescribed on the nose, not only up to a boundary.
Lifts along a prescribed boundary are unique up to boundaries and cycles of S.X₁. Let
x₂, x₂' be elements of S.X₂ in degree i with the same differential, whose images in S.X₃
are homologous cycles. Then x₂ - x₂' is the sum of a boundary and the image of an element a
of S.X₁ killed by the differential to degree j (so a cycle when c.Rel i j).