The cubical Eilenberg–Zilber theorem and the Künneth theorem for cubical homology #
The cubical cross product TauCeti.cubicalCrossProduct, N(X; k) ⊗ N(Y; k) ⟶ N(X × Y; k), is a
quasi-isomorphism (TauCeti.quasiIso_cubicalCrossProduct). After the comparison with simplicial
chains it is naturally chain homotopic to the tensor product of the two comparison maps followed
by the simplicial cross product (TauCeti.cubicalSingularCrossProductHomotopy), which is a
quasi-isomorphism since the shuffle map is a homotopy equivalence (Eilenberg–Zilber) and the
comparison maps are homotopy equivalences.
The Künneth map of the cubical chain complexes, ⨁_{p + q = n} Hₚ(X; k) ⊗ H_q(Y; k) ⟶ Hₙ(X × Y; k)
with the cubical homology modules, is the algebraic Künneth map followed by the map induced by the
cross product (TauCeti.cubicalHomologyKunneth). The Künneth theorem for it is the algebraic
Künneth theorem for the chain complexes N(X; k) and N(Y; k), transported along the cross
product: when the cycles split off and the homology splits off the cycles, for instance over a
semisimple ring, it is an isomorphism, and over a principal ideal domain the Künneth sequence is
exact. The normalized cubical chains are projective, being a retract of the free module on the
cubes (an instance in Cubical/Normalization.lean).
Main definitions and results #
TauCeti.quasiIso_cubicalCrossProduct: the cubical cross product is a quasi-isomorphism.TauCeti.cubicalHomologyKunneth: the Künneth map of cubical homology.TauCeti.isIso_cubicalHomologyKunneth: the Künneth theorem for cubical homology.TauCeti.cubicalHomologyKunnethShortComplex_shortExact: the Künneth sequence over a principal ideal domain.TauCeti.tensorHom_comp_singularHomologyKunneth: the cubical Künneth map corresponds to the singular Künneth map (TopCat.singularHomologyKunneth) under the comparison isomorphism.
The tensor product of the two comparison maps is a quasi-isomorphism: they are homotopy equivalences, and the tensor product preserves homotopy equivalences.
The cubical cross product followed by the comparison map is a quasi-isomorphism: it is homotopic to the tensor product of the two comparison maps followed by the simplicial cross product.
The cubical Eilenberg–Zilber theorem: the cross product of normalized cubical chains
N(X; k) ⊗ N(Y; k) ⟶ N(X × Y; k) is a quasi-isomorphism.
The Künneth map of cubical homology,
⨁_{p + q = n} Hₚ(X; k) ⊗ H_q(Y; k) ⟶ Hₙ(X × Y; k), with the homology of the normalized cubical
chains: the algebraic Künneth map of the chain complexes N(X; k) and N(Y; k) followed by the
map induced by the cubical cross product.
Instances For
The cubical Künneth map is the algebraic Künneth map of the chain complexes followed by the map induced by the cubical cross product.
The cubical Künneth map restricts to the homology cross product followed by the map induced by the cubical cross product on each summand.
The cubical Künneth map restricts to the homology cross product followed by the map induced by the cubical cross product on each summand.
Naturality of the cubical Künneth map in both spaces.
Naturality of the cubical Künneth map in both spaces.
The cubical cross product induces an isomorphism on homology.
The Künneth theorem for cubical homology: if the cycles of the normalized cubical chain
complexes split off their terms and their homology splits off the cycles, the Künneth map
⨁_{p + q = n} Hₚ(X; k) ⊗ H_q(Y; k) ⟶ Hₙ(X × Y; k) is an isomorphism. This is the Künneth
theorem for the chain complexes N(X; k) and N(Y; k), transported along the cubical
Eilenberg–Zilber quasi-isomorphism.
The Künneth theorem for cubical homology over a semisimple ring, for instance a field:
⨁_{p + q = n} Hₚ(X; k) ⊗ H_q(Y; k) ≅ Hₙ(X × Y; k) for the homology of the normalized cubical
chains.
The Künneth theorem for cubical homology with projective homology: over a principal ideal
domain k, if the cubical homology modules of X and Y are projective, for instance free, the
Künneth map is an isomorphism. The cycles split off the normalized cubical chains, since these
are projective.
The cubical Künneth map is the simplicial one under the comparison: the tensor product of the comparison isomorphisms on homology, followed by the algebraic Künneth map of the singular chain complexes and the map induced by the simplicial cross product, is the cubical Künneth map followed by the comparison isomorphism of the product. Equivalently, the cubical cross product corresponds to the homology cross product of singular homology.
The same statement for the Künneth map of singular homology with coefficients in the ring
(TopCat.singularHomologyKunneth, followed by the unitor k ⊗ k ≅ k).
The map Hₘ₊₁(X × Y; k) ⟶ ⨁_{p + q = m} Tor₁(Hₚ(X; k), H_q(Y; k)) of the cubical Künneth
sequence: the inverse of the isomorphism induced by the cross product followed by the map to Tor₁
of the algebraic Künneth sequence.
Instances For
The map cubicalHomologyToTor is the inverse of the isomorphism induced by the cross product
followed by the map to Tor₁ of the algebraic Künneth sequence.
The map induced by the cross product followed by the cubical map to Tor₁ is the map to
Tor₁ of the algebraic Künneth sequence.
The map induced by the cross product followed by the cubical map to Tor₁ is the map to
Tor₁ of the algebraic Künneth sequence.
The cubical Künneth map followed by the map to Tor₁ vanishes.
The cubical Künneth map followed by the map to Tor₁ vanishes.
The Künneth short complex of cubical homology,
⨁_{p + q = m + 1} Hₚ(X; k) ⊗ H_q(Y; k) ⟶ Hₘ₊₁(X × Y; k) ⟶ ⨁_{p + q = m} Tor₁(Hₚ(X; k), H_q(Y; k)),
formed by the cubical Künneth map and the map to Tor₁ of the algebraic Künneth sequence, through
the isomorphism induced on homology by the cross product.
Instances For
The Künneth short exact sequence for cubical homology over a principal ideal domain:
0 ⟶ ⨁_{p + q = m + 1} Hₚ(X; k) ⊗ H_q(Y; k) ⟶ Hₘ₊₁(X × Y; k)
⟶ ⨁_{p + q = m} Tor₁(Hₚ(X; k), H_q(Y; k)) ⟶ 0
is exact, for the homology of the normalized cubical chains.