Degree of the antipodal map #

Proves parity and mod-two statements for the antipodal degree and identifies the bundled antipodal map with ambient negation. The exact integer formula degree(antipodal on Sⁿ) = (-1)^(n+1) is exposed conditionally through DegreeEqAmbientDet, the standard bridge from an orthogonal linear map to the sign of its determinant.

source

@[reducible, inline]

abbrev SphereOddDegree.ambientNeg (n : ℕ) :

EuclideanSpace ℝ (Fin (n + 1)) →ₗ[ℝ ] EuclideanSpace ℝ (Fin (n + 1))

The ambient antipodal linear map x ↦ -x on ℝ^(n+1), abbreviated. Its determinant is (-1)^(n+1) (det_ambientNeg).

Equations

SphereOddDegree.ambientNeg n = -LinearMap.id

Instances For

Parity of the target value `(-1)^(n+1)` #

source

theorem SphereOddDegree.odd_neg_one_pow_succ (n : ℕ) :

Odd ((-1) ^ (n + 1))

(-1)^(n+1) is odd (it is ±1).

source

theorem SphereOddDegree.neg_one_pow_succ_emod_two (n : ℕ) :

(-1) ^ (n + 1) % 2 = 1

(-1)^(n+1) ≡ 1 (mod 2).

source

theorem SphereOddDegree.neg_one_pow_succ_eq_one_or_neg_one (n : ℕ) :

(-1) ^ (n + 1) = 1 ∨ (-1) ^ (n + 1) = -1

(-1)^(n+1) is 1 or -1.

Compatibility of `antipodal` with the ambient negation #

source

theorem SphereOddDegree.antipodal_coe_eq_ambientNeg {n : ℕ} (x : Sphere n) :

↑((antipodal n) x) = (ambientNeg n) ↑x

Compatibility with ambient negation. The bundled antipodal self-map antipodal n is the restriction to the unit sphere of the ambient linear map -LinearMap.id: on underlying vectors, ↑(antipodal n x) = (-LinearMap.id) ↑x. This is the precise sense in which the orientation sign det_ambientNeg = (-1)^(n+1) governs the antipodal map.

Parity of the antipodal degree (unconditional given `e`) #

source

theorem SphereOddDegree.odd_degreeOfIso_antipodal {n : ℕ} (e : SphereTopHomologyIso n) :

Odd (degreeOfIso e (antipodal n))

The degree of the antipodal map is odd (relative to any chosen identification e : Hₙ(Sⁿ;ℤ) ≅ ℤ). This is the parity consequence of degree (antipodal n) = (-1)^(n+1), and it holds unconditionally on the sign: the antipodal map is a self-homeomorphism, so its degree is ±1, hence odd.

source

theorem SphereOddDegree.degreeOfIso_antipodal_emod_two {n : ℕ} (e : SphereTopHomologyIso n) :

degreeOfIso e (antipodal n) % 2 = 1

The degree of the antipodal map is ≡ 1 (mod 2) (relative to any chosen e). This is the parity statement degree(antipodal) ≡ 1 mod 2 expressed as an integer remainder statement.

source

theorem SphereOddDegree.degreeOfIso_antipodal_emod_two_eq_neg_one_pow {n : ℕ} (e : SphereTopHomologyIso n) :

degreeOfIso e (antipodal n) % 2 = (-1) ^ (n + 1) % 2

Mod-2 agreement with the target value. The degree of the antipodal map agrees with (-1)^(n+1) modulo 2: both are odd. This is the parity content of the full degree theorem, available now without the orientation sign.

Conditional full theorem: degree = determinant sign ⇒ `(-1)^(n+1)` #

The value is derived from the topological bridge "degree of a linear sphere map = sign of its ambient determinant", expressed here as an explicit hypothesis.

source

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

Prop

The hypothesis that the antipodal degree equals the determinant of its ambient linear map -LinearMap.id. This specializes the linear-sphere-map degree formula to the antipodal map.

Equations

SphereOddDegree.DegreeEqAmbientDet e = (↑(SphereOddDegree.degreeOfIso e (SphereOddDegree.antipodal n)) = LinearMap.det (SphereOddDegree.ambientNeg n))

Instances For

source

theorem SphereOddDegree.degreeOfIso_antipodal_eq_neg_one_pow_of_eq_det {n : ℕ} (e : SphereTopHomologyIso n) (h : DegreeEqAmbientDet e) :

degreeOfIso e (antipodal n) = (-1) ^ (n + 1)

Conditional antipodal-degree theorem. If the degree of the antipodal map equals the determinant of its ambient linear map (DegreeEqAmbientDet), then degree (antipodal n) = (-1)^(n+1). The proof simply rewrites with the genuine ambient determinant fact det_ambientNeg.