Strengthened sphere-degree API

Extends degreeOfIso and SphereOrientation.degree with categorical-sphere wrappers, constant maps, homeomorphisms, and antipodal parity results. The declarations are parameterized by a chosen top-homology isomorphism or orientation; later modules supply the unconditional positive-dimensional orientation.

Degree of a TopCat.sphere n self-morphism

The degree relative to e reads off the integer scalar by which a self-morphism of TopCat.sphere n acts on top homology. This is the most model-agnostic form of the conditional degree: it consumes a raw categorical morphism, and the raw Sphere n degree degreeOfIso is its image under the model transport.

noncomputable def SphereOddDegree.degreeOfIsoTop {n : ℕ} (e : SphereTopHomologyIso n) (g : TopCat.sphere n ⟶ TopCat.sphere n) : ℤ

The integer degree of a TopCat.sphere n self-morphism g relative to a chosen identification e : Hₙ(Sⁿ; ℤ) ≅ ℤ. The raw Sphere n degree is the special case g = toTopCatSphereSelfMap f (see degreeOfIso_eq_degreeOfIsoTop).

Equations

• SphereOddDegree.degreeOfIsoTop e g = (SphereOddDegree.degreeRingHomOfIso (SphereOddDegree.sphereTopHomologyℤ n) e) ((SphereOddDegree.singularHomologyℤ n).map g)

@[simp]

theorem SphereOddDegree.degreeOfIsoTop_id {n : ℕ} (e : SphereTopHomologyIso n) : degreeOfIsoTop e (CategoryTheory.CategoryStruct.id (TopCat.sphere n)) = 1

The degree of the identity morphism is 1.

theorem SphereOddDegree.degreeOfIsoTop_comp {n : ℕ} (e : SphereTopHomologyIso n) (g h : TopCat.sphere n ⟶ TopCat.sphere n) : degreeOfIsoTop e (CategoryTheory.CategoryStruct.comp g h) = degreeOfIsoTop e h * degreeOfIsoTop e g

theorem SphereOddDegree.degreeOfIso_eq_degreeOfIsoTop {n : ℕ} (e : SphereTopHomologyIso n) (f : C(Sphere n, Sphere n)) : degreeOfIso e f = degreeOfIsoTop e (toTopCatSphereSelfMap f)

Compatibility with the raw Sphere n degree. The conditional degree degreeOfIso e f is exactly the TopCat-degree of the model transport of f.

theorem SphereOddDegree.degreeOfIsoTop_well_defined {n : ℕ} (e e' : SphereTopHomologyIso n) (g : TopCat.sphere n ⟶ TopCat.sphere n) : degreeOfIsoTop e g = degreeOfIsoTop e' g

Choice independence of the TopCat-degree: it does not depend on the chosen identification e.

Degree of one-point maps (n ≥ 1)

A single-valued self-map (ContinuousMap.const) of Sphere n factors through a one-point space, whose n-th homology vanishes for n ≥ 1 (it is totally disconnected). Hence the induced endomorphism of top homology is 0 and the degree is 0.

theorem SphereOddDegree.singularHomologyℤ_punit_isZero {n : ℕ} (hn : n ≠ 0) : CategoryTheory.Limits.IsZero ((singularHomologyℤ n).obj ↧PUnit.{1})

For n ≥ 1 the n-th integral singular homology of the one-point space PUnit is the zero object (a point is totally disconnected).

theorem SphereOddDegree.inducedOnTopHomology_const {n : ℕ} (hn : n ≠ 0) (c : Sphere n) : inducedOnTopHomology (ContinuousMap.const (Sphere n) c) = 0

The induced top-homology endomorphism of a one-point map is 0 (n ≥ 1). The single-valued self-map factors through the one-point space PUnit, and the induced map on Hₙ therefore factors through Hₙ(PUnit) = 0.

theorem SphereOddDegree.degreeOfIso_const {n : ℕ} (e : SphereTopHomologyIso n) (hn : n ≠ 0) (c : Sphere n) : degreeOfIso e (ContinuousMap.const (Sphere n) c) = 0

Degree of a one-point map is 0 for n ≥ 1.

Degree of homeomorphisms is a unit

If h is a self-homeomorphism then degree h · degree h⁻¹ = degree id = 1, so the degree is a unit of ℤ, i.e. ±1 (hence in particular odd).

theorem SphereOddDegree.degreeOfIso_homeomorph_mul_symm {n : ℕ} (e : SphereTopHomologyIso n) (h : Sphere n ≃ₜ Sphere n) : degreeOfIso e ↑h * degreeOfIso e ↑h.symm = 1

For a self-homeomorphism h, degree h * degree h⁻¹ = 1.

theorem SphereOddDegree.isUnit_degreeOfIso_homeomorph {n : ℕ} (e : SphereTopHomologyIso n) (h : Sphere n ≃ₜ Sphere n) : IsUnit (degreeOfIso e ↑h)

The degree of a self-homeomorphism is a unit of ℤ.

theorem SphereOddDegree.degreeOfIso_homeomorph_eq_one_or_neg_one {n : ℕ} (e : SphereTopHomologyIso n) (h : Sphere n ≃ₜ Sphere n) : degreeOfIso e ↑h = 1 ∨ degreeOfIso e ↑h = -1

The degree of a self-homeomorphism is ±1.

theorem SphereOddDegree.odd_degreeOfIso_homeomorph {n : ℕ} (e : SphereTopHomologyIso n) (h : Sphere n ≃ₜ Sphere n) : Odd (degreeOfIso e ↑h)

Parity wrapper. The degree of a self-homeomorphism is odd.

Degree of the antipodal map

theorem SphereOddDegree.degreeOfIso_antipodal_sq {n : ℕ} (e : SphereTopHomologyIso n) : degreeOfIso e (antipodal n) * degreeOfIso e (antipodal n) = 1

The square of the degree of the antipodal map is 1 (it is an involution).

theorem SphereOddDegree.degreeOfIso_antipodal_eq_one_or_neg_one {n : ℕ} (e : SphereTopHomologyIso n) : degreeOfIso e (antipodal n) = 1 ∨ degreeOfIso e (antipodal n) = -1

The degree of the antipodal map is ±1. Which sign occurs is (-1)^(n+1) after choosing the standard orientation identification Hₙ(Sⁿ;ℤ) ≅ ℤ (cf. det_ambientNeg).

Oriented-degree wrappers

The same facts repackaged on the bundled SphereOrientation.degree.

theorem SphereOddDegree.SphereOrientation.degree_const (o : SphereOrientation) {n : ℕ} (hn : n ≠ 0) (c : Sphere n) : o.degree (ContinuousMap.const (Sphere n) c) = 0

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

theorem SphereOddDegree.SphereOrientation.degree_homeomorph_eq_one_or_neg_one (o : SphereOrientation) {n : ℕ} (h : Sphere n ≃ₜ Sphere n) : o.degree ↑h = 1 ∨ o.degree ↑h = -1

The degree of a self-homeomorphism is ±1.

theorem SphereOddDegree.SphereOrientation.odd_degree_homeomorph (o : SphereOrientation) {n : ℕ} (h : Sphere n ≃ₜ Sphere n) : Odd (o.degree ↑h)

The degree of a self-homeomorphism is odd.

theorem SphereOddDegree.SphereOrientation.degree_antipodal_eq_one_or_neg_one (o : SphereOrientation) (n : ℕ) : o.degree (antipodal n) = 1 ∨ o.degree (antipodal n) = -1

The degree of the antipodal map is ±1.