Positive-dimensional degree from bundled sphere orientations

Packages the conditional degree API through SphereOrientationPos, so all positive dimensions share one coherent family of top-homology orientations. It derives identity, composition, homotopy invariance, and conditional odd-map results from that bundle. Later sphere-homology modules construct the unconditional orientation used by the public final theorem.

Positive-dimensional degree

noncomputable def SphereOddDegree.degreePos (o : SphereOrientationPos) {n : ℕ} (hn : 1 ≤ n) (f : C(Sphere n, Sphere n)) : ℤ

The integer positive-dimensional degree of a self-map f : C(Sphere n, Sphere n) (n ≥ 1), read off a positive top-homology orientation o : SphereOrientationPos.

This is degreeOfIso of Degree.lean evaluated at the orientation's chosen identification o.iso n hn : Hₙ(Sⁿ; ℤ) ≅ ℤ; in particular it carries no free per-dimension SphereTopHomologyIso n argument — only the bundled o.

Equations

• SphereOddDegree.degreePos o hn f = SphereOddDegree.degreeOfIso (o.iso n hn) f

theorem SphereOddDegree.degreePos_eq_degreeOfIso (o : SphereOrientationPos) {n : ℕ} (hn : 1 ≤ n) (f : C(Sphere n, Sphere n)) : degreePos o hn f = degreeOfIso (o.iso n hn) f

Compatibility with the conditional API. degreePos is the conditional degreeOfIso at the orientation's chosen identification.

theorem SphereOddDegree.degreePos_eq_orientation_degree (o : SphereOrientationPos) {n : ℕ} (hn : 1 ≤ n) (f : C(Sphere n, Sphere n)) : degreePos o hn f = o.degree hn f

Agreement with SphereOrientationPos.degree.

@[simp]

theorem SphereOddDegree.degreePos_id (o : SphereOrientationPos) {n : ℕ} (hn : 1 ≤ n) : degreePos o hn (ContinuousMap.id (Sphere n)) = 1

The degree of the identity map is 1.

theorem SphereOddDegree.degreePos_comp (o : SphereOrientationPos) {n : ℕ} (hn : 1 ≤ n) (f g : C(Sphere n, Sphere n)) : degreePos o hn (g.comp f) = degreePos o hn g * degreePos o hn f

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

