Additional API for homological complexes #
This file records additivity of the cycles functor, degreewise recursion for powers of a
complex endomorphism, and the existence of coproducts of complexes, computed degreewise. It also
records the basic properties of the maps
K.toCycles i j : K.X i ⟶ K.cycles j induced by the differentials: they kill the cycles in degree
i, commute with morphisms of complexes, vanish after a morphism from a complex concentrated in
degree i, and are epimorphisms in degrees where the complex is exact; consequently, a morphism of
complexes which is an epimorphism in degree i induces an epimorphism on cycles in degree j when
its target is exact at j (HomologicalComplex.epi_cyclesMap_of_exactAt). In a degree with no
nonzero differential into it, the identification of the homology with the cycles is natural
(HomologicalComplex.isoHomologyπ_inv_naturality). The sequence
Zᵢ ⟶ Kᵢ ⟶ Zⱼ of cycles is exact when j = c.next i
(HomologicalComplex.cyclesShortComplex_exact). For adjacent degrees i and j, the cycles of a
complex exact in degree j fit into a short exact sequence 0 ⟶ Zᵢ ⟶ Kᵢ ⟶ Zⱼ ⟶ 0
(HomologicalComplex.cyclesShortComplex_shortExact, written out as
HomologicalComplex.shortExact_mk_iCycles_toCycles), which stays short exact when its outer terms
are replaced by isomorphic objects
(HomologicalComplex.cyclesShortComplex_shortExact_of_iso), and whose second map Kᵢ ⟶ Zⱼ is an
isomorphism when Zᵢ vanishes (HomologicalComplex.isIso_toCycles_of_isZero_cycles); in
particular K⁰ ⟶ Z¹ is an isomorphism for a cochain complex exact in degrees 0 and 1
(CochainComplex.isIso_toCycles_zero_of_exactAt). A monomorphism of nonnegative cochain
complexes that is an isomorphism on zero cochains induces an isomorphism on zero cohomology
(CochainComplex.isIso_homologyMap_zero_of_mono). Likewise a
monomorphism onto the kernel of the differential Kᵢ ⟶ Kⱼ gives a short exact sequence
0 ⟶ A ⟶ Kᵢ ⟶ Zⱼ ⟶ 0 (HomologicalComplex.shortExact_toCycles). A morphism of complexes
vanishing in some degree induces zero on homology there
(HomologicalComplex.homologyMap_eq_zero_of_f_eq_zero), and two morphisms of complexes agreeing on
the cycles in some degree induce the same map on homology there
(HomologicalComplex.homologyMap_eq_of_iCycles_comp). Constructing the bundled cycle
sequence requires homology only in the two selected degrees.
The exactness results additionally require homology of the cycle sequence itself.
In an abelian category, the map from the opcycles in degree i to the cycles in degree j is an
isomorphism when the complex is exact in both degrees (HomologicalComplex.isIso_opcyclesToCycles).
For chain complexes indexed by the natural numbers, the identification of zero chains with
cycles is natural (ChainComplex.cycles₀Iso_inv_naturality), and so is the passage from zero
chains to zeroth homology (ChainComplex.pOpcycles_comp_isoHomologyι₀_inv_comp_homologyMap).
The isomorphisms homologyIsoSc'
are natural (HomologicalComplex.homologyMap_comp_homologyIsoSc'_hom), and exactness in a degree
is the vanishing of the homology of the short complex sc' there
(HomologicalComplex.exactAt_iff_isZero_homology_sc').
Homology of complexes commutes with an additive functor preserving homology
(CategoryTheory.Functor.mapHomologicalComplexCompHomologyFunctorIso), the complex-level form of
Mathlib's CategoryTheory.ShortComplex.homologyFunctorIso.
Every morphism between acyclic complexes is a quasi-isomorphism
(HomologicalComplex.quasiIso_of_acyclic).
A chain map of complexes in a concrete category with zero morphisms commutes with the differentials, on elements.
Degreewise recursion for the powers of a chain endomorphism.
Homological complexes have the coproducts that the underlying category has. They are computed degreewise.
The maps onto the cycles #
The map from the cycles in degree i to the cycles in degree j induced by the differential
vanishes.
The map from the cycles in degree i to the cycles in degree j induced by the differential
vanishes.
The short complex Zᵢ(K) ⟶ Kᵢ ⟶ Zⱼ(K) cut out of a homological complex. Its
second map is the differential with codomain restricted to the cycles in degree j.
Instances For
The cycle sequence is formed by the inclusion of cycles and the corestricted differential.
The first map of the cycle sequence is the inclusion of cycles, transported along the
object equalities cyclesShortComplex_X₁ and cyclesShortComplex_X₂.
The second map of the cycle sequence is the corestricted differential, transported along the
object equalities cyclesShortComplex_X₂ and cyclesShortComplex_X₃.
The maps onto the cycles induced by the differentials commute with morphisms of complexes.
The maps onto the cycles induced by the differentials commute with morphisms of complexes.
In a degree j with no nonzero differential into it, the identifications
K.isoHomologyπ i j of the homology with the cycles commute with the maps induced by a morphism of
complexes.
In a degree j with no nonzero differential into it, the identifications
K.isoHomologyπ i j of the homology with the cycles commute with the maps induced by a morphism of
complexes.
A morphism from a complex concentrated in degree i vanishes after the differential out of
degree i.
A morphism from a complex concentrated in degree i vanishes after the differential out of
degree i.
A morphism from a complex concentrated in degree i vanishes after the map onto the cycles in
degree j.
A morphism from a complex concentrated in degree i vanishes after the map onto the cycles in
degree j.
The sequence Zᵢ ⟶ Kᵢ ⟶ Zⱼ of the cycles of a complex K is exact when j is the degree
following i: the cycles in degree i are the kernel of the differential.
A morphism killed by the differential Kᵢ ⟶ Kⱼ is killed by its corestriction to the
cycles in degree j.
The corestriction Kᵢ ⟶ Zⱼ of the differential has the same kernel as the differential
Kᵢ ⟶ Kⱼ: if A ⟶ Kᵢ ⟶ Kⱼ is exact, then so is A ⟶ Kᵢ ⟶ Zⱼ.
In a complex exact in degree j, the map onto the cycles in degree j from the preceding
degree is an epimorphism.
A morphism of complexes which is an epimorphism in degree i = c.prev j induces an
epimorphism on the cycles in degree j when its target is exact at j.
The cycle sequence Zᵢ(K) ⟶ Kᵢ ⟶ Zⱼ(K) is short exact when i and j are adjacent
and K is exact in degree j.
HomologicalComplex.cyclesShortComplex_shortExact with the short complex written out as
ShortComplex.mk (K.iCycles i) (K.toCycles i j) _, so that its terms are the cycles and the term
of K themselves.
The map Kᵢ ⟶ Zⱼ(K) onto the cycles is an isomorphism when i and j are adjacent, K is
exact in degree j and the cycles of K in degree i vanish.
The cycle sequence Zᵢ(K) ⟶ Kᵢ ⟶ Zⱼ(K), with its outer terms replaced along isomorphisms
X ≅ Zᵢ(K) and Zⱼ(K) ≅ Y, is short exact when i and j are adjacent and K is exact in
degree j.
A monomorphism A ⟶ Kᵢ onto the kernel of the differential Kᵢ ⟶ Kⱼ fits into a short exact
sequence 0 ⟶ A ⟶ Kᵢ ⟶ Zⱼ ⟶ 0 when i precedes j and K is exact in degree j.
The map K⁰ ⟶ Z¹(K) onto the cycles in degree 1 is an isomorphism when K is exact in
degrees 0 and 1, since the cycles Z⁰(K) ≅ H⁰(K) then vanish.
A monomorphism of nonnegative cochain complexes that is an isomorphism in degree zero induces an isomorphism on zeroth cohomology.
A morphism of complexes that vanishes in degree i induces zero on homology in degree i.
Two morphisms of complexes that agree on the cycles in degree i induce the same map on
homology in degree i.
If a complex is exact in degrees i and j, with c.Rel i j, the map from the opcycles in
degree i to the cycles in degree j is an isomorphism, by the exact sequence
Hⁱ ⟶ opcyclesⁱ ⟶ Zʲ ⟶ Hʲ.
Taking cycles is additive on morphisms of complexes.
The isomorphisms homologyIsoSc' are natural (this is the naturality of Mathlib's
homologyFunctorIso', for complexes which only individually have homology).
The isomorphisms homologyIsoSc' are natural (this is the naturality of Mathlib's
homologyFunctorIso', for complexes which only individually have homology).
A homological complex is exact at j exactly when the homology of its short complex at j,
with explicit neighbouring indices, is zero.
The identification of degree-zero chains with degree-zero cycles is natural.
The identification of degree-zero chains with degree-zero cycles is natural.
The passage from degree-zero chains to degree-zero homology, through the identification of the homology with the opcycles, is natural.
The passage from degree-zero chains to degree-zero homology, through the identification of the homology with the opcycles, is natural.
A morphism transported along equalities of complexes induces the corresponding transport of the homology map.
A morphism between acyclic homological complexes is a quasi-isomorphism.
Homology of homological complexes commutes with a functor preserving homology.