The integer-unit action on real spheres

The two units of the integers act on every sphere in a real seminormed space by the identity and the antipodal map. This file restricts Mathlib's scalar action on spheres to that action, proves its basic coercion rules and continuity, and shows that the action on every nonzero-radius sphere is free.

The scalar action on spheres and ne_neg_of_mem_sphere are from Mathlib's Analysis.Normed.Module.Ball.Action, due to Yury Kudryashov and Heather Macbeth.

Main declarations

• TauCeti.Sphere.instMulActionIntUnitsSphere: the action of ℤˣ on a real sphere.
• TauCeti.Sphere.instContinuousConstSMulIntUnitsSphere: continuity of the action.
• TauCeti.Sphere.instIsCancelSMulIntUnitsSphere: freeness on every nonzero-radius sphere.

def TauCeti.Sphere.intUnitsToUnitSphere : ℤˣ →* ↑(Metric.sphere 0 1)

The homomorphism that regards an integer unit as a real scalar of norm one.

Equations

• TauCeti.Sphere.intUnitsToUnitSphere = { toFun := fun (u : ℤˣ) => ⟨↑↑u, ⋯⟩, map_one' := TauCeti.Sphere.intUnitsToUnitSphere._proof_5✝, map_mul' := TauCeti.Sphere.intUnitsToUnitSphere._proof_7✝ }

@[simp]

theorem TauCeti.Sphere.coe_intUnitsToUnitSphere (u : ℤˣ) : ↑(intUnitsToUnitSphere u) = ↑↑u

An integer unit, regarded as a unit-norm real scalar, has the expected underlying value.

@[instance_reducible]

noncomputable instance TauCeti.Sphere.instMulActionIntUnitsSphere {E : Type u} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {r : ℝ} : MulAction ℤˣ ↑(Metric.sphere 0 r)

The two integer units act on every sphere centred at zero by the identity and the antipodal map.

Equations

• TauCeti.Sphere.instMulActionIntUnitsSphere = MulAction.compHom (↑(Metric.sphere 0 r)) TauCeti.Sphere.intUnitsToUnitSphere

@[simp]

theorem TauCeti.Sphere.coe_intUnits_smul {E : Type u} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {r : ℝ} (u : ℤˣ) (x : ↑(Metric.sphere 0 r)) : ↑(u • x) = ↑↑u • ↑x

The underlying vector of the integer-unit action is multiplication by the corresponding integer.

@[simp]

theorem TauCeti.Sphere.neg_one_smul {E : Type u} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {r : ℝ} (x : ↑(Metric.sphere 0 r)) : -1 • x = -x

The nontrivial integer unit acts on a sphere as the antipodal map.

instance TauCeti.Sphere.instContinuousConstSMulIntUnitsSphere {E : Type u} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {r : ℝ} : ContinuousConstSMul ℤˣ ↑(Metric.sphere 0 r)

The integer-unit action on a sphere is continuous in the sphere variable.

instance TauCeti.Sphere.instIsCancelSMulIntUnitsSphere {E : Type u} [SeminormedAddCommGroup E] [NormedSpace ℝ E] {r : ℝ} [NeZero r] : IsCancelSMul ℤˣ ↑(Metric.sphere 0 r)

The antipodal integer-unit action on every nonzero-radius sphere is free.