The fundamental cycles of the cube pair and of the boundary of the cube

The identity cube upCube (m + 1) of Iᵐ⁺¹ sends the boundary of the cube into ∂Iᵐ⁺¹, so it is a relative cycle of the normalized cubical chains of the cube pair (Iᵐ⁺¹, ∂Iᵐ⁺¹) (TauCeti.cubeBoundaryPairCycle). A singular cube c of a pair P sending the boundary of the cube into the subspace is a map of pairs c : (Iᵐ⁺¹, ∂Iᵐ⁺¹) ⟶ P (TauCeti.cubeBoundaryPairHom), and it sends the class of this fundamental cycle to the class of c in relative cubical homology (TauCeti.homologyMap_cubeBoundaryPairHom_cubeBoundaryPairCycle).

The class of the fundamental cycle is a generator in every dimension m + 1 ≥ 1 and over every commutative ring k: a ↦ a • [Iᵐ⁺¹] is an isomorphism from k onto the relative cubical homology Hₘ₊₁(Iᵐ⁺¹, ∂Iᵐ⁺¹; k) of the cube pair (TauCeti.cubicalHomologyCubeBoundaryPairEquiv), for instance over 𝔽₂ as well as over ℤ. With integer coefficients, read in relative singular homology, it is ± the generator TauCeti.singularHomologyCubeBoundaryPairIso of Hₘ₊₁(Iᵐ⁺¹, ∂Iᵐ⁺¹; ℤ) ≅ ℤ (TauCeti.exists_singularCubicalHomologyIso_inv_homologyπ_cubeBoundaryPairCycle_eq_units_smul). In dimension one, over every ring k, it is exactly the singular generator of H₁(I¹, ∂I¹; k) (TauCeti.singularCubicalHomologyIso_inv_homologyπ_cubeBoundaryPairCycle_zero), so a ↦ a • [I¹] is an isomorphism from k onto the relative cubical homology of (I¹, ∂I¹) even when k is not commutative (TauCeti.cubicalHomologyCubeBoundaryPairOneEquiv). This is what makes the identity cube a fundamental chain of the cube relative to its boundary, for every choice of coefficients.

The boundary of the identity cube, the signed sum of the faces of Iᵐ⁺¹, is a cycle of ∂Iᵐ⁺¹ (TauCeti.cubeBoundaryCycle), and the connecting morphism of the pair sends [Iᵐ⁺¹] to its class (TauCeti.cubicalHomologyδ_homologyπ_cubeBoundaryPairCycle). Since the cube is contractible, the connecting morphism Hₙ₊₂(Iⁿ⁺², ∂Iⁿ⁺²) ⟶ Hₙ₊₁(∂Iⁿ⁺²) is an isomorphism, so over every commutative ring k the class of this cycle generates Hₙ₊₁(∂Iⁿ⁺²; k) ≅ k (TauCeti.cubicalHomologyCubeBoundaryEquiv): the boundary of the fundamental chain of the cube is a fundamental cycle of its boundary, the sphere ∂Iⁿ⁺².

In dimension n + 2 ≥ 2 the proof compares both classes in the homology of the sphere Sⁿ⁺² = Iⁿ⁺²/∂Iⁿ⁺². The collapse TauCeti.sphereGenLoop (n + 2) : (Iⁿ⁺², ∂Iⁿ⁺²) → (Sⁿ⁺², N) sends the singular generator to the Hurewicz class of the tautological loop, which generates Hₙ₊₂(Sⁿ⁺²; ℤ) (TauCeti.isIso_hurewicz_sphereGenLoop), so it induces an isomorphism on relative singular homology. It sends the fundamental cycle to the relative class of the tautological loop, which is the cubical Hurewicz class of that loop (GenLoop.homologyMap_π_cubicalHurewicz). The two Hurewicz maps differ by a universal sign (HomotopyGroup.exists_hurewicz_eq_units_smul_cubicalHurewicz), and the comparison isomorphisms of absolute and relative homology are compatible (TopPair.homologyMap_π_comp_singularCubicalHomologyIso_inv).

