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.

source

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

Subsemigroup 𝕜

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

Equations

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

source

instance Metric.unitBall.semigroup {𝕜 : Type u_1} [NonUnitalSeminormedRing 𝕜] :

Semigroup ↑(Metric.ball 0 1)

Equations

Metric.unitBall.semigroup = MulMemClass.toSemigroup (Subsemigroup.unitBall 𝕜)

source

instance Metric.unitBall.continuousMul {𝕜 : Type u_1} [NonUnitalSeminormedRing 𝕜] :

ContinuousMul ↑(Metric.ball 0 1)

Equations

⋯ = ⋯

source

instance Metric.unitBall.commSemigroup {𝕜 : Type u_1} [SeminormedCommRing 𝕜] :

CommSemigroup ↑(Metric.ball 0 1)

Equations

Metric.unitBall.commSemigroup = MulMemClass.toCommSemigroup (Subsemigroup.unitBall 𝕜)

source

instance Metric.unitBall.hasDistribNeg {𝕜 : Type u_1} [NonUnitalSeminormedRing 𝕜] :

HasDistribNeg ↑(Metric.ball 0 1)

Equations

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

source

@[simp]

theorem coe_mul_unitBall {𝕜 : Type u_1} [NonUnitalSeminormedRing 𝕜] (x : ↑(Metric.ball 0 1)) (y : ↑(Metric.ball 0 1)) :

↑(x * y) = ↑x * ↑y

source

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

Subsemigroup 𝕜

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

Equations

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

source

instance Metric.unitClosedBall.semigroup {𝕜 : Type u_1} [NonUnitalSeminormedRing 𝕜] :

Semigroup ↑(Metric.closedBall 0 1)

Equations

Metric.unitClosedBall.semigroup = MulMemClass.toSemigroup (Subsemigroup.unitClosedBall 𝕜)

source

instance Metric.unitClosedBall.hasDistribNeg {𝕜 : Type u_1} [NonUnitalSeminormedRing 𝕜] :

HasDistribNeg ↑(Metric.closedBall 0 1)

Equations

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

source

instance Metric.unitClosedBall.continuousMul {𝕜 : Type u_1} [NonUnitalSeminormedRing 𝕜] :

ContinuousMul ↑(Metric.closedBall 0 1)

Equations

⋯ = ⋯

source

@[simp]

theorem coe_mul_unitClosedBall {𝕜 : Type u_1} [NonUnitalSeminormedRing 𝕜] (x : ↑(Metric.closedBall 0 1)) (y : ↑(Metric.closedBall 0 1)) :

↑(x * y) = ↑x * ↑y

source

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

Submonoid 𝕜

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

Equations

