Bundled sphere degree setup

Packages positive-dimensional sphere orientation data and a singular prism operator into SphereDegreeSetup, then exposes degree, composition, homeomorphism, antipodal, and homotopy invariance APIs from that setup. Unconditional instances of both fields are constructed later and re-exported through SphereOddDegree.Final.

The single compact setup structure

structure SphereOddDegree.SphereDegreeSetup : Type

A sphere-degree setup bundling the two inputs used by the integral degree theory of sphere self-maps.

• orientation : SphereOrientationPos — a choice of top-homology identification Hₙ(Sⁿ; ℤ) ≅ ℤ in every dimension n ≥ 1, represented by a SphereSuspensionTower.
• prism : SingularPrismOperator — the algebraic prism operator underlying homotopy invariance of singular homology.

Bundling both means a downstream consumer assumes one hypothesis rather than several, and every degree theorem — including homotopy invariance — is unconditional relative to a SphereDegreeSetup. The fields are supplied by the final assembly modules.

• orientation : SphereOrientationPos

  The positive top-homology orientation Hₙ(Sⁿ; ℤ) ≅ ℤ (n ≥ 1).

• prism : SingularPrismOperator

  The algebraic prism operator for homotopy invariance of singular homology.

The degree on the library sphere model Sphere n

noncomputable def SphereOddDegree.SphereDegreeSetup.degree (S : SphereDegreeSetup) {n : ℕ} (hn : 1 ≤ n) (f : C(Sphere n, Sphere n)) : ℤ

The integer degree of a self-map f : C(Sphere n, Sphere n) (n ≥ 1), read off the setup's top-homology orientation. Honest and unconditional given the setup S.

Equations

• S.degree hn f = S.orientation.degree hn f

theorem SphereOddDegree.SphereDegreeSetup.degree_eq_degreeOfIso (S : SphereDegreeSetup) {n : ℕ} (hn : 1 ≤ n) (f : C(Sphere n, Sphere n)) : S.degree hn f = degreeOfIso (S.orientation.iso n hn) f

Compatibility with the conditional API. The setup degree is the conditional degreeOfIso of Degree.lean at the setup's chosen identification.

@[simp]

theorem SphereOddDegree.SphereDegreeSetup.degree_id (S : SphereDegreeSetup) {n : ℕ} (hn : 1 ≤ n) : S.degree hn (ContinuousMap.id (Sphere n)) = 1

The degree of the identity map is 1.

theorem SphereOddDegree.SphereDegreeSetup.degree_comp (S : SphereDegreeSetup) {n : ℕ} (hn : 1 ≤ n) (f g : C(Sphere n, Sphere n)) : S.degree hn (g.comp f) = S.degree hn g * S.degree hn f

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

