Algebraic structures on unit balls and spheres #
In this file we define algebraic structures (semigroup
, comm_semigroup
, monoid
, comm_monoid
,
group
, comm_group
) on metric.ball (0 : ๐) 1
, metric.closed_ball (0 : ๐) 1
, and
metric.sphere (0 : ๐) 1
. In each case we use the weakest possible typeclass assumption on ๐
,
from non_unital_semi_normed_ring
to normed_field
.
Unit ball in a non unital semi normed ring as a bundled subsemigroup
.
Equations
- subsemigroup.unit_ball ๐ = {carrier := metric.ball 0 1, mul_mem' := _}
@[protected, instance]
def
metric.ball.semigroup
{๐ : Type u_1}
[non_unital_semi_normed_ring ๐] :
semigroup โฅ(metric.ball 0 1)
Equations
@[protected, instance]
@[protected, instance]
def
metric.ball.comm_semigroup
{๐ : Type u_1}
[semi_normed_comm_ring ๐] :
comm_semigroup โฅ(metric.ball 0 1)
Equations
@[protected, instance]
Equations
- metric.ball.has_distrib_neg = function.injective.has_distrib_neg coe metric.ball.has_distrib_neg._proof_1 metric.ball.has_distrib_neg._proof_2 metric.ball.has_distrib_neg._proof_3
@[simp, norm_cast]
theorem
coe_mul_unit_ball
{๐ : Type u_1}
[non_unital_semi_normed_ring ๐]
(x y : โฅ(metric.ball 0 1)) :
def
subsemigroup.unit_closed_ball
(๐ : Type u_1)
[non_unital_semi_normed_ring ๐] :
subsemigroup ๐
Closed unit ball in a non unital semi normed ring as a bundled subsemigroup
.
Equations
- subsemigroup.unit_closed_ball ๐ = {carrier := metric.closed_ball 0 1, mul_mem' := _}
@[protected, instance]
@[protected, instance]
Equations
- metric.closed_ball.has_distrib_neg = function.injective.has_distrib_neg coe metric.closed_ball.has_distrib_neg._proof_1 metric.closed_ball.has_distrib_neg._proof_2 metric.closed_ball.has_distrib_neg._proof_3
@[protected, instance]
@[simp, norm_cast]
theorem
coe_mul_unit_closed_ball
{๐ : Type u_1}
[non_unital_semi_normed_ring ๐]
(x y : โฅ(metric.closed_ball 0 1)) :
def
submonoid.unit_closed_ball
(๐ : Type u_1)
[semi_normed_ring ๐]
[norm_one_class ๐] :
submonoid ๐
Closed unit ball in a semi normed ring as a bundled submonoid
.
Equations
- submonoid.unit_closed_ball ๐ = {carrier := metric.closed_ball 0 1, mul_mem' := _, one_mem' := _}
@[protected, instance]
def
metric.closed_ball.monoid
{๐ : Type u_1}
[semi_normed_ring ๐]
[norm_one_class ๐] :
monoid โฅ(metric.closed_ball 0 1)
Equations
@[protected, instance]
def
metric.closed_ball.comm_monoid
{๐ : Type u_1}
[semi_normed_comm_ring ๐]
[norm_one_class ๐] :
@[simp, norm_cast]
@[simp, norm_cast]
theorem
coe_pow_unit_closed_ball
{๐ : Type u_1}
[semi_normed_ring ๐]
[norm_one_class ๐]
(x : โฅ(metric.closed_ball 0 1))
(n : โ) :
Unit sphere in a normed division ring as a bundled submonoid
.
Equations
- submonoid.unit_sphere ๐ = {carrier := metric.sphere 0 1, mul_mem' := _, one_mem' := _}
@[protected, instance]
def
metric.sphere.has_inv
{๐ : Type u_1}
[normed_division_ring ๐] :
has_inv โฅ(metric.sphere 0 1)
Equations
- metric.sphere.has_inv = {inv := ฮป (x : โฅ(metric.sphere 0 1)), โจ(โx)โปยน, _โฉ}
@[simp, norm_cast]
theorem
coe_inv_unit_sphere
{๐ : Type u_1}
[normed_division_ring ๐]
(x : โฅ(metric.sphere 0 1)) :
@[protected, instance]
def
metric.sphere.has_div
{๐ : Type u_1}
[normed_division_ring ๐] :
has_div โฅ(metric.sphere 0 1)
Equations
- metric.sphere.has_div = {div := ฮป (x y : โฅ(metric.sphere 0 1)), โจโx / โy, _โฉ}
@[simp, norm_cast]
theorem
coe_div_unit_sphere
{๐ : Type u_1}
[normed_division_ring ๐]
(x y : โฅ(metric.sphere 0 1)) :
@[protected, instance]
Equations
- int.has_pow = {pow := ฮป (x : โฅ(metric.sphere 0 1)) (n : โค), โจโx ^ n, _โฉ}
@[simp, norm_cast]
theorem
coe_zpow_unit_sphere
{๐ : Type u_1}
[normed_division_ring ๐]
(x : โฅ(metric.sphere 0 1))
(n : โค) :
@[protected, instance]
def
metric.sphere.monoid
{๐ : Type u_1}
[normed_division_ring ๐] :
monoid โฅ(metric.sphere 0 1)
Equations
@[simp, norm_cast]
@[simp, norm_cast]
theorem
coe_mul_unit_sphere
{๐ : Type u_1}
[normed_division_ring ๐]
(x y : โฅ(metric.sphere 0 1)) :
@[simp, norm_cast]
theorem
coe_pow_unit_sphere
{๐ : Type u_1}
[normed_division_ring ๐]
(x : โฅ(metric.sphere 0 1))
(n : โ) :
def
unit_sphere_to_units
(๐ : Type u_1)
[normed_division_ring ๐] :
โฅ(metric.sphere 0 1) โ* ๐หฃ
Monoid homomorphism from the unit sphere to the group of units.
Equations
- unit_sphere_to_units ๐ = units.lift_right (submonoid.unit_sphere ๐).subtype (ฮป (x : โฅ(metric.sphere 0 1)), units.mk0 โx _) _
@[simp]
theorem
unit_sphere_to_units_apply_coe
{๐ : Type u_1}
[normed_division_ring ๐]
(x : โฅ(metric.sphere 0 1)) :
โ(โ(unit_sphere_to_units ๐) x) = โx
@[protected, instance]
def
metric.sphere.group
{๐ : Type u_1}
[normed_division_ring ๐] :
group โฅ(metric.sphere 0 1)
Equations
- metric.sphere.group = function.injective.group โ(unit_sphere_to_units ๐) unit_sphere_to_units_injective metric.sphere.group._proof_1 metric.sphere.group._proof_2 metric.sphere.group._proof_3 metric.sphere.group._proof_4 metric.sphere.group._proof_5 metric.sphere.group._proof_6
@[protected, instance]
Equations
- metric.sphere.has_distrib_neg = function.injective.has_distrib_neg coe metric.sphere.has_distrib_neg._proof_1 metric.sphere.has_distrib_neg._proof_2 metric.sphere.has_distrib_neg._proof_3
@[protected, instance]
@[protected, instance]
def
metric.sphere.comm_group
{๐ : Type u_1}
[normed_field ๐] :
comm_group โฅ(metric.sphere 0 1)
Equations
- metric.sphere.comm_group = {mul := group.mul metric.sphere.group, mul_assoc := _, one := group.one metric.sphere.group, one_mul := _, mul_one := _, npow := group.npow metric.sphere.group, npow_zero' := _, npow_succ' := _, inv := group.inv metric.sphere.group, div := group.div metric.sphere.group, div_eq_mul_inv := _, zpow := group.zpow metric.sphere.group, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, mul_left_inv := _, mul_comm := _}