Submonoid.unitClosedBall 𝕜 = let __src := Subsemigroup.unitClosedBall 𝕜; { toSubsemigroup := { carrier := Metric.closedBall 0 1, mul_mem' := ⋯ }, one_mem' := ⋯ }

source

instance Metric.unitClosedBall.monoid {𝕜 : Type u_1} [SeminormedRing 𝕜] [NormOneClass 𝕜] :

Monoid ↑(Metric.closedBall 0 1)

Equations

Metric.unitClosedBall.monoid = SubmonoidClass.toMonoid (Submonoid.unitClosedBall 𝕜)

source

instance Metric.unitClosedBall.commMonoid {𝕜 : Type u_1} [SeminormedCommRing 𝕜] [NormOneClass 𝕜] :

CommMonoid ↑(Metric.closedBall 0 1)

Equations

Metric.unitClosedBall.commMonoid = SubmonoidClass.toCommMonoid (Submonoid.unitClosedBall 𝕜)

source

@[simp]

theorem coe_one_unitClosedBall {𝕜 : Type u_1} [SeminormedRing 𝕜] [NormOneClass 𝕜] :

↑1 = 1

source

@[simp]

theorem coe_pow_unitClosedBall {𝕜 : Type u_1} [SeminormedRing 𝕜] [NormOneClass 𝕜] (x : ↑(Metric.closedBall 0 1)) (n : ℕ) :

↑(x ^ n) = ↑x ^ n

source

def Submonoid.unitSphere (𝕜 : Type u_2) [NormedDivisionRing 𝕜] :

Submonoid 𝕜

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

Equations

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

source

instance Metric.unitSphere.inv {𝕜 : Type u_1} [NormedDivisionRing 𝕜] :

Inv ↑(Metric.sphere 0 1)

Equations

Metric.unitSphere.inv = { inv := fun (x : ↑(Metric.sphere 0 1)) => { val := (↑x)⁻¹, property := ⋯ } }

source

@[simp]

theorem coe_inv_unitSphere {𝕜 : Type u_1} [NormedDivisionRing 𝕜] (x : ↑(Metric.sphere 0 1)) :

↑x⁻¹ = (↑x)⁻¹

source

instance Metric.unitSphere.div {𝕜 : Type u_1} [NormedDivisionRing 𝕜] :

Div ↑(Metric.sphere 0 1)

Equations

Metric.unitSphere.div = { div := fun (x y : ↑(Metric.sphere 0 1)) => { val := ↑x / ↑y, property := ⋯ } }

source

@[simp]

theorem coe_div_unitSphere {𝕜 : Type u_1} [NormedDivisionRing 𝕜] (x : ↑(Metric.sphere 0 1)) (y : ↑(Metric.sphere 0 1)) :

↑(x / y) = ↑x / ↑y

source

instance Metric.unitSphere.pow {𝕜 : Type u_1} [NormedDivisionRing 𝕜] :

Pow ↑(Metric.sphere 0 1) ℤ

Equations

Metric.unitSphere.pow = { pow := fun (x : ↑(Metric.sphere 0 1)) (n : ℤ) => { val := ↑x ^ n, property := ⋯ } }

source

@[simp]

theorem coe_zpow_unitSphere {𝕜 : Type u_1} [NormedDivisionRing 𝕜] (x : ↑(Metric.sphere 0 1)) (n : ℤ) :

↑(x ^ n) = ↑x ^ n

source

instance Metric.unitSphere.monoid {𝕜 : Type u_1} [NormedDivisionRing 𝕜] :

Monoid ↑(Metric.sphere 0 1)

Equations

Metric.unitSphere.monoid = SubmonoidClass.toMonoid (Submonoid.unitSphere 𝕜)

source

@[simp]

theorem coe_one_unitSphere {𝕜 : Type u_1} [NormedDivisionRing 𝕜] :

↑1 = 1

source

@[simp]

theorem coe_mul_unitSphere {𝕜 : Type u_1} [NormedDivisionRing 𝕜] (x : ↑(Metric.sphere 0 1)) (y : ↑(Metric.sphere 0 1)) :

↑(x * y) = ↑x * ↑y

source

@[simp]

theorem coe_pow_unitSphere {𝕜 : Type u_1} [NormedDivisionRing 𝕜] (x : ↑(Metric.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 to the group of units.

Equations

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

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.sphere.group {𝕜 : Type u_1} [NormedDivisionRing 𝕜] :

Group ↑(Metric.sphere 0 1)

Equations

Metric.sphere.group = Function.Injective.group ⇑(unitSphereToUnits 𝕜) ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

source

instance Metric.sphere.hasDistribNeg {𝕜 : Type u_1} [NormedDivisionRing 𝕜] :

HasDistribNeg ↑(Metric.sphere 0 1)

Equations

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

source

instance Metric.sphere.topologicalGroup {𝕜 : Type u_1} [NormedDivisionRing 𝕜] :

TopologicalGroup ↑(Metric.sphere 0 1)

Equations

⋯ = ⋯

source

instance Metric.sphere.commGroup {𝕜 : Type u_1} [NormedField 𝕜] :

CommGroup ↑(Metric.sphere 0 1)

Equations

Metric.sphere.commGroup = let __src := Metric.sphere.group; let __src_1 := Function.Injective.commMonoid Subtype.val ⋯ ⋯ ⋯ ⋯; CommGroup.mk ⋯

Documentation

Mathlib.Analysis.Normed.Field.UnitBall

Algebraic structures on unit balls and spheres #