Topological degree relative to a sphere orientation

Defines the transport from the project sphere model to TopCat.sphere, the induced endomorphism on top singular homology, and the integer scalar obtained after choosing an isomorphism from top homology to ℤ. The resulting degreeOfIso API includes identity, composition, and independence of the chosen orientation isomorphism. Unconditional orientation data is supplied by later sphere-homology modules.

Orientation of the ambient antipodal map

The orientation/determinant facts about the ambient linear map x ↦ -x on ℝ^(n+1). The bundled antipodal self-map antipodal n is the restriction of this ambient map to the unit sphere, and its determinant (-1)^(n+1) is the orientation sign that the topological degree degree (antipodal n) must reproduce. These facts are degree/orientation support — not point-set foundation — so they live here rather than in Antipodal.lean.

theorem SphereOddDegree.ambientNeg_eq_neg_one_smul (n : ℕ) : -LinearMap.id = -1 • LinearMap.id

The ambient antipodal map x ↦ -x on ℝ^(n+1), as a linear endomorphism, equals scalar multiplication by -1. This is the linear-algebra shadow of the bundled antipodal n self-map (which is its restriction to the unit sphere).

theorem SphereOddDegree.det_ambientNeg (n : ℕ) : LinearMap.det (-LinearMap.id) = (-1) ^ (n + 1)

The determinant of the ambient antipodal linear map x ↦ -x on ℝ^(n+1) is (-1)^(n+1).

This is the ambient orientation calculation used by the later theorem degree (antipodal n) = (-1)^(n+1): the antipodal map is the restriction to the sphere of this linear map, and its determinant gives the expected degree sign.

Model transport of self-maps to TopCat.sphere n

noncomputable def SphereOddDegree.toTopCatSphereSelfMap {n : ℕ} (f : C(Sphere n, Sphere n)) : TopCat.sphere n ⟶ TopCat.sphere n

Transport a continuous self-map of the raw sphere model Sphere n to a self-morphism of Mathlib's categorical sphere TopCat.sphere n, by conjugating with the bridge isomorphism topCatSphereIso.

Equations

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

@[simp]

theorem SphereOddDegree.toTopCatSphereSelfMap_id (n : ℕ) : toTopCatSphereSelfMap (ContinuousMap.id (Sphere n)) = CategoryTheory.CategoryStruct.id (TopCat.sphere n)

The transport sends the identity self-map to the identity morphism.

theorem SphereOddDegree.toTopCatSphereSelfMap_comp {n : ℕ} (f g : C(Sphere n, Sphere n)) : toTopCatSphereSelfMap (g.comp f) = CategoryTheory.CategoryStruct.comp (toTopCatSphereSelfMap f) (toTopCatSphereSelfMap g)

The transport is functorial: it turns composition of continuous maps into composition of TopCat morphisms (in the same order).

Induced endomorphism of top singular homology

noncomputable def SphereOddDegree.inducedOnTopHomology {n : ℕ} (f : C(Sphere n, Sphere n)) : CategoryTheory.End ((singularHomologyℤ n).obj (TopCat.sphere n))

The endomorphism of Hₙ(TopCat.sphere n; ℤ) induced by a continuous self-map of Sphere n, through the model transport and the integral singular homology functor.

Equations

• SphereOddDegree.inducedOnTopHomology f = (SphereOddDegree.singularHomologyℤ n).map (SphereOddDegree.toTopCatSphereSelfMap f)

@[simp]

theorem SphereOddDegree.inducedOnTopHomology_id (n : ℕ) : inducedOnTopHomology (ContinuousMap.id (Sphere n)) = CategoryTheory.CategoryStruct.id ((singularHomologyℤ n).obj (TopCat.sphere n))

The induced endomorphism of the identity is the identity.

theorem SphereOddDegree.inducedOnTopHomology_comp {n : ℕ} (f g : C(Sphere n, Sphere n)) : inducedOnTopHomology (g.comp f) = CategoryTheory.CategoryStruct.comp (inducedOnTopHomology f) (inducedOnTopHomology g)

Functoriality of the induced endomorphism, in categorical composition form.

theorem SphereOddDegree.inducedOnTopHomology_comp_mul {n : ℕ} (f g : C(Sphere n, Sphere n)) : inducedOnTopHomology (g.comp f) = inducedOnTopHomology g * inducedOnTopHomology f

Functoriality of the induced endomorphism, in End-monoid product form. Note that in End X the product a * b is b ≫ a, so the order reverses.

The ℤ-endomorphism scalar API

def SphereOddDegree.evalAtOneℤ : (ℤ →ₗ[ℤ] ℤ) →+* ℤ

Evaluation at 1 as a ring homomorphism (ℤ →ₗ[ℤ] ℤ) →+* ℤ. This packages "multiplication by an integer on ℤ": a ℤ-linear endomorphism of ℤ is exactly multiplication by its value at 1, and this assignment is a ring homomorphism (map_one gives the identity ↦ 1, map_mul gives composition ↦ product).

Equations

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

theorem SphereOddDegree.endℤ_acts_by_evalAtOne (f : ℤ →ₗ[ℤ] ℤ) (x : ℤ) : f x = evalAtOneℤ f * x

A ℤ-linear endomorphism of ℤ acts by multiplication by its value at 1.

theorem SphereOddDegree.evalAtOneℤ_bijective : Function.Bijective ⇑evalAtOneℤ

Evaluation at 1 is a bijection of (ℤ →ₗ[ℤ] ℤ) onto ℤ.

Scalar extraction from End of a rank-one ℤ-module

def SphereOddDegree.degreeRingHomOfIso (M : ModuleCat ℤ) (e : M ≅ ↧ℤ) : CategoryTheory.End M →+* ℤ

