# 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`.

### Algebraic structures on `Metric.ball 0 1` #

source
def Subsemigroup.unitBall (𝕜 : Type u_2) [NonUnitalSeminormedRing 𝕜] :
Subsemigroup 𝕜

Unit ball in a non-unital seminormed ring as a bundled `Subsemigroup`.

Equations

- Subsemigroup.unitBall 𝕜 = { carrier := Metric.ball 0 1, mul_mem' := ⋯ }

Instances For

source
instance Metric.unitBall.instSemigroup {𝕜 : Type u_1} [NonUnitalSeminormedRing 𝕜] :
Semigroup ↑(ball 0 1)
Equations

- Metric.unitBall.instSemigroup = MulMemClass.toSemigroup (Subsemigroup.unitBall 𝕜)

source
instance Metric.unitBall.instContinuousMul {𝕜 : Type u_1} [NonUnitalSeminormedRing 𝕜] :
ContinuousMul ↑(ball 0 1)
source
instance Metric.unitBall.instCommSemigroup {𝕜 : Type u_1} [SeminormedCommRing 𝕜] :
CommSemigroup ↑(ball 0 1)
Equations

- Metric.unitBall.instCommSemigroup = MulMemClass.toCommSemigroup (Subsemigroup.unitBall 𝕜)

source
instance Metric.unitBall.instHasDistribNeg {𝕜 : Type u_1} [NonUnitalSeminormedRing 𝕜] :
HasDistribNeg ↑(ball 0 1)
Equations

- Metric.unitBall.instHasDistribNeg = Function.Injective.hasDistribNeg Subtype.val ⋯ ⋯ ⋯

source
@[simp]
theorem Metric.unitBall.coe_mul {𝕜 : Type u_1} [NonUnitalSeminormedRing 𝕜] (x y : ↑(ball 0 1)) :
↑(x * y) = ↑x * ↑y
source
instance Metric.unitBall.instZero {𝕜 : Type u_1} [Zero 𝕜] [PseudoMetricSpace 𝕜] :
Zero ↑(ball 0 1)
Equations

- Metric.unitBall.instZero = { zero := ⟨0, ⋯⟩ }

source
@[simp]
theorem Metric.unitBall.coe_zero {𝕜 : Type u_1} [Zero 𝕜] [PseudoMetricSpace 𝕜] :
↑0 = 0
source
@[simp]
theorem Metric.unitBall.coe_eq_zero {𝕜 : Type u_1} [Zero 𝕜] [PseudoMetricSpace 𝕜] {a : ↑(ball 0 1)} :
↑a = 0 ↔ a = 0
source
instance Metric.unitBall.instSemigroupWithZero {𝕜 : Type u_1} [NonUnitalSeminormedRing 𝕜] :
SemigroupWithZero ↑(ball 0 1)
Equations

- Metric.unitBall.instSemigroupWithZero = { toSemigroup := Metric.unitBall.instSemigroup, toZero := Metric.unitBall.instZero, zero_mul := ⋯, mul_zero := ⋯ }

source
instance Metric.unitBall.instIsLeftCancelMulZero {𝕜 : Type u_1} [NonUnitalSeminormedRing 𝕜] [IsLeftCancelMulZero 𝕜] :
IsLeftCancelMulZero ↑(ball 0 1)
source
instance Metric.unitBall.instIsRightCancelMulZero {𝕜 : Type u_1} [NonUnitalSeminormedRing 𝕜] [IsRightCancelMulZero 𝕜] :
IsRightCancelMulZero ↑(ball 0 1)
source
instance Metric.unitBall.instIsCancelMulZero {𝕜 : Type u_1} [NonUnitalSeminormedRing 𝕜] [IsCancelMulZero 𝕜] :
IsCancelMulZero ↑(ball 0 1)

### Algebraic instances for `Metric.closedBall 0 1` #

source
def Subsemigroup.unitClosedBall (𝕜 : Type u_2) [NonUnitalSeminormedRing 𝕜] :
Subsemigroup 𝕜

Closed unit ball in a non-unital seminormed ring as a bundled `Subsemigroup`.

Equations

- Subsemigroup.unitClosedBall 𝕜 = { carrier := Metric.closedBall 0 1, mul_mem' := ⋯ }

Instances For

source
instance Metric.unitClosedBall.instSemigroup {𝕜 : Type u_1} [NonUnitalSeminormedRing 𝕜] :
Semigroup ↑(closedBall 0 1)
Equations

- Metric.unitClosedBall.instSemigroup = MulMemClass.toSemigroup (Subsemigroup.unitClosedBall 𝕜)

source
instance Metric.unitClosedBall.instHasDistribNeg {𝕜 : Type u_1} [NonUnitalSeminormedRing 𝕜] :
HasDistribNeg ↑(closedBall 0 1)
Equations

- Metric.unitClosedBall.instHasDistribNeg = Function.Injective.hasDistribNeg Subtype.val ⋯ ⋯ ⋯

source
instance Metric.unitClosedBall.instContinuousMul {𝕜 : Type u_1} [NonUnitalSeminormedRing 𝕜] :
ContinuousMul ↑(closedBall 0 1)
source
@[simp]
theorem Metric.unitClosedBall.coe_mul {𝕜 : Type u_1} [NonUnitalSeminormedRing 𝕜] (x y : ↑(closedBall 0 1)) :
↑(x * y) = ↑x * ↑y
source
instance Metric.unitClosedBall.instZero {𝕜 : Type u_1} [Zero 𝕜] [PseudoMetricSpace 𝕜] :
Zero ↑(closedBall 0 1)
Equations

- Metric.unitClosedBall.instZero = { zero := ⟨0, ⋯⟩ }

source
@[simp]
theorem Metric.unitClosedBall.coe_zero {𝕜 : Type u_1} [Zero 𝕜] [PseudoMetricSpace 𝕜] :
↑0 = 0
source
@[simp]
theorem Metric.unitClosedBall.coe_eq_zero {𝕜 : Type u_1} [Zero 𝕜] [PseudoMetricSpace 𝕜] {a : ↑(closedBall 0 1)} :
↑a = 0 ↔ a = 0
source
instance Metric.unitClosedBall.instSemigroupWithZero {𝕜 : Type u_1} [NonUnitalSeminormedRing 𝕜] :
SemigroupWithZero ↑(closedBall 0 1)
Equations

- Metric.unitClosedBall.instSemigroupWithZero = { toSemigroup := Metric.unitClosedBall.instSemigroup, toZero := Metric.unitClosedBall.instZero, zero_mul := ⋯, mul_zero := ⋯ }

source
def Submonoid.unitClosedBall (𝕜 : Type u_2) [SeminormedRing 𝕜] [NormOneClass 𝕜] :
Submonoid 𝕜

Closed unit ball in a seminormed ring as a bundled `Submonoid`.

Equations

- Submonoid.unitClosedBall 𝕜 = { carrier := Metric.closedBall 0 1, mul_mem' := ⋯, one_mem' := ⋯ }

Instances For

source
instance Metric.unitClosedBall.instMonoid {𝕜 : Type u_1} [SeminormedRing 𝕜] [NormOneClass 𝕜] :
Monoid ↑(closedBall 0 1)
Equations

- Metric.unitClosedBall.instMonoid = SubmonoidClass.toMonoid (Submonoid.unitClosedBall 𝕜)

source
instance Metric.unitClosedBall.instCommMonoid {𝕜 : Type u_1} [SeminormedCommRing 𝕜] [NormOneClass 𝕜] :
CommMonoid ↑(closedBall 0 1)
Equations

- Metric.unitClosedBall.instCommMonoid = SubmonoidClass.toCommMonoid (Submonoid.unitClosedBall 𝕜)

source
@[simp]
theorem Metric.unitClosedBall.coe_one {𝕜 : Type u_1} [SeminormedRing 𝕜] [NormOneClass 𝕜] :
↑1 = 1
source
@[simp]
theorem Metric.unitClosedBall.coe_eq_one {𝕜 : Type u_1} [SeminormedRing 𝕜] [NormOneClass 𝕜] {a : ↑(closedBall 0 1)} :
↑a = 1 ↔ a = 1
source
@[simp]
theorem Metric.unitClosedBall.coe_pow {𝕜 : Type u_1} [SeminormedRing 𝕜] [NormOneClass 𝕜] (x : ↑(closedBall 0 1)) (n : ℕ) :
↑(x ^ n) = ↑x ^ n
source
instance Metric.unitClosedBall.instMonoidWithZero {𝕜 : Type u_1} [SeminormedRing 𝕜] [NormOneClass 𝕜] :
MonoidWithZero ↑(closedBall 0 1)
Equations

- Metric.unitClosedBall.instMonoidWithZero = { toMonoid := Metric.unitClosedBall.instMonoid, toZero := Metric.unitClosedBall.instSemigroupWithZero.toZero, zero_mul := ⋯, mul_zero := ⋯ }

source
instance Metric.unitClosedBall.instCancelMonoidWithZero {𝕜 : Type u_1} [SeminormedRing 𝕜] [IsCancelMulZero 𝕜] [NormOneClass 𝕜] :
CancelMonoidWithZero ↑(closedBall 0 1)
Equations

- Metric.unitClosedBall.instCancelMonoidWithZero = { toMonoidWithZero := Metric.unitClosedBall.instMonoidWithZero, toIsCancelMulZero := ⋯ }

### Algebraic instances on the unit sphere #

source
def Submonoid.unitSphere (𝕜 : Type u_2) [SeminormedRing 𝕜] [NormMulClass 𝕜] [NormOneClass 𝕜] :
Submonoid 𝕜

Unit sphere in a seminormed ring (with strictly multiplicative norm) as a bundled `Submonoid`.

Equations

- Submonoid.unitSphere 𝕜 = { carrier := Metric.sphere 0 1, mul_mem' := ⋯, one_mem' := ⋯ }

Instances For

source
@[simp]
theorem Submonoid.coe_unitSphere (𝕜 : Type u_2) [SeminormedRing 𝕜] [NormMulClass 𝕜] [NormOneClass 𝕜] :
↑(unitSphere 𝕜) = Metric.sphere 0 1
source
instance Metric.unitSphere.instInv {𝕜 : Type u_1} [NormedDivisionRing 𝕜] :
Inv ↑(sphere 0 1)
Equations

- Metric.unitSphere.instInv = { inv := fun (x : ↑(Metric.sphere 0 1)) => ⟨(↑x)⁻¹, ⋯⟩ }

source
@[simp]
theorem Metric.unitSphere.coe_inv {𝕜 : Type u_1} [NormedDivisionRing 𝕜] (x : ↑(sphere 0 1)) :
↑x⁻¹ = (↑x)⁻¹
source
instance Metric.unitSphere.instDiv {𝕜 : Type u_1} [NormedDivisionRing 𝕜] :
Div ↑(sphere 0 1)
Equations

- Metric.unitSphere.instDiv = { div := fun (x y : ↑(Metric.sphere 0 1)) => ⟨↑x / ↑y, ⋯⟩ }

source
@[simp]
theorem Metric.unitSphere.coe_div {𝕜 : Type u_1} [NormedDivisionRing 𝕜] (x y : ↑(sphere 0 1)) :
↑(x / y) = ↑x / ↑y
source
instance Metric.unitSphere.instZPow {𝕜 : Type u_1} [NormedDivisionRing 𝕜] :
Pow ↑(sphere 0 1) ℤ
Equations

- Metric.unitSphere.instZPow = { pow := fun (x : ↑(Metric.sphere 0 1)) (n : ℤ) => ⟨↑x ^ n, ⋯⟩ }

source
@[simp]
theorem Metric.unitSphere.coe_zpow {𝕜 : Type u_1} [NormedDivisionRing 𝕜] (x : ↑(sphere 0 1)) (n : ℤ) :
↑(x ^ n) = ↑x ^ n
source
instance Metric.unitSphere.instMonoid {𝕜 : Type u_1} [SeminormedRing 𝕜] [NormMulClass 𝕜] [NormOneClass 𝕜] :
Monoid ↑(sphere 0 1)
Equations

- Metric.unitSphere.instMonoid = SubmonoidClass.toMonoid (Submonoid.unitSphere 𝕜)

source
instance Metric.unitSphere.instCommMonoid {𝕜 : Type u_1} [SeminormedCommRing 𝕜] [NormMulClass 𝕜] [NormOneClass 𝕜] :
CommMonoid ↑(sphere 0 1)
Equations

- Metric.unitSphere.instCommMonoid = SubmonoidClass.toCommMonoid (Submonoid.unitSphere 𝕜)

source
@[simp]
theorem Metric.unitSphere.coe_one {𝕜 : Type u_1} [SeminormedRing 𝕜] [NormMulClass 𝕜] [NormOneClass 𝕜] :
↑1 = 1
source
@[simp]
theorem Metric.unitSphere.coe_mul {𝕜 : Type u_1} [SeminormedRing 𝕜] [NormMulClass 𝕜] [NormOneClass 𝕜] (x y : ↑(sphere 0 1)) :
↑(x * y) = ↑x * ↑y
source
@[simp]
theorem Metric.unitSphere.coe_pow {𝕜 : Type u_1} [SeminormedRing 𝕜] [NormMulClass 𝕜] [NormOneClass 𝕜] (x : ↑(sphere 0 1)) (n : ℕ) :
↑(x ^ n) = ↑x ^ n
source
def unitSphereToUnits (𝕜 : Type u_2) [NormedDivisionRing 𝕜] :
↑(Metric.sphere 0 1) →* 𝕜 ˣ

Monoid homomorphism from the unit sphere in a normed division ring to the group of units.

Equations

- unitSphereToUnits 𝕜 = Units.liftRight (Submonoid.unitSphere 𝕜).subtype (fun (x : ↑(Metric.sphere 0 1)) => Units.mk0 ↑x ⋯) ⋯

Instances For

source
@[simp]
theorem unitSphereToUnits_apply_coe {𝕜 : Type u_1} [NormedDivisionRing 𝕜] (x : ↑(Metric.sphere 0 1)) :
↑((unitSphereToUnits 𝕜) x) = ↑x
source
theorem unitSphereToUnits_injective {𝕜 : Type u_1} [NormedDivisionRing 𝕜] :
Function.Injective ⇑(unitSphereToUnits 𝕜)
source
instance Metric.unitSphere.instGroup {𝕜 : Type u_1} [NormedDivisionRing 𝕜] :
Group ↑(sphere 0 1)
Equations

- Metric.unitSphere.instGroup = Function.Injective.group ⇑(unitSphereToUnits 𝕜) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

source
instance Metric.sphere.instHasDistribNeg {𝕜 : Type u_1} [SeminormedRing 𝕜] [NormMulClass 𝕜] [NormOneClass 𝕜] :
HasDistribNeg ↑(sphere 0 1)
Equations

- Metric.sphere.instHasDistribNeg = Function.Injective.hasDistribNeg Subtype.val ⋯ ⋯ ⋯

source
instance Metric.sphere.instContinuousMul {𝕜 : Type u_1} [SeminormedRing 𝕜] [NormMulClass 𝕜] [NormOneClass 𝕜] :
ContinuousMul ↑(sphere 0 1)
source
instance Metric.sphere.instIsTopologicalGroup {𝕜 : Type u_1} [NormedDivisionRing 𝕜] :
IsTopologicalGroup ↑(sphere 0 1)
source
instance Metric.sphere.instCommGroup {𝕜 : Type u_1} [NormedField 𝕜] :
CommGroup ↑(sphere 0 1)
Equations

- Metric.sphere.instCommGroup = { toGroup := Metric.unitSphere.instGroup, mul_comm := ⋯ }