Degree functoriality and homotopy invariance (consolidation layer) #

This file consolidates the standard degree API — identity, composition, homotopy invariance, and the homotopy-class–distinguishing application form — into the strongest formalized statements the library supports today.

The degree API is parameterized by a top-homology identification Hₙ(Sⁿ; ℤ) ≅ ℤ (a term of SphereTopHomologyIso n for n ≥ 1). Homotopy invariance is conditional on the required algebraic prism operator (SingularPrismOperator), exactly as in HomotopyInvariance.lean.

What is added here, building only on Degree.lean, SphereTopHomology.lean, DegreeAPIStrengthening.lean and HomotopyInvariance.lean:

TopCat.sphere-native homotopy invariance. degreeOfIsoTop_eq_of_homotopic (conditional on the prism operator): homotopic self-morphisms of TopCat.sphere n have equal TopCat-degree.
Degree as a monoid homomorphism + power law. degreeMonoidHomTop, the multiplicative End (TopCat.sphere n) →* ℤ underlying degreeOfIsoTop, with degreeMonoidHomTop_apply and the power law degreeOfIsoTop_pow (degree (gᵏ) = (degree g)ᵏ).
Homotopy-class invariant (the application form). The contrapositives of homotopy invariance: maps of different degree are not homotopic (not_homotopic_of_degreeOfIso_ne, not_homotopic_of_degreeOfIsoTop_ne, and the oriented SphereOrientation.not_homotopic_of_degree_ne). This is the exact shape the final odd-map theorem consumes.
Oriented TopCat degree. SphereOrientation.degreeTop with degreeTop_id, degreeTop_comp, degreeTop_eq_of_homotopic, and the compatibility degreeTop_toTopCatSphereSelfMap identifying it with the raw Sphere n degree.

Every statement is conditional only on the explicit identification e (resp. a SphereOrientation) and, for homotopy invariance, on SingularPrismOperator — the honest set of hypotheses. None of them is a disguised unconditional theorem.

`TopCat.sphere`-native homotopy invariance #

source

theorem SphereOddDegree.degreeOfIsoTop_eq_of_homotopic (prism : SingularPrismOperator) {n : ℕ} (e : SphereTopHomologyIso n) {g h : TopCat.sphere n ⟶ TopCat.sphere n} (H : (TopCat.Hom.hom g).Homotopic (TopCat.Hom.hom h)) :

degreeOfIsoTop e g = degreeOfIsoTop e h

Conditional homotopy invariance of the TopCat-degree.

Assuming the prism operator, two self-morphisms g, h of TopCat.sphere n whose underlying continuous maps are homotopic have equal TopCat-degree (relative to any chosen identification e : Hₙ(Sⁿ; ℤ) ≅ ℤ).

Degree as a monoid homomorphism and the power law #

source

noncomputable def SphereOddDegree.degreeMonoidHomTop {n : ℕ} (e : SphereTopHomologyIso n) :

CategoryTheory.End (TopCat.sphere n) →* ℤ

The multiplicative degree homomorphism End (TopCat.sphere n) →* ℤ underlying degreeOfIsoTop: it sends the identity to 1 and respects the monoid product of End (TopCat.sphere n) (categorical composition). This is the functorial composite of Functor.mapEnd for the homology functor with the scalar ring homomorphism degreeRingHomOfIso.

Equations

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

Instances For

source

@[simp]

theorem SphereOddDegree.degreeMonoidHomTop_apply {n : ℕ} (e : SphereTopHomologyIso n) (g : TopCat.sphere n ⟶ TopCat.sphere n) :

(degreeMonoidHomTop e) g = degreeOfIsoTop e g

degreeMonoidHomTop computes the TopCat-degree.

source

theorem SphereOddDegree.degreeOfIsoTop_pow {n : ℕ} (e : SphereTopHomologyIso n) (g : CategoryTheory.End (TopCat.sphere n)) (k : ℕ) :

degreeOfIsoTop e (g ^ k) = degreeOfIsoTop e g ^ k

Power law. The TopCat-degree of a k-fold self-composite is the k-th power of the degree: degree (gᵏ) = (degree g)ᵏ (powers in the endomorphism monoid End (TopCat.sphere n)).

Homotopy-class invariant (the application form) #

The contrapositives of homotopy invariance: a degree mismatch obstructs a homotopy. This is the shape the final odd-map / Borsuk–Ulam–style argument consumes — a degree invariant distinguishing homotopy classes of self-maps.

source

theorem SphereOddDegree.not_homotopic_of_degreeOfIso_ne (prism : SingularPrismOperator) {n : ℕ} (e : SphereTopHomologyIso n) {f g : C(Sphere n, Sphere n)} (h : degreeOfIso e f ≠ degreeOfIso e g) :

¬f.Homotopic g

Maps of different degree are not homotopic (raw C(Sphere n, Sphere n) form, conditional on the prism operator).

source

theorem SphereOddDegree.not_homotopic_of_degreeOfIsoTop_ne (prism : SingularPrismOperator) {n : ℕ} (e : SphereTopHomologyIso n) {g h : TopCat.sphere n ⟶ TopCat.sphere n} (hne : degreeOfIsoTop e g ≠ degreeOfIsoTop e h) :

¬(TopCat.Hom.hom g).Homotopic (TopCat.Hom.hom h)

Maps of different degree are not homotopic (TopCat.sphere n form, conditional on the prism operator).

Oriented `TopCat` degree #

The bundled-orientation analogue of degreeOfIsoTop, repackaging the same identity / composition / homotopy-invariance facts on a SphereOrientation.

source