In dimension n + 2 and for a commutative ring k, the integral result produces an integral cocycle φ on the relative chains with φ [Iⁿ⁺²] = 1: the relative chains are projective, so over the principal ideal domain ℤ the relative cycles split off them. Reading the values of φ on cubes in k gives a k-valued cocycle taking the value 1 on [Iⁿ⁺²], because the boundary of a cube has integer coefficients. Since Hₙ₊₂(Iⁿ⁺², ∂Iⁿ⁺²; k) ≅ k, a functional to k with value 1 on [Iⁿ⁺²] forces [Iⁿ⁺²] to correspond to a unit of k.

Main declarations

• TauCeti.mapsTo_upCube_boundary: the identity cube sends the boundary of the cube into the subspace of the cube pair.
• TauCeti.cubeBoundaryPairCycle: the fundamental relative cycle of the cube pair.
• TauCeti.homologyMap_cubeBoundaryPairHom_cubeBoundaryPairCycle: c_*[Iᵐ⁺¹] = [c] in relative cubical homology.
• TauCeti.exists_singularCubicalHomologyIso_inv_homologyπ_cubeBoundaryPairCycle_eq_units_smul: the fundamental cycle is ± the singular generator of Hₘ₊₁(Iᵐ⁺¹, ∂Iᵐ⁺¹; ℤ).
• TauCeti.bijective_smul_homologyπ_cubeBoundaryPairCycle, TauCeti.cubicalHomologyCubeBoundaryPairEquiv: the isomorphism k ≃ₗ[k] Hₘ₊₁(Iᵐ⁺¹, ∂Iᵐ⁺¹; k), a ↦ a • [Iᵐ⁺¹], of relative cubical homology over a commutative ring k.
• TauCeti.cubeBoundaryCycle: the fundamental cycle of ∂Iᵐ⁺¹, the boundary of the identity cube.
• TauCeti.cubicalHomologyδ_homologyπ_cubeBoundaryPairCycle: δ[Iᵐ⁺¹] = [∂Iᵐ⁺¹].
• TauCeti.injective_cubicalHomologyδ_cubeBoundaryPair: the connecting morphism Hₘ₊₁(Iᵐ⁺¹, ∂Iᵐ⁺¹) ⟶ Hₘ(∂Iᵐ⁺¹) is injective.
• TauCeti.singularCubicalHomologyIso_inv_homologyπ_cubeBoundaryPairCycle_zero, TauCeti.bijective_smul_homologyπ_cubeBoundaryPairCycle_zero: in dimension one, [I¹] is the singular generator of H₁(I¹, ∂I¹; k) over every ring k.
• TauCeti.cubicalHomologyCubeBoundaryPairOneEquiv: the isomorphism k ≃ₗ[k] H₁(I¹, ∂I¹; k), a ↦ a • [I¹], of relative cubical homology, over every ring k.
• TauCeti.bijective_smul_homologyπ_cubeBoundaryCycle, TauCeti.cubicalHomologyCubeBoundaryEquiv: the isomorphism k ≃ₗ[k] Hₙ₊₁(∂Iⁿ⁺²; k), a ↦ a • [∂Iⁿ⁺²], of cubical homology, for every commutative ring k.

References

• W. S. Massey, Singular Homology Theory, GTM 70, Springer, 1980, Chapters II and VII.
• A. Hatcher, Algebraic Topology, Section 4.2, the Hurewicz map defined by a generator of Hₙ(Dⁿ, ∂Dⁿ), and Section 3.1, the universal coefficient argument behind the transfer of the integral cocycle to k.

theorem TauCeti.mapsTo_upCube_boundary (m : ℕ) : Set.MapsTo (⇑(upCube m)) (Cube.boundary (Fin m)) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom TopPair.map))

The identity cube upCube m sends the boundary of Iᵐ into the subspace ∂Iᵐ of the cube pair.

