# Algebraic structures on unit balls and spheres #

In this file we define algebraic structures (Semigroup, CommSemigroup, Monoid, CommMonoid, Group, CommGroup) on Metric.ball (0 : ๐) 1, Metric.closedBall (0 : ๐) 1, and Metric.sphere (0 : ๐) 1. In each case we use the weakest possible typeclass assumption on ๐, from NonUnitalSeminormedRing to NormedField.

def Subsemigroup.unitBall (๐ : Type u_2) [] :
Subsemigroup ๐

Unit ball in a non unital semi normed ring as a bundled Subsemigroup.

Equations
• = { carrier := , mul_mem' := โฏ }
Instances For
instance Metric.unitBall.semigroup {๐ : Type u_1} [] :
Semigroup โ()
Equations
• Metric.unitBall.semigroup =
instance Metric.unitBall.continuousMul {๐ : Type u_1} [] :
ContinuousMul โ()
Equations
• โฏ = โฏ
instance Metric.unitBall.commSemigroup {๐ : Type u_1} [] :
CommSemigroup โ()
Equations
• Metric.unitBall.commSemigroup =
instance Metric.unitBall.hasDistribNeg {๐ : Type u_1} [] :
HasDistribNeg โ()
Equations
@[simp]
theorem coe_mul_unitBall {๐ : Type u_1} [] (x : โ()) (y : โ()) :
โ(x * y) = โx * โy
def Subsemigroup.unitClosedBall (๐ : Type u_2) [] :
Subsemigroup ๐

Closed unit ball in a non unital semi normed ring as a bundled Subsemigroup.

Equations
• = { carrier := , mul_mem' := โฏ }
Instances For
instance Metric.unitClosedBall.semigroup {๐ : Type u_1} [] :
Semigroup โ()
Equations
• Metric.unitClosedBall.semigroup =
instance Metric.unitClosedBall.hasDistribNeg {๐ : Type u_1} [] :
HasDistribNeg โ()
Equations
instance Metric.unitClosedBall.continuousMul {๐ : Type u_1} [] :
ContinuousMul โ()
Equations
• โฏ = โฏ
@[simp]
theorem coe_mul_unitClosedBall {๐ : Type u_1} [] (x : โ()) (y : โ()) :
โ(x * y) = โx * โy
def Submonoid.unitClosedBall (๐ : Type u_2) [SeminormedRing ๐] [NormOneClass ๐] :
Submonoid ๐

Closed unit ball in a semi normed ring as a bundled Submonoid.

Equations
• = let __src := ; { carrier := , mul_mem' := โฏ, one_mem' := โฏ }
Instances For
instance Metric.unitClosedBall.monoid {๐ : Type u_1} [SeminormedRing ๐] [NormOneClass ๐] :
Monoid โ()
Equations
• Metric.unitClosedBall.monoid =
instance Metric.unitClosedBall.commMonoid {๐ : Type u_1} [] [NormOneClass ๐] :
CommMonoid โ()
Equations
• Metric.unitClosedBall.commMonoid =
@[simp]
theorem coe_one_unitClosedBall {๐ : Type u_1} [SeminormedRing ๐] [NormOneClass ๐] :
โ1 = 1
@[simp]
theorem coe_pow_unitClosedBall {๐ : Type u_1} [SeminormedRing ๐] [NormOneClass ๐] (x : โ()) (n : โ) :
โ(x ^ n) = โx ^ n
def Submonoid.unitSphere (๐ : Type u_2) [] :
Submonoid ๐

Unit sphere in a normed division ring as a bundled Submonoid.

Equations
• = { carrier := , mul_mem' := โฏ, one_mem' := โฏ }
Instances For
instance Metric.unitSphere.inv {๐ : Type u_1} [] :
Inv โ()
Equations
• Metric.unitSphere.inv = { inv := fun (x : โ()) => โจ(โx)โปยน, โฏโฉ }
@[simp]
theorem coe_inv_unitSphere {๐ : Type u_1} [] (x : โ()) :
โ = (โx)โปยน
instance Metric.unitSphere.div {๐ : Type u_1} [] :
Div โ()
Equations
• Metric.unitSphere.div = { div := fun (x y : โ()) => โจโx / โy, โฏโฉ }
@[simp]
theorem coe_div_unitSphere {๐ : Type u_1} [] (x : โ()) (y : โ()) :
โ(x / y) = โx / โy
instance Metric.unitSphere.pow {๐ : Type u_1} [] :
Pow โ() โค
Equations
• Metric.unitSphere.pow = { pow := fun (x : โ()) (n : โค) => โจโx ^ n, โฏโฉ }
@[simp]
theorem coe_zpow_unitSphere {๐ : Type u_1} [] (x : โ()) (n : โค) :
โ(x ^ n) = โx ^ n
instance Metric.unitSphere.monoid {๐ : Type u_1} [] :
Monoid โ()
Equations
• Metric.unitSphere.monoid =
@[simp]
theorem coe_one_unitSphere {๐ : Type u_1} [] :
โ1 = 1
@[simp]
theorem coe_mul_unitSphere {๐ : Type u_1} [] (x : โ()) (y : โ()) :
โ(x * y) = โx * โy
@[simp]
theorem coe_pow_unitSphere {๐ : Type u_1} [] (x : โ()) (n : โ) :
โ(x ^ n) = โx ^ n
def unitSphereToUnits (๐ : Type u_2) [] :
โ() โ* ๐หฃ

Monoid homomorphism from the unit sphere to the group of units.

Equations
Instances For
@[simp]
theorem unitSphereToUnits_apply_coe {๐ : Type u_1} [] (x : โ()) :
โ(() x) = โx
theorem unitSphereToUnits_injective {๐ : Type u_1} [] :
instance Metric.sphere.group {๐ : Type u_1} [] :
Group โ()
Equations
instance Metric.sphere.hasDistribNeg {๐ : Type u_1} [] :
HasDistribNeg โ()
Equations
instance Metric.sphere.topologicalGroup {๐ : Type u_1} [] :
Equations
• โฏ = โฏ
instance Metric.sphere.commGroup {๐ : Type u_1} [NormedField ๐] :
CommGroup โ()
Equations