The homology of spheres

For a point p of the unit sphere S of a real normed space, the complements of p and of -p form an open cover of S by two contractible sets whose intersection is S ∖ {p, -p}. The reduced Mayer–Vietoris connecting morphism of this cover is therefore an isomorphism Hₖ₊₁(S) ≅ H_redₖ(S ∖ {p, -p}) in every degree. In a real inner product space, S ∖ {p, -p} is homotopy equivalent to the unit sphere of the orthogonal complement (ℝ ∙ p)ᗮ, and composing gives the isomorphism H_redₖ₊₁(S) ≅ H_redₖ(S ∩ (ℝ ∙ p)ᗮ), lowering both the sphere's dimension and the degree.

Iterating this suspension isomorphism down to the zero-sphere, whose reduced homology is one copy of the coefficient object in degree zero and vanishes above, computes the reduced homology of the unit sphere of an (n + 1)-dimensional real inner product space: it is one copy of the coefficient object in degree n and vanishes in every other degree. Mathlib's TopCat.sphere n is the universe lift of the unit sphere of EuclideanSpace ℝ (Fin (n + 1)); through TauCeti.diskBoundaryHomeomorph it is homeomorphic to the unit sphere of a Euclidean space of the same dimension in the lifted universe, so the same computation applies to it.

For the unit circle S of a two-dimensional real inner product space, the explicit form of the Mayer–Vietoris sequence is recorded directly: the cover is by the two open arcs S ∖ {p} and S ∖ {-p}, whose intersection S ∖ {p, -p} consists of two open arcs, the path components of any of its points x and of -x. The connecting morphism H₁(S) ⟶ H₀(S ∖ {p, -p}) identifies H₁(S) with one copy of the coefficient object and sends the resulting generator to [-x] - [x].

Coefficients are an object R of an abelian category with coproducts.

Main definitions and results

• TauCeti.isZero_reducedSingularHomologyFunctor_sphere_compl_singleton: the unit sphere minus a point is acyclic.
• TauCeti.isIso_reducedMayerVietorisδ_sphere: the reduced Mayer–Vietoris connecting morphism Hₖ₊₁(S) ⟶ H_redₖ(S ∖ {p, -p}) of the cover of S by the complements of p and -p is an isomorphism.
• TauCeti.reducedSingularHomologySphereSuccIso: the isomorphism H_redₖ₊₁(S) ≅ H_redₖ(S ∩ (ℝ ∙ p)ᗮ), given by that connecting morphism followed by the homotopy equivalence of S ∖ {p, -p} with the equator.
• TauCeti.reducedSingularHomologySphereIsoOfFinrankEq: the unit spheres of two finite-dimensional real normed spaces of the same dimension have isomorphic reduced homology, which transports the computations below from inner product spaces to normed spaces.
• TauCeti.reducedSingularHomologySphereZeroIso: H_red₀(S) ≅ R for the zero-sphere, with generator [-p] - [p].
• TauCeti.singularHomologySphereOneIso and TauCeti.singularHomologySphereOneIso_inv_mayerVietorisδ: H₁(S) ≅ R for the circle, whose generator the Mayer–Vietoris connecting morphism of the cover by S ∖ {p} and S ∖ {-p} sends to [-x] - [x] in the zeroth homology of S ∖ {p, -p}.
• TauCeti.isZero_reducedSingularHomologyFunctor_sphere_of_ne and TauCeti.reducedSingularHomologySphereIso: for finrank ℝ E = n + 1, the reduced homology of the unit sphere of E vanishes in degrees k ≠ n and is isomorphic to R in degree n.
• TauCeti.isZero_reducedSingularHomologyFunctor_topCatSphere_of_ne and TauCeti.reducedSingularHomologyTopCatSphereIso: the same for Mathlib's TopCat.sphere n.

References

• A. Hatcher, Algebraic Topology, Section 2.2, Example 2.46: the reduced Mayer–Vietoris sequence of a cover of Sⁿ by two contractible open sets meeting in a space homotopy equivalent to Sⁿ⁻¹, there neighbourhoods of the two hemispheres and here the complements of two antipodal points, and the resulting induction on dimension. The computed groups are those of Section 2.1, Corollary 2.14.

theorem TauCeti.isIso_reducedMayerVietorisδ_sphere {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {E : Type w} [NormedAddCommGroup E] [NormedSpace ℝ E] (p : ↑(Metric.sphere 0 1)) (k : ℕ) : CategoryTheory.IsIso (TopCat.reducedMayerVietorisδ R ⋯ ⋯ ⋯ k)

The Mayer–Vietoris isomorphism of a sphere. The reduced Mayer–Vietoris connecting morphism Hₖ₊₁(S) ⟶ H_redₖ(S ∖ {p, -p}) of the cover of the unit sphere S by the complements of p and -p is an isomorphism in every degree, since both complements are contractible.

theorem TauCeti.isZero_reducedSingularHomologyFunctor_sphere_compl_singleton {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {E : Type w} [NormedAddCommGroup E] [NormedSpace ℝ E] (p : ↑(Metric.sphere 0 1)) (k : ℕ) : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor R k).obj ↧↑{p}ᶜ)