noncomputable def TauCeti.cubeBoundaryPairCycle (k : Type u) [Ring k] (m : ℕ) : ↑(HomologicalComplex.cycles (TopPair.cubicalChainComplex k (cubeBoundaryPair (m + 1))) (m + 1))

The fundamental relative cycle of the cube pair (Iᵐ⁺¹, ∂Iᵐ⁺¹): the identity cube upCube, as a relative cycle of the normalized cubical chains with coefficients in k.

@[simp]

theorem TauCeti.iCycles_cubeBoundaryPairCycle (k : Type u) [Ring k] (m : ℕ) : (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.iCycles (TopPair.cubicalChainComplex k (cubeBoundaryPair (m + 1))) (m + 1))) (cubeBoundaryPairCycle k m) = TopPair.cubicalChainOfCube k (upCube (m + 1))

The underlying relative chain of the fundamental cycle of the cube pair is the identity cube.

theorem TauCeti.homologyMap_cubeBoundaryPairHom_cubeBoundaryPairCycle (k : Type u) [Ring k] {P : TopPair} {m : ℕ} (c : SingularCube (↑TopPair.fst) (m + 1)) (hc : Set.MapsTo (⇑c) (Cube.boundary (Fin (m + 1))) (Set.range ⇑(CategoryTheory.ConcreteCategory.hom TopPair.map))) : (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyMap (TopPair.cubicalChainComplexMap k (cubeBoundaryPairHom c hc)) (m + 1))) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (TopPair.cubicalChainComplex k (cubeBoundaryPair (m + 1))) (m + 1))) (cubeBoundaryPairCycle k m)) = (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (TopPair.cubicalChainComplex k P) (m + 1))) (TopPair.cubicalCycleOfCube k c hc)

The map of pairs c : (Iᵐ⁺¹, ∂Iᵐ⁺¹) ⟶ P given by a cube c sends the class of the fundamental cycle of the cube pair to the class of c in relative cubical homology.

The fundamental cycle in dimension at least two

Dimension n + 2 over every commutative ring

The boundary of the fundamental cycle

noncomputable def TauCeti.cubeBoundaryCycle (k : Type u) [Ring k] (m : ℕ) : ↑(HomologicalComplex.cycles ((normalizedCubicalChainComplex k).obj TopPair.snd) m)

The fundamental cycle of the boundary of the cube ∂Iᵐ⁺¹: the boundary of the identity cube, the signed sum ∑ᵢ (-1)ⁱ (∂ᵢ⁰ - ∂ᵢ¹) of the faces of Iᵐ⁺¹, as a normalized cubical m-cycle of ∂Iᵐ⁺¹ with coefficients in k.

@[simp]

theorem TauCeti.iCycles_cubeBoundaryCycle (k : Type u) [Ring k] (m : ℕ) : (ModuleCat.Hom.hom (HomologicalComplex.iCycles ((normalizedCubicalChainComplex k).obj TopPair.snd) m)) (cubeBoundaryCycle k m) = TopPair.cubicalBoundaryChainOfCube k (upCube (m + 1)) ⋯

The underlying chain of the fundamental cycle of ∂Iᵐ⁺¹ is the boundary of the identity cube, read in ∂Iᵐ⁺¹.

theorem TauCeti.cubicalHomologyδ_homologyπ_cubeBoundaryPairCycle (k : Type u) [Ring k] (m : ℕ) : (ModuleCat.Hom.hom (TopPair.cubicalHomologyδ k (cubeBoundaryPair (m + 1)) (m + 1) m ⋯)) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (TopPair.cubicalChainComplex k (cubeBoundaryPair (m + 1))) (m + 1))) (cubeBoundaryPairCycle k m)) = (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ ((normalizedCubicalChainComplex k).obj TopPair.snd) m)) (cubeBoundaryCycle k m)

The connecting morphism Hₘ₊₁(Iᵐ⁺¹, ∂Iᵐ⁺¹) ⟶ Hₘ(∂Iᵐ⁺¹) sends the class of the fundamental cycle of the cube pair to the class of the fundamental cycle of the boundary.