Given an isomorphism e : M ≅ ℤ of ℤ-modules, the ring homomorphism End M →+* ℤ extracting the integer scalar by which an endomorphism acts: conjugate End M into End ℤ = (ℤ →ₗ[ℤ] ℤ) and evaluate at 1.

Equations

• SphereOddDegree.degreeRingHomOfIso M e = SphereOddDegree.evalAtOneℤ.comp (e.toLinearEquiv.conjRingEquiv.toRingHom.comp M.endRingEquiv.toRingHom)

noncomputable def SphereOddDegree.degreeRingEquivOfIso (M : ModuleCat ℤ) (e : M ≅ ↧ℤ) : CategoryTheory.End M ≃+* ℤ

degreeRingHomOfIso is in fact a ring isomorphism End M ≃+* ℤ: every component (the endomorphism-ring equivalence, the conjugation, and evaluation at 1) is a bijection.

Equations

• SphereOddDegree.degreeRingEquivOfIso M e = (M.endRingEquiv.trans e.toLinearEquiv.conjRingEquiv).trans (RingEquiv.ofBijective SphereOddDegree.evalAtOneℤ SphereOddDegree.evalAtOneℤ_bijective)

@[simp]

theorem SphereOddDegree.degreeRingEquivOfIso_apply (M : ModuleCat ℤ) (e : M ≅ ↧ℤ) (a : CategoryTheory.End M) : (degreeRingEquivOfIso M e) a = (degreeRingHomOfIso M e) a

The ring equivalence degreeRingEquivOfIso acts as degreeRingHomOfIso on elements.

The conditional degree relative to a chosen identification Hₙ(Sⁿ) ≅ ℤ

noncomputable def SphereOddDegree.degreeOfIso {n : ℕ} (e : (singularHomologyℤ n).obj (TopCat.sphere n) ≅ ↧ℤ) (f : C(Sphere n, Sphere n)) : ℤ

The integer degree of f relative to a chosen isomorphism e : Hₙ(Sⁿ; ℤ) ≅ ℤ. Later modules supply a canonical positive-dimensional isomorphism and expose an unconditional orientation-based degree.

Equations

• SphereOddDegree.degreeOfIso e f = (SphereOddDegree.degreeRingHomOfIso ((SphereOddDegree.singularHomologyℤ n).obj (TopCat.sphere n)) e) (SphereOddDegree.inducedOnTopHomology f)

@[simp]

theorem SphereOddDegree.degreeOfIso_id {n : ℕ} (e : (singularHomologyℤ n).obj (TopCat.sphere n) ≅ ↧ℤ) : degreeOfIso e (ContinuousMap.id (Sphere n)) = 1

The degree of the identity map is 1.

theorem SphereOddDegree.degreeOfIso_comp {n : ℕ} (e : (singularHomologyℤ n).obj (TopCat.sphere n) ≅ ↧ℤ) (f g : C(Sphere n, Sphere n)) : degreeOfIso e (g.comp f) = degreeOfIso e g * degreeOfIso e f

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

theorem SphereOddDegree.degreeOfIso_well_defined {n : ℕ} (e e' : (singularHomologyℤ n).obj (TopCat.sphere n) ≅ ↧ℤ) (f : C(Sphere n, Sphere n)) : degreeOfIso e f = degreeOfIso e' f

Choice independence. The relative degree does not depend on the chosen identification e : Hₙ(Sⁿ; ℤ) ≅ ℤ: any two choices give the same integer. This is because every component of degreeRingHomOfIso is a ring isomorphism, so the extracted scalar is read off the intrinsic ring End M, and any two ring homomorphisms ℤ →+* ℤ agree.

Homotopy invariance of the degree (conditional on the prism operator)

These wrappers feed the conditional homotopy-invariance theorem (singularHomologyMap_eq_of_homotopic, HomotopyInvariance.lean) into the degree layer. They are stated conditionally on the required prism operator SingularPrismOperator — there is Once the algebraic prism is constructed, every statement here becomes unconditional with no further change.

theorem SphereOddDegree.toTopCatSphereSelfMap_hom_homotopic {n : ℕ} {f g : C(Sphere n, Sphere n)} (h : f.Homotopic g) : (TopCat.Hom.hom (toTopCatSphereSelfMap f)).Homotopic (TopCat.Hom.hom (toTopCatSphereSelfMap g))

The model transport of a self-map of Sphere n is conjugate, on underlying spaces, to the original continuous map: homotopic self-maps f, g transport to TopCat.sphere n self-morphisms whose underlying continuous maps are homotopic.

This is ContinuousMap.Homotopic.comp applied to the conjugation by the bridge isomorphism topCatSphereIso.

theorem SphereOddDegree.inducedOnTopHomology_eq_of_homotopic (prism : SingularPrismOperator) {n : ℕ} {f g : C(Sphere n, Sphere n)} (h : f.Homotopic g) : inducedOnTopHomology f = inducedOnTopHomology g

Conditional homotopy invariance of the induced top-homology endomorphism.

Assuming the prism operator, homotopic self-maps f, g : C(Sphere n, Sphere n) induce the same endomorphism of Hₙ(TopCat.sphere n; ℤ).

theorem SphereOddDegree.degreeOfIso_eq_of_homotopic (prism : SingularPrismOperator) {n : ℕ} (e : (singularHomologyℤ n).obj (TopCat.sphere n) ≅ ↧ℤ) {f g : C(Sphere n, Sphere n)} (h : f.Homotopic g) : degreeOfIso e f = degreeOfIso e g

Conditional homotopy invariance of the degree.

Assuming the prism operator, homotopic self-maps of Sphere n have equal degree (relative to any chosen identification e : Hₙ(Sⁿ; ℤ) ≅ ℤ). This is the form the sphere-degree theory consumes: the integer degree is a homotopy invariant.