theorem SphereOddDegree.degreePos_well_defined (o o' : SphereOrientationPos) {n : ℕ} (hn : 1 ≤ n) (f : C(Sphere n, Sphere n)) : degreePos o hn f = degreePos o' hn f

Choice independence. Any two positive orientations assign the same degree: the integer is read off the intrinsic endomorphism ring, independent of the chosen identification.

theorem SphereOddDegree.degreePos_homotopy (o : SphereOrientationPos) {n : ℕ} (hn : 1 ≤ n) {f g : C(Sphere n, Sphere n)} (h : f.Homotopic g) : degreePos o hn f = degreePos o hn g

Homotopy invariance of the positive degree — unconditional. Homotopic self-maps of Sphere n (n ≥ 1) have equal degree. No prism hypothesis is needed: singularPrismOperator is a theorem.

theorem SphereOddDegree.not_homotopic_of_degreePos_ne (o : SphereOrientationPos) {n : ℕ} (hn : 1 ≤ n) {f g : C(Sphere n, Sphere n)} (h : degreePos o hn f ≠ degreePos o hn g) : ¬f.Homotopic g

Homotopy-class invariant. Self-maps of different positive degree are not homotopic.

Standard wrappers for the positive degree

theorem SphereOddDegree.degreePos_const (o : SphereOrientationPos) {n : ℕ} (hn : 1 ≤ n) (c : Sphere n) : degreePos o hn (ContinuousMap.const (Sphere n) c) = 0

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

theorem SphereOddDegree.degreePos_homeomorph_eq_one_or_neg_one (o : SphereOrientationPos) {n : ℕ} (hn : 1 ≤ n) (h : Sphere n ≃ₜ Sphere n) : degreePos o hn ↑h = 1 ∨ degreePos o hn ↑h = -1

The degree of a self-homeomorphism is ±1.

theorem SphereOddDegree.odd_degreePos_homeomorph (o : SphereOrientationPos) {n : ℕ} (hn : 1 ≤ n) (h : Sphere n ≃ₜ Sphere n) : Odd (degreePos o hn ↑h)

The degree of a self-homeomorphism is odd.

theorem SphereOddDegree.degreePos_antipodal_eq_one_or_neg_one (o : SphereOrientationPos) {n : ℕ} (hn : 1 ≤ n) : degreePos o hn (antipodal n) = 1 ∨ degreePos o hn (antipodal n) = -1

The degree of the antipodal map is ±1.

theorem SphereOddDegree.odd_degreePos_antipodal (o : SphereOrientationPos) {n : ℕ} (hn : 1 ≤ n) : Odd (degreePos o hn (antipodal n))

The degree of the antipodal map is odd.

theorem SphereOddDegree.degreePos_intCast_zmodTwo_eq_one_iff_odd (o : SphereOrientationPos) {n : ℕ} (hn : 1 ≤ n) (f : C(Sphere n, Sphere n)) : ↑(degreePos o hn f) = 1 ↔ Odd (degreePos o hn f)

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

The final odd-map theorem, with the free SphereTopHomologyIso n removed

theorem SphereOddDegree.oddMap_degreePos_odd_final (o : SphereOrientationPos) {n : ℕ} (hn : 1 ≤ n) (hcmp : ModTwoTopClassComparison (o.iso n hn)) (htop : OddMapFixesTopClass n) (f : C(Sphere n, Sphere n)) (hf : IsOddMap f) : Odd (degreePos o hn f)

Final odd-map degree theorem through a positive orientation.

This is oddMap_degree_odd_final with the free e : SphereTopHomologyIso n argument replaced by a bundled positive orientation o : SphereOrientationPos together with hn : 1 ≤ n. Given the two remaining named topological inputs

• hcmp : ModTwoTopClassComparison (o.iso n hn) — a self-map fixing a nonzero top F₂-class has odd integer degree;
• htop : OddMapFixesTopClass n — an odd self-map fixes a nonzero top F₂-class,

every odd self-map f of Sⁿ (n ≥ 1) has odd degreePos. For 1 ≤ n the statement no longer carries a free SphereTopHomologyIso n.

theorem SphereOddDegree.oddMap_degreePos_odd_of_monodromyFunctional (o : SphereOrientationPos) {n : ℕ} (hn : 1 ≤ n) (m : MonodromyFunctional n) (f : C(Sphere n, Sphere n)) (hf : IsOddMap f) (hne : (CategoryTheory.ConcreteCategory.hom (projPullback n n)) (cupPowZMod2 (rpAlpha n m) n) ≠ 0) (hcmp : (CategoryTheory.ConcreteCategory.hom (spherePullback f n)) ((CategoryTheory.ConcreteCategory.hom (projPullback n n)) (cupPowZMod2 (rpAlpha n m) n)) = (CategoryTheory.ConcreteCategory.hom (projPullback n n)) (cupPowZMod2 (rpAlpha n m) n) → (CategoryTheory.ConcreteCategory.hom (projPullback n n)) (cupPowZMod2 (rpAlpha n m) n) ≠ 0 → ↑(degreePos o hn f) = 1) : Odd (degreePos o hn f)

Final odd-map theorem through a positive orientation and a monodromy functional. This is oddMap_degree_odd_of_monodromyFunctional with the free SphereTopHomologyIso n replaced by a bundled positive orientation; the action hypothesis fbar^*(α) = α and its top-power consequence are discharged via the constructed class rpAlpha n m. The remaining inputs are the orientation o, the monodromy functional m, and the sphere-side comparison data.