theorem TauCeti.injective_cubicalHomologyδ_cubeBoundaryPair (k : Type u) [Ring k] (m : ℕ) : Function.Injective ⇑(ModuleCat.Hom.hom (TopPair.cubicalHomologyδ k (cubeBoundaryPair (m + 1)) (m + 1) m ⋯))

The connecting morphism Hₘ₊₁(Iᵐ⁺¹, ∂Iᵐ⁺¹) ⟶ Hₘ(∂Iᵐ⁺¹) of relative cubical homology is injective, since the cube is contractible.

Dimension one

theorem TauCeti.singularCubicalHomologyIso_inv_homologyπ_cubeBoundaryPairCycle_zero (k : Type u) [Ring k] : (CategoryTheory.ConcreteCategory.hom (TopPair.singularCubicalHomologyIso k (cubeBoundaryPair 1) 1).inv) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (TopPair.cubicalChainComplex k (cubeBoundaryPair 1)) 1)) (cubeBoundaryPairCycle k 0)) = (CategoryTheory.ConcreteCategory.hom (singularHomologyCubeBoundaryPairIso (↧k) 1).inv) 1

In dimension one the fundamental cycle of the cube pair is the singular generator, over every ring k: the class of TauCeti.cubeBoundaryPairCycle k 0 in H₁(I¹, ∂I¹; k), read in relative singular homology, is the generator TauCeti.singularHomologyCubeBoundaryPairIso of H₁(I¹, ∂I¹; k) ≅ k, with no sign. Both classes have boundary [0] - [1] in H₀(∂I¹; k).

theorem TauCeti.bijective_smul_homologyπ_cubeBoundaryPairCycle_zero (k : Type u) [Ring k] : Function.Bijective fun (a : k) => a • (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (TopPair.cubicalChainComplex k (cubeBoundaryPair 1)) 1)) (cubeBoundaryPairCycle k 0)

The fundamental cycle of I¹ generates H₁(I¹, ∂I¹; k), over every ring k: a ↦ a • [I¹] is bijective, where [I¹] is the class of TauCeti.cubeBoundaryPairCycle k 0.

noncomputable def TauCeti.cubicalHomologyCubeBoundaryPairOneEquiv (k : Type u) [Ring k] : k ≃ₗ[k] ↑(HomologicalComplex.homology (TopPair.cubicalChainComplex k (cubeBoundaryPair 1)) 1)

The relative cubical homology of the interval is free on the fundamental cycle: over any ring k, the isomorphism k ≃ₗ[k] H₁(I¹, ∂I¹; k) of relative normalized cubical homology sending a to a • [I¹] (TauCeti.cubicalHomologyCubeBoundaryPairOneEquiv_apply).

@[simp]

theorem TauCeti.cubicalHomologyCubeBoundaryPairOneEquiv_apply (k : Type u) [Ring k] (a : k) : (cubicalHomologyCubeBoundaryPairOneEquiv k) a = a • (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (TopPair.cubicalChainComplex k (cubeBoundaryPair 1)) 1)) (cubeBoundaryPairCycle k 0)

The fundamental cycle in singular homology over the integers

theorem TauCeti.exists_singularCubicalHomologyIso_inv_homologyπ_cubeBoundaryPairCycle_eq_units_smul (m : ℕ) : ∃ (ε : ℤˣ), (CategoryTheory.ConcreteCategory.hom (TopPair.singularCubicalHomologyIso ℤ (cubeBoundaryPair (m + 1)) (m + 1)).inv) ((CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (TopPair.cubicalChainComplex ℤ (cubeBoundaryPair (m + 1))) (m + 1))) (cubeBoundaryPairCycle ℤ m)) = ↑ε • (CategoryTheory.ConcreteCategory.hom (singularHomologyCubeBoundaryPairIso (↧ℤ) (m + 1)).inv) 1