theorem SphereOddDegree.SphereDegreeSetup.degree_well_defined (S S' : SphereDegreeSetup) {n : ℕ} (hn : 1 ≤ n) (f : C(Sphere n, Sphere n)) : S.degree hn f = S'.degree hn f

Choice independence. Any two setups assign the same degree (the integer is read off the intrinsic endomorphism ring, independent of the chosen identification).

theorem SphereOddDegree.SphereDegreeSetup.degree_homotopy (S : SphereDegreeSetup) {n : ℕ} (hn : 1 ≤ n) {f g : C(Sphere n, Sphere n)} (h : f.Homotopic g) : S.degree hn f = S.degree hn g

Homotopy invariance — unconditional given the setup. Homotopic self-maps of Sphere n (n ≥ 1) have equal degree. Unlike the conditional API, no separate prism hypothesis is needed: the prism is part of S.

theorem SphereOddDegree.SphereDegreeSetup.not_homotopic_of_degree_ne (S : SphereDegreeSetup) {n : ℕ} (hn : 1 ≤ n) {f g : C(Sphere n, Sphere n)} (h : S.degree hn f ≠ S.degree hn g) : ¬f.Homotopic g

Homotopy-class invariant. Self-maps of different degree are not homotopic. No separate prism hypothesis — it is part of S.

The degree on the categorical sphere TopCat.sphere n

noncomputable def SphereOddDegree.SphereDegreeSetup.degreeTopCat (S : SphereDegreeSetup) {n : ℕ} (hn : 1 ≤ n) (g : TopCat.sphere n ⟶ TopCat.sphere n) : ℤ

The integer degree of a TopCat.sphere n self-morphism g, read off the setup's orientation. the library-sphere degree is its value on the model transport (degree_eq_degreeTopCat).

Equations

• S.degreeTopCat hn g = SphereOddDegree.degreeOfIsoTop (S.orientation.iso n hn) g

@[simp]

theorem SphereOddDegree.SphereDegreeSetup.degreeTopCat_id (S : SphereDegreeSetup) {n : ℕ} (hn : 1 ≤ n) : S.degreeTopCat hn (CategoryTheory.CategoryStruct.id (TopCat.sphere n)) = 1

The TopCat-degree of the identity morphism is 1.

theorem SphereOddDegree.SphereDegreeSetup.degreeTopCat_comp (S : SphereDegreeSetup) {n : ℕ} (hn : 1 ≤ n) (g h : TopCat.sphere n ⟶ TopCat.sphere n) : S.degreeTopCat hn (CategoryTheory.CategoryStruct.comp g h) = S.degreeTopCat hn h * S.degreeTopCat hn g

The TopCat-degree is multiplicative under categorical composition (the factors reverse, as for degreeOfIsoTop_comp).

theorem SphereOddDegree.SphereDegreeSetup.degreeTopCat_homotopy (S : SphereDegreeSetup) {n : ℕ} (hn : 1 ≤ n) {g h : TopCat.sphere n ⟶ TopCat.sphere n} (H : (TopCat.Hom.hom g).Homotopic (TopCat.Hom.hom h)) : S.degreeTopCat hn g = S.degreeTopCat hn h

Homotopy invariance of the TopCat-degree — unconditional given the setup. Self-morphisms with homotopic underlying maps have equal TopCat-degree.

theorem SphereOddDegree.SphereDegreeSetup.degree_eq_degreeTopCat (S : SphereDegreeSetup) {n : ℕ} (hn : 1 ≤ n) (f : C(Sphere n, Sphere n)) : S.degree hn f = S.degreeTopCat hn (toTopCatSphereSelfMap f)

Model compatibility. the library-sphere degree of f is the TopCat-degree of its model transport toTopCatSphereSelfMap f.

Standard degree wrappers, under the single setup

theorem SphereOddDegree.SphereDegreeSetup.degree_const (S : SphereDegreeSetup) {n : ℕ} (hn : 1 ≤ n) (c : Sphere n) : S.degree hn (ContinuousMap.const (Sphere n) c) = 0

The degree of a one-point map is 0 (n ≥ 1).

theorem SphereOddDegree.SphereDegreeSetup.degree_homeomorph_eq_one_or_neg_one (S : SphereDegreeSetup) {n : ℕ} (hn : 1 ≤ n) (h : Sphere n ≃ₜ Sphere n) : S.degree hn ↑h = 1 ∨ S.degree hn ↑h = -1

The degree of a self-homeomorphism is ±1.

theorem SphereOddDegree.SphereDegreeSetup.odd_degree_homeomorph (S : SphereDegreeSetup) {n : ℕ} (hn : 1 ≤ n) (h : Sphere n ≃ₜ Sphere n) : Odd (S.degree hn ↑h)

The degree of a self-homeomorphism is odd.

theorem SphereOddDegree.SphereDegreeSetup.degree_antipodal_eq_one_or_neg_one (S : SphereDegreeSetup) {n : ℕ} (hn : 1 ≤ n) : S.degree hn (antipodal n) = 1 ∨ S.degree hn (antipodal n) = -1

The degree of the antipodal map is ±1.

theorem SphereOddDegree.SphereDegreeSetup.odd_degree_antipodal (S : SphereDegreeSetup) {n : ℕ} (hn : 1 ≤ n) : Odd (S.degree hn (antipodal n))

The degree of the antipodal map is odd.

theorem SphereOddDegree.SphereDegreeSetup.degree_antipodal_eq_neg_one_pow_of_eq_det (S : SphereDegreeSetup) {n : ℕ} (hn : 1 ≤ n) (h : DegreeEqAmbientDet (S.orientation.iso n hn)) : S.degree hn (antipodal n) = (-1) ^ (n + 1)

Conditional antipodal value. Given the orientation-sign datum DegreeEqAmbientDet (degree of the antipodal map = its ambient determinant), the antipodal degree is (-1)^(n+1).

theorem SphereOddDegree.SphereDegreeSetup.degree_intCast_zmodTwo_eq_one_iff_odd (S : SphereDegreeSetup) {n : ℕ} (hn : 1 ≤ n) (f : C(Sphere n, Sphere n)) : ↑(S.degree hn f) = 1 ↔ Odd (S.degree hn f)

Mod-2 comparison. The reduction of the degree to ZMod 2 is 1 iff the degree is odd.

theorem SphereOddDegree.SphereDegreeSetup.degree_antipodal_intCast_zmodTwo_eq_one (S : SphereDegreeSetup) {n : ℕ} (hn : 1 ≤ n) : ↑(S.degree hn (antipodal n)) = 1

The mod-2 degree of the antipodal map is 1.

Assembling a degree setup

noncomputable def SphereOddDegree.SphereSuspensionTower.degreeSetup (T : SphereSuspensionTower) (prism : SingularPrismOperator) : SphereDegreeSetup

A SphereSuspensionTower and a SingularPrismOperator assemble a full SphereDegreeSetup.

Equations

• T.degreeSetup prism = { orientation := T.orientation, prism := ⋯ }

@[simp]

theorem SphereOddDegree.SphereSuspensionTower.degreeSetup_orientation (T : SphereSuspensionTower) (prism : SingularPrismOperator) : (T.degreeSetup ⋯).orientation = T.orientation