Antipodal map API

This file packages the antipodal involution on the concrete sphere model as a bundled continuous self-map and proves the basic lemmas about composition of odd maps.

This file is part of the point-set foundation layer; it depends only on the sphere model in Basic.lean and the normed-ball action API. The orientation/determinant facts about the ambient linear map x ↦ -x (which belong to the topological-degree support layer, not the point-set foundation) live in Degree.lean.

noncomputable def SphereOddDegree.antipodal (n : ℕ) : C(Sphere n, Sphere n)

The antipodal map on S^n, bundled as a continuous self-map.

Equations

• SphereOddDegree.antipodal n = { toFun := fun (x : SphereOddDegree.Sphere n) => -x, continuous_toFun := ⋯ }

@[simp]

theorem SphereOddDegree.antipodal_apply {n : ℕ} (x : Sphere n) : (antipodal n) x = -x

theorem SphereOddDegree.antipodal_ne_self {n : ℕ} (x : Sphere n) : -x ≠ x

The antipodal map is fixed-point free on the sphere: -x ≠ x.

This is the canonical fixed-point-free fact and the sphere-level API (it does not mention the projective quotient), so it lives here next to the antipodal map rather than in the covering-space file. The reversed orientation x ≠ -x is ne_neg_self.

theorem SphereOddDegree.ne_neg_self {n : ℕ} (x : Sphere n) : x ≠ -x

The antipodal map is fixed-point free on the sphere, reversed orientation: x ≠ -x. This is the .symm of the canonical antipodal_ne_self; it is the orientation consumed by Set.ncard_pair/Set.encard_pair on the fibers of the double cover.

theorem SphereOddDegree.antipodal_involutive (n : ℕ) : Function.Involutive ⇑(antipodal n)

The antipodal map is an involution, pointwise.

@[simp]

theorem SphereOddDegree.antipodal_comp_antipodal (n : ℕ) : (antipodal n).comp (antipodal n) = ContinuousMap.id (Sphere n)

The antipodal map composed with itself is the identity.

noncomputable def SphereOddDegree.antipodalHomeomorph (n : ℕ) : Sphere n ≃ₜ Sphere n

The antipodal map as a self-homeomorphism of the sphere. It is its own inverse, since the antipodal map is an involution.

Equations

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

@[simp]

theorem SphereOddDegree.antipodalHomeomorph_apply {n : ℕ} (x : Sphere n) : (antipodalHomeomorph n) x = -x

@[simp]

theorem SphereOddDegree.antipodalHomeomorph_symm (n : ℕ) : (antipodalHomeomorph n).symm = antipodalHomeomorph n

theorem SphereOddDegree.antipodal_bijective (n : ℕ) : Function.Bijective ⇑(antipodal n)

The antipodal map is bijective.

theorem SphereOddDegree.antipodal_injective (n : ℕ) : Function.Injective ⇑(antipodal n)

The antipodal map is injective.

theorem SphereOddDegree.antipodal_surjective (n : ℕ) : Function.Surjective ⇑(antipodal n)

The antipodal map is surjective.

theorem SphereOddDegree.antipodal_isHomeomorph (n : ℕ) : IsHomeomorph ⇑(antipodal n)

The antipodal map is a homeomorphism.

theorem SphereOddDegree.isOddMap_id (n : ℕ) : IsOddMap (ContinuousMap.id (Sphere n))

The identity map is odd.

theorem SphereOddDegree.isOddMap_antipodal (n : ℕ) : IsOddMap (antipodal n)

The antipodal map itself is odd.

theorem SphereOddDegree.IsOddMap.apply_neg {n : ℕ} {f : C(Sphere n, Sphere n)} (hf : IsOddMap f) (x : Sphere n) : f (-x) = -f x

Pointwise rewrite for an odd map on a negated argument: f (-x) = - f x. This is the defining property IsOddMap, repackaged for dot notation so that rw [hf.apply_neg] is available at use sites.

theorem SphereOddDegree.IsOddMap.comp {n : ℕ} {f g : C(Sphere n, Sphere n)} (hg : IsOddMap g) (hf : IsOddMap f) : IsOddMap (g.comp f)

Composition of odd maps is odd.

theorem SphereOddDegree.isOddMap_iff_comp_antipodal {n : ℕ} {f : C(Sphere n, Sphere n)} : IsOddMap f ↔ f.comp (antipodal n) = (antipodal n).comp f

Oddness is equivalent to commuting with the bundled antipodal map.

theorem SphereOddDegree.IsOddMap.map_antipodal {n : ℕ} {f : C(Sphere n, Sphere n)} (hf : IsOddMap f) (x : Sphere n) : f ((antipodal n) x) = (antipodal n) (f x)

Pointwise commutation of an odd map with the bundled antipodal map: f (antipodal n x) = antipodal n (f x). This is the definition IsOddMap restated through the bundled antipodal n map, convenient for rw/simp when the surrounding context is phrased with antipodal n rather than raw negation.

theorem SphereOddDegree.IsOddMap.comp_antipodal_eq {n : ℕ} {f : C(Sphere n, Sphere n)} (hf : IsOddMap f) : f.comp (antipodal n) = (antipodal n).comp f

Forward direction of isOddMap_iff_comp_antipodal, packaged for dot notation: an odd map commutes with the bundled antipodal map. Using hf.comp_antipodal_eq is more convenient than isOddMap_iff_comp_antipodal.mp hf at use sites.