Basic sphere and odd-map interface

This file fixes a working model of the sphere and defines odd maps. The definitions here should eventually be aligned with whichever sphere API is most convenient for the full formalization, possibly TopCat.sphere n.

@[reducible, inline]

abbrev SphereOddDegree.Sphere (n : ℕ) : Type

A concrete model of S^n as the unit sphere in R^(n+1).

Equations

• SphereOddDegree.Sphere n = ↑(Metric.sphere 0 1)

def SphereOddDegree.IsOddMap {n : ℕ} (f : C(Sphere n, Sphere n)) : Prop

An odd map between spheres is equivariant for the antipodal map.

Equations

• SphereOddDegree.IsOddMap f = ∀ (x : SphereOddDegree.Sphere n), f (-x) = -f x

theorem SphereOddDegree.isOddMap_iff {n : ℕ} {f : C(Sphere n, Sphere n)} : IsOddMap f ↔ ∀ (x : Sphere n), f (-x) = -f x

IsOddMap f unfolds to the pointwise oddness condition f (-x) = - f x. This restatement is convenient for rw/simp even though it holds by rfl.