Sphere top homology and degree interfaces

Defines the integral top-homology objects for spheres, orientation packages, and degree relative to a selected top-homology isomorphism. Positive-dimensional unconditional instances are built from the Mayer--Vietoris suspension computation and re-exported by the final API.

Top-homology abbreviations over TopCat.sphere n

@[reducible, inline]

noncomputable abbrev SphereOddDegree.sphereHomologyℤ (k n : ℕ) : ModuleCat ℤ

Hₖ(Sⁿ; ℤ): the k-th integral singular homology of Mathlib's categorical sphere object TopCat.sphere n.

Equations

• SphereOddDegree.sphereHomologyℤ k n = (SphereOddDegree.singularHomologyℤ k).obj (TopCat.sphere n)

@[reducible, inline]

noncomputable abbrev SphereOddDegree.sphereTopHomologyℤ (n : ℕ) : ModuleCat ℤ

The top homology Hₙ(Sⁿ; ℤ) — the group that should be ≅ ℤ and that the topological degree reads.

Equations

• SphereOddDegree.sphereTopHomologyℤ n = SphereOddDegree.sphereHomologyℤ n n

Model bridge: TopCat.sphere n vs. the raw Sphere n model

noncomputable def SphereOddDegree.sphereModelHomologyIso (k n : ℕ) : sphereHomologyℤ k n ≅ (singularHomologyℤ k).obj ↧(Sphere n)

Model bridge on homology. The integral singular homology of the categorical sphere TopCat.sphere n is isomorphic to that of the library's raw subtype model Sphere n, by applying the homology functor to the bridge isomorphism topCatSphereIso (TopCatBridge.lean).

Equations

• SphereOddDegree.sphereModelHomologyIso k n = (SphereOddDegree.singularHomologyℤ k).mapIso (SphereOddDegree.topCatSphereIso n)

Genuine low-dimensional case: n = 0

Sphere 0 is the unit sphere in ℝ¹, i.e. the two-point set {±e}. It is finite (at most two points by sphere_zero_eq_or_neg), hence discrete and totally disconnected; the bridge homeomorphism transports this to TopCat.sphere 0.

instance SphereOddDegree.instFiniteSphereZero : Finite (Sphere 0)

Sphere 0 is finite: every point equals a fixed p or its antipode -p (sphere_zero_eq_or_neg), so it is the image of Bool.

instance SphereOddDegree.instTotallyDisconnectedTopCatSphereZero : TotallyDisconnectedSpace ↑(TopCat.sphere 0)

TopCat.sphere 0 is totally disconnected: it is homeomorphic (via topCatSphereHomeomorph) to the finite, hence discrete, two-point set Sphere 0.

theorem SphereOddDegree.sphere0_singularHomologyℤ_isZero (k : ℕ) (hk : k ≠ 0) : CategoryTheory.Limits.IsZero (sphereHomologyℤ k 0)

Genuine low-dimensional homology of S⁰. For k ≠ 0, Hₖ(S⁰; ℤ) = 0, since S⁰ is totally disconnected. (The k = 0 value is H₀(S⁰; ℤ) ≅ ℤ², which is not ℤ; the degree theory therefore concerns n ≥ 1.)

Conditional isomorphism wrappers

@[reducible, inline]

abbrev SphereOddDegree.SphereTopHomologyIso (n : ℕ) : Type

The type of top-homology identifications Hₙ(Sⁿ; ℤ) ≅ ℤ (over TopCat.sphere n). A term of this type selects an orientation in dimension n.

Equations

• SphereOddDegree.SphereTopHomologyIso n = (SphereOddDegree.sphereTopHomologyℤ n ≅ ↧ℤ)

noncomputable def SphereOddDegree.sphereTopHomologyIsoOfModelIso {n : ℕ} (e : (singularHomologyℤ n).obj ↧(Sphere n) ≅ ↧ℤ) : SphereTopHomologyIso n

Transport an identification Hₙ(Sⁿ) ≅ ℤ from the raw Sphere n model to the categorical TopCat.sphere n model, through the homology model bridge.

Equations

• SphereOddDegree.sphereTopHomologyIsoOfModelIso e = SphereOddDegree.sphereModelHomologyIso n n ≪≫ e

noncomputable def SphereOddDegree.modelIsoOfSphereTopHomologyIso {n : ℕ} (e : SphereTopHomologyIso n) : (singularHomologyℤ n).obj ↧(Sphere n) ≅ ↧ℤ

Transport an identification Hₙ(Sⁿ) ≅ ℤ from the categorical TopCat.sphere n model to the raw Sphere n model, through the homology model bridge.

Equations

• SphereOddDegree.modelIsoOfSphereTopHomologyIso e = (SphereOddDegree.sphereModelHomologyIso n n).symm ≪≫ e

Bundled orientation ⇒ unconditional degree

SphereOrientation bundles a choice of Hₙ(Sⁿ; ℤ) ≅ ℤ in every dimension and packages the degree of Degree.lean relative to that orientation data.

structure SphereOddDegree.SphereOrientation : Type

A choice of top-homology identification Hₙ(Sⁿ; ℤ) ≅ ℤ in every dimension. This structure provides the orientation data used by the degree API.

• iso (n : ℕ) : SphereTopHomologyIso n

  The identification Hₙ(Sⁿ; ℤ) ≅ ℤ in dimension n.

noncomputable def SphereOddDegree.SphereOrientation.degree (o : SphereOrientation) {n : ℕ} (f : C(Sphere n, Sphere n)) : ℤ

The integer degree of a self-map of Sphere n, read off the supplied top-homology identification o.iso n. Honest and unconditional once a SphereOrientation is provided.

Equations

• o.degree f = SphereOddDegree.degreeOfIso (o.iso n) f

@[simp]

theorem SphereOddDegree.SphereOrientation.degree_id (o : SphereOrientation) (n : ℕ) : o.degree (ContinuousMap.id (Sphere n)) = 1

The degree of the identity map is 1.

theorem SphereOddDegree.SphereOrientation.degree_comp (o : SphereOrientation) {n : ℕ} (f g : C(Sphere n, Sphere n)) : o.degree (g.comp f) = o.degree g * o.degree f

The degree is multiplicative: degree (g ∘ f) = degree g * degree f.

theorem SphereOddDegree.SphereOrientation.degree_well_defined (o o' : SphereOrientation) {n : ℕ} (f : C(Sphere n, Sphere n)) : o.degree f = o'.degree f

Choice independence. Any two orientations assign the same degree, since the relative degree is independent of the chosen identification.

theorem SphereOddDegree.SphereOrientation.degree_eq_of_homotopic (o : SphereOrientation) (prism : SingularPrismOperator) {n : ℕ} {f g : C(Sphere n, Sphere n)} (h : f.Homotopic g) : o.degree f = o.degree g

Homotopy invariance of the degree (conditional on the prism operator). Homotopic self-maps of Sphere n have equal degree.