The unit sphere minus a point is acyclic. For a point p of the unit sphere of a real normed space, the reduced homology of the complement of p vanishes in every degree, since that complement is contractible.

noncomputable def TauCeti.reducedSingularHomologySphereZeroIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {E : Type w} [NormedAddCommGroup E] [NormedSpace ℝ E] (h : Module.finrank ℝ E = 1) (p : ↑(Metric.sphere 0 1)) : (reducedSingularHomologyFunctor R 0).obj ↧↑(Metric.sphere 0 1) ≅ R

Reduced homology of the zero-sphere. For a point p of the unit sphere of a one-dimensional real normed space, the reduced homology of the sphere in degree zero is one copy of the coefficient object, generated by the class [-p] - [p] (TauCeti.reducedSingularHomologySphereZeroIso_inv_ι).

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.reducedSingularHomologySphereZeroIso_inv_ι {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {E : Type w} [NormedAddCommGroup E] [NormedSpace ℝ E] (h : Module.finrank ℝ E = 1) (p : ↑(Metric.sphere 0 1)) : CategoryTheory.CategoryStruct.comp (reducedSingularHomologySphereZeroIso R h p).inv ((reducedSingularHomologyι R 0).app ↧↑(Metric.sphere 0 1)) = singularHomology₀Section R (-p) - singularHomology₀Section R p

The generator of the reduced homology of the zero-sphere {p, -p} is the class [-p] - [p].

theorem TauCeti.reducedSingularHomologySphereZeroIso_inv_ι_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {E : Type w} [NormedAddCommGroup E] [NormedSpace ℝ E] (h : Module.finrank ℝ E = 1) (p : ↑(Metric.sphere 0 1)) {Z : C} (h✝ : ((AlgebraicTopology.singularHomologyFunctor C 0).obj R).obj ↧↑(Metric.sphere 0 1) ⟶ Z) : CategoryTheory.CategoryStruct.comp (reducedSingularHomologySphereZeroIso R h p).inv (CategoryTheory.CategoryStruct.comp ((reducedSingularHomologyι R 0).app ↧↑(Metric.sphere 0 1)) h✝) = CategoryTheory.CategoryStruct.comp (singularHomology₀Section R (-p) - singularHomology₀Section R p) h✝

The generator of the reduced homology of the zero-sphere {p, -p} is the class [-p] - [p].

noncomputable def TauCeti.reducedSingularHomologySphereIsoOfFinrankEq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {E : Type w} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {F : Type w} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] (hEF : Module.finrank ℝ E = Module.finrank ℝ F) (k : ℕ) : (reducedSingularHomologyFunctor R k).obj ↧↑(Metric.sphere 0 1) ≅ (reducedSingularHomologyFunctor R k).obj ↧↑(Metric.sphere 0 1)

The unit spheres of two finite-dimensional real normed spaces of the same dimension have isomorphic reduced homology, through the homeomorphism TauCeti.sphereHomeomorphOfFinrankEq. This transports the computations of this file from inner product spaces to normed spaces.

Equations

• TauCeti.reducedSingularHomologySphereIsoOfFinrankEq R hEF k = (TauCeti.reducedSingularHomologyFunctor R k).mapIso (TopCat.isoOfHomeo (TauCeti.sphereHomeomorphOfFinrankEq hEF))

@[simp]

theorem TauCeti.reducedSingularHomologySphereIsoOfFinrankEq_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {E : Type w} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {F : Type w} [NormedAddCommGroup F] [NormedSpace ℝ F] [FiniteDimensional ℝ F] (hEF : Module.finrank ℝ E = Module.finrank ℝ F) (k : ℕ) : (reducedSingularHomologySphereIsoOfFinrankEq R hEF k).hom = (reducedSingularHomologyFunctor R k).map (TopCat.ofHom ↑(sphereHomeomorphOfFinrankEq hEF))

TauCeti.reducedSingularHomologySphereIsoOfFinrankEq is the map induced by TauCeti.sphereHomeomorphOfFinrankEq.

noncomputable def TauCeti.reducedSingularHomologySphereSuccIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {E : Type w} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (p : ↑(Metric.sphere 0 1)) (k : ℕ) : (reducedSingularHomologyFunctor R (k + 1)).obj ↧↑(Metric.sphere 0 1) ≅ (reducedSingularHomologyFunctor R k).obj ↧↑(Metric.sphere 0 1)