The fundamental cycle of the cube pair is a generator, in singular homology. There is a sign ε such that the class of the fundamental cycle TauCeti.cubeBoundaryPairCycle of (Iᵐ⁺¹, ∂Iᵐ⁺¹), read in relative singular homology, is ε times the generator TauCeti.singularHomologyCubeBoundaryPairIso of Hₘ₊₁(Iᵐ⁺¹, ∂Iᵐ⁺¹; ℤ) ≅ ℤ. In dimension one the sign is 1, over any ring (TauCeti.singularCubicalHomologyIso_inv_homologyπ_cubeBoundaryPairCycle_zero).

The fundamental cycle generates over every commutative ring

theorem TauCeti.bijective_smul_homologyπ_cubeBoundaryPairCycle (k : Type) [CommRing k] (m : ℕ) : Function.Bijective fun (a : k) => a • (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (TopPair.cubicalChainComplex k (cubeBoundaryPair (m + 1))) (m + 1))) (cubeBoundaryPairCycle k m)

The fundamental cycle generates the relative cubical homology of the cube pair, over every commutative ring k and in every dimension m + 1 ≥ 1: a ↦ a • [Iᵐ⁺¹] is bijective onto Hₘ₊₁(Iᵐ⁺¹, ∂Iᵐ⁺¹; k), where [Iᵐ⁺¹] is the class of the fundamental cycle TauCeti.cubeBoundaryPairCycle.

noncomputable def TauCeti.cubicalHomologyCubeBoundaryPairEquiv (k : Type) [CommRing k] (m : ℕ) : k ≃ₗ[k] ↑(HomologicalComplex.homology (TopPair.cubicalChainComplex k (cubeBoundaryPair (m + 1))) (m + 1))

The relative cubical homology of the cube pair is free on the fundamental cycle: the isomorphism k ≃ₗ[k] Hₘ₊₁(Iᵐ⁺¹, ∂Iᵐ⁺¹; k) of relative normalized cubical homology sending a to a • [Iᵐ⁺¹] (TauCeti.cubicalHomologyCubeBoundaryPairEquiv_apply), for every commutative ring k.

@[simp]

theorem TauCeti.cubicalHomologyCubeBoundaryPairEquiv_apply (k : Type) [CommRing k] (m : ℕ) (a : k) : (cubicalHomologyCubeBoundaryPairEquiv k m) a = a • (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ (TopPair.cubicalChainComplex k (cubeBoundaryPair (m + 1))) (m + 1))) (cubeBoundaryPairCycle k m)

The fundamental cycle of the boundary generates

theorem TauCeti.bijective_smul_homologyπ_cubeBoundaryCycle (k : Type) [CommRing k] (n : ℕ) : Function.Bijective fun (a : k) => a • (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ ((normalizedCubicalChainComplex k).obj TopPair.snd) (n + 1))) (cubeBoundaryCycle k (n + 1))

The fundamental cycle of the boundary of the cube generates its homology. Over every commutative ring k, a ↦ a • [∂Iⁿ⁺²] is bijective onto Hₙ₊₁(∂Iⁿ⁺²; k), where [∂Iⁿ⁺²] is the class of TauCeti.cubeBoundaryCycle.

noncomputable def TauCeti.cubicalHomologyCubeBoundaryEquiv (k : Type) [CommRing k] (n : ℕ) : k ≃ₗ[k] ↑(HomologicalComplex.homology ((normalizedCubicalChainComplex k).obj TopPair.snd) (n + 1))

The homology of the boundary of the cube is free on its fundamental cycle: the isomorphism k ≃ₗ[k] Hₙ₊₁(∂Iⁿ⁺²; k) of normalized cubical homology sending a to a • [∂Iⁿ⁺²] (TauCeti.cubicalHomologyCubeBoundaryEquiv_apply), for every commutative ring k.

@[simp]

theorem TauCeti.cubicalHomologyCubeBoundaryEquiv_apply (k : Type) [CommRing k] (n : ℕ) (a : k) : (cubicalHomologyCubeBoundaryEquiv k n) a = a • (CategoryTheory.ConcreteCategory.hom (HomologicalComplex.homologyπ ((normalizedCubicalChainComplex k).obj TopPair.snd) (n + 1))) (cubeBoundaryCycle k (n + 1))