Documentation

TauCeti.Analysis.Normed.Module.Ball.Action

Unit scalars acting on spheres #

Mathlib's Analysis.Normed.Module.Ball.Action, due to Yury Kudryashov and Heather Macbeth, lets the unit sphere of a normed field ๐•œ act on every sphere centred at zero in a normed ๐•œ-space. This file records that the underlying vector of this action is scalar multiplication.

Over a noncommutative normed ring, such as the quaternions, the natural scalar action on a coordinate space is often on the right. A right action of ๐•œ on F is a module structure over ๐•œแตแต’แต–, and when it multiplies norms, right multiplication by unit scalars preserves every sphere centred at zero. This file packages it as a continuous action of the opposite monoid (sphere (0 : ๐•œ) 1)แตแต’แต– on the sphere, the right-handed counterpart of Mathlib's action.

Main declarations #

source
@[simp]
theorem TauCeti.Sphere.coe_sphere_smul {๐•œ : Type u_1} {F : Type u_2} [NormedField ๐•œ] [SeminormedAddCommGroup F] [NormedSpace ๐•œ F] {r : โ„} (c : โ†‘(Metric.sphere 0 1)) (x : โ†‘(Metric.sphere 0 r)) :
โ†‘(c โ€ข x) = โ†‘c โ€ข โ†‘x

The coercion of Mathlib's action of the unit sphere of a normed field ๐•œ on a sphere of a normed ๐•œ-space is scalar multiplication in the ambient space.

source
@[instance_reducible]
instance TauCeti.Sphere.instSMulMulOpposite {๐•œ : Type u_1} {F : Type u_2} [SeminormedRing ๐•œ] [SeminormedAddCommGroup F] [Module ๐•œแตแต’แต– F] [NormSMulClass ๐•œแตแต’แต– F] {r : โ„} :
SMul (โ†‘(Metric.sphere 0 1))แตแต’แต– โ†‘(Metric.sphere 0 r)

Right multiplication by a unit scalar preserves every sphere centred at zero.

source
@[simp]
theorem TauCeti.Sphere.coe_op_sphere_smul {๐•œ : Type u_1} {F : Type u_2} [SeminormedRing ๐•œ] [SeminormedAddCommGroup F] [Module ๐•œแตแต’แต– F] [NormSMulClass ๐•œแตแต’แต– F] {r : โ„} (c : (โ†‘(Metric.sphere 0 1))แตแต’แต–) (x : โ†‘(Metric.sphere 0 r)) :
โ†‘(c โ€ข x) = MulOpposite.op โ†‘(MulOpposite.unop c) โ€ข โ†‘x

The right action of a unit scalar on a sphere is right scalar multiplication in the ambient space.

source
@[instance_reducible]
instance TauCeti.Sphere.instMulActionMulOpposite {๐•œ : Type u_1} {F : Type u_2} [SeminormedRing ๐•œ] [SeminormedAddCommGroup F] [Module ๐•œแตแต’แต– F] [NormSMulClass ๐•œแตแต’แต– F] {r : โ„} [NormMulClass ๐•œ] [NormOneClass ๐•œ] :
MulAction (โ†‘(Metric.sphere 0 1))แตแต’แต– โ†‘(Metric.sphere 0 r)

Unit scalars act on the right on every sphere centred at zero.

source
instance TauCeti.Sphere.instContinuousSMulMulOpposite {๐•œ : Type u_1} {F : Type u_2} [SeminormedRing ๐•œ] [SeminormedAddCommGroup F] [Module ๐•œแตแต’แต– F] [NormSMulClass ๐•œแตแต’แต– F] {r : โ„} :
ContinuousSMul (โ†‘(Metric.sphere 0 1))แตแต’แต– โ†‘(Metric.sphere 0 r)

The right action of unit scalars on a sphere centred at zero is continuous.