The suspension isomorphism for the homology of spheres. For a point p of the unit sphere S of a real inner product space E, the reduced homology of S in degree k + 1 is isomorphic to the reduced homology in degree k of the equator, the unit sphere of (ℝ ∙ p)ᗮ. It is the Mayer–Vietoris connecting morphism of the cover of S by the complements of p and -p, followed by the homotopy equivalence TauCeti.equatorHomotopyEquiv of S ∖ {p, -p} with the equator.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.reducedSingularHomologySphereSuccIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {E : Type w} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (p : ↑(Metric.sphere 0 1)) (k : ℕ) : (reducedSingularHomologySphereSuccIso R p k).hom = CategoryTheory.CategoryStruct.comp ((reducedSingularHomologyι R (k + 1)).app ↧↑(Metric.sphere 0 1)) (CategoryTheory.CategoryStruct.comp (TopCat.reducedMayerVietorisδ R ⋯ ⋯ ⋯ k) ((reducedSingularHomologyFunctor R k).map (TopCat.ofHom (equatorHomotopyEquiv p).toFun)))

The suspension isomorphism is the identification of reduced with ordinary homology in positive degrees, followed by the reduced Mayer–Vietoris connecting morphism of the cover by the complements of p and -p, and by the map induced by radial projection of the orthogonal projection onto (ℝ ∙ p)ᗮ.

noncomputable def TauCeti.singularHomologySphereOneIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {E : Type w} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {p : ↑(Metric.sphere 0 1)} (hE : Module.finrank ℝ E = 2) {x : ↑(Metric.sphere 0 1)} (hx : x ∈ {p}ᶜ ∩ {-p}ᶜ) : (TopCat.toSSet.obj ↧↑(Metric.sphere 0 1)).homology R 1 ≅ R

The first homology of a circle through its Mayer–Vietoris sequence. For a point p of the unit circle S of a two-dimensional real inner product space, the Mayer–Vietoris connecting morphism of the cover of S by the two open arcs S ∖ {p} and S ∖ {-p} identifies H₁(S) with the reduced zeroth homology of their intersection, which consists of two open arcs. For a point x of that intersection, the arcs are the path components of x and of -x, so this reduced homology is one copy of the coefficient object, generated by [-x] - [x]. The connecting morphism therefore sends the generator of H₁(S) determined by this isomorphism to [-x] - [x] (TauCeti.singularHomologySphereOneIso_inv_mayerVietorisδ).

Equations

• One or more equations did not get rendered due to their size.

theorem TauCeti.singularHomologySphereOneIso_inv_mayerVietorisδ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {E : Type w} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {p : ↑(Metric.sphere 0 1)} (hE : Module.finrank ℝ E = 2) {x : ↑(Metric.sphere 0 1)} (hx : x ∈ {p}ᶜ ∩ {-p}ᶜ) : CategoryTheory.CategoryStruct.comp (singularHomologySphereOneIso R hE hx).inv (TopCat.mayerVietorisδ R ⋯ ⋯ ⋯ 1 0 singularHomologySphereOneIso_inv_mayerVietorisδ._proof_2) = singularHomology₀Section R ⟨-x, ⋯⟩ - singularHomology₀Section R ⟨x, hx⟩

The Mayer–Vietoris sequence of a circle covered by two arcs. The generator of H₁(S) given by TauCeti.singularHomologySphereOneIso is sent by the Mayer–Vietoris connecting morphism of the cover of S by S ∖ {p} and S ∖ {-p} to the class [-x] - [x] in the zeroth homology of S ∖ {p, -p}, the difference of points on its two arcs.

theorem TauCeti.singularHomologySphereOneIso_inv_mayerVietorisδ_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {E : Type w} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {p : ↑(Metric.sphere 0 1)} (hE : Module.finrank ℝ E = 2) {x : ↑(Metric.sphere 0 1)} (hx : x ∈ {p}ᶜ ∩ {-p}ᶜ) {Z : C} (h : (TopCat.toSSet.obj ↧↑({p}ᶜ ∩ {-p}ᶜ)).homology R 0 ⟶ Z) : CategoryTheory.CategoryStruct.comp (singularHomologySphereOneIso R hE hx).inv (CategoryTheory.CategoryStruct.comp (TopCat.mayerVietorisδ R ⋯ ⋯ ⋯ 1 0 singularHomologySphereOneIso_inv_mayerVietorisδ._proof_2) h) = CategoryTheory.CategoryStruct.comp (singularHomology₀Section R ⟨-x, ⋯⟩ - singularHomology₀Section R ⟨x, hx⟩) h

The Mayer–Vietoris sequence of a circle covered by two arcs. The generator of H₁(S) given by TauCeti.singularHomologySphereOneIso is sent by the Mayer–Vietoris connecting morphism of the cover of S by S ∖ {p} and S ∖ {-p} to the class [-x] - [x] in the zeroth homology of S ∖ {p, -p}, the difference of points on its two arcs.

theorem TauCeti.isZero_reducedSingularHomologyFunctor_sphere_of_ne {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {E : Type w} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n k : ℕ} (h : Module.finrank ℝ E = n + 1) (hk : k ≠ n) : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor R k).obj ↧↑(Metric.sphere 0 1))

The reduced homology of a sphere vanishes outside its dimension. For a real inner product space E of dimension n + 1, the reduced singular homology of its unit sphere vanishes in every degree k ≠ n.

noncomputable def TauCeti.reducedSingularHomologySphereIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {E : Type w} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (h : Module.finrank ℝ E = n + 1) : (reducedSingularHomologyFunctor R n).obj ↧↑(Metric.sphere 0 1) ≅ R

The reduced homology of a sphere in its dimension. For a real inner product space E of dimension n + 1, the reduced singular homology of its unit sphere in degree n is one copy of the coefficient object. The isomorphism iterates the suspension isomorphism TauCeti.reducedSingularHomologySphereSuccIso along a chosen point of each sphere down to the zero-sphere TauCeti.reducedSingularHomologySphereZeroIso; it depends on these choices, and is one choice of generator rather than a canonical identification.

Equations

• TauCeti.reducedSingularHomologySphereIso R h = TauCeti.reducedSingularHomologySphereIsoAux✝ R n E h

@[simp]

theorem TauCeti.reducedSingularHomologySphereIso_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {E : Type w} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (h : Module.finrank ℝ E = 0 + 1) [Nonempty ↑(Metric.sphere 0 1)] : reducedSingularHomologySphereIso R h = reducedSingularHomologySphereZeroIso R h (Classical.arbitrary ↑(Metric.sphere 0 1))

For a one-dimensional space, the chosen generator of H_red₀(S) is the zero-sphere isomorphism TauCeti.reducedSingularHomologySphereZeroIso at the point Classical.arbitrary of the sphere.

@[simp]

theorem TauCeti.reducedSingularHomologySphereIso_succ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {E : Type w} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (h : Module.finrank ℝ E = n + 1 + 1) [Nonempty ↑(Metric.sphere 0 1)] (hp : Module.finrank ℝ ↥(ℝ ∙ ↑(Classical.arbitrary ↑(Metric.sphere 0 1)))ᗮ = n + 1) : reducedSingularHomologySphereIso R h = reducedSingularHomologySphereSuccIso R (Classical.arbitrary ↑(Metric.sphere 0 1)) n ≪≫ reducedSingularHomologySphereIso R hp

For a space of dimension n + 2, the chosen generator of H_redₙ₊₁(S) is the suspension isomorphism at the point p = Classical.arbitrary of the sphere, followed by the chosen generator of the reduced homology of the equator, the unit sphere of (ℝ ∙ p)ᗮ. The dimension hypothesis hp on the equator may be any proof of it.

theorem TauCeti.isZero_reducedSingularHomologyFunctor_topCatSphere_of_ne {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) {n k : ℕ} (hk : k ≠ n) : CategoryTheory.Limits.IsZero ((reducedSingularHomologyFunctor R k).obj (TopCat.sphere n))

The reduced homology of TopCat.sphere n vanishes outside degree n.

noncomputable def TauCeti.reducedSingularHomologyTopCatSphereIso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (n : ℕ) : (reducedSingularHomologyFunctor R n).obj (TopCat.sphere n) ≅ R

The reduced homology of TopCat.sphere n in degree n is one copy of the coefficient object. This is one choice of generator, transported from TauCeti.reducedSingularHomologySphereIso along TauCeti.diskBoundaryHomeomorph.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.reducedSingularHomologyTopCatSphereIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Abelian C] (R : C) (n : ℕ) : (reducedSingularHomologyTopCatSphereIso R n).hom = CategoryTheory.CategoryStruct.comp ((reducedSingularHomologyFunctor R n).map (TopCat.ofHom (diskBoundaryHomeomorph (n + 1)).toHomotopyEquiv.toFun)) (reducedSingularHomologySphereIso R ⋯).hom

The chosen generator of H_redₙ(TopCat.sphere n) is the map induced by the homeomorphism TauCeti.diskBoundaryHomeomorph with the unit sphere of EuclideanSpace ℝ (ULift (Fin (n + 1))), followed by the chosen generator TauCeti.reducedSingularHomologySphereIso of that sphere.