Algebraic structures on unit balls and spheres #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source

def subsemigroup.unit_ball (𝕜 : Type u_1) [non_unital_semi_normed_ring 𝕜] :

subsemigroup 𝕜

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

Equations

subsemigroup.unit_ball 𝕜 = {carrier := metric.ball 0 1, mul_mem' := _}

source

@[protected, instance]

def metric.ball.semigroup {𝕜 : Type u_1} [non_unital_semi_normed_ring 𝕜] :

semigroup ↥(metric.ball 0 1)

Equations

metric.ball.semigroup = mul_mem_class.to_semigroup (subsemigroup.unit_ball 𝕜)

source

@[protected, instance]

def metric.ball.has_continuous_mul {𝕜 : Type u_1} [non_unital_semi_normed_ring 𝕜] :

has_continuous_mul ↥(metric.ball 0 1)

source

@[protected, instance]

def metric.ball.comm_semigroup {𝕜 : Type u_1} [semi_normed_comm_ring 𝕜] :

comm_semigroup ↥(metric.ball 0 1)

Equations

metric.ball.comm_semigroup = mul_mem_class.to_comm_semigroup (subsemigroup.unit_ball 𝕜)

source

@[protected, instance]

def metric.ball.has_distrib_neg {𝕜 : Type u_1} [non_unital_semi_normed_ring 𝕜] :

has_distrib_neg ↥(metric.ball 0 1)

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

source

@[simp, norm_cast]

theorem coe_mul_unit_ball {𝕜 : Type u_1} [non_unital_semi_normed_ring 𝕜] (x y : ↥(metric.ball 0 1)) :

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

source

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' := _}

source

@[protected, instance]

def metric.closed_ball.semigroup {𝕜 : Type u_1} [non_unital_semi_normed_ring 𝕜] :

semigroup ↥(metric.closed_ball 0 1)

Equations

metric.closed_ball.semigroup = mul_mem_class.to_semigroup (subsemigroup.unit_closed_ball 𝕜)

source

@[protected, instance]

def metric.closed_ball.has_distrib_neg {𝕜 : Type u_1} [non_unital_semi_normed_ring 𝕜] :

has_distrib_neg ↥(metric.closed_ball 0 1)

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

source

@[protected, instance]

def metric.closed_ball.has_continuous_mul {𝕜 : Type u_1} [non_unital_semi_normed_ring 𝕜] :

has_continuous_mul ↥(metric.closed_ball 0 1)

source

@[simp, norm_cast]

theorem coe_mul_unit_closed_ball {𝕜 : Type u_1} [non_unital_semi_normed_ring 𝕜] (x y : ↥(metric.closed_ball 0 1)) :

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

source

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' := _}

source

@[protected, instance]

def metric.closed_ball.monoid {𝕜 : Type u_1} [semi_normed_ring 𝕜] [norm_one_class 𝕜] :

monoid ↥(metric.closed_ball 0 1)

Equations

metric.closed_ball.monoid = submonoid_class.to_monoid (submonoid.unit_closed_ball 𝕜)

source

@[protected, instance]

def metric.closed_ball.comm_monoid {𝕜 : Type u_1} [semi_normed_comm_ring 𝕜] [norm_one_class 𝕜] :

comm_monoid ↥(metric.closed_ball 0 1)

Equations

metric.closed_ball.comm_monoid = submonoid_class.to_comm_monoid (submonoid.unit_closed_ball 𝕜)

source

@[simp, norm_cast]

theorem coe_one_unit_closed_ball {𝕜 : Type u_1} [semi_normed_ring 𝕜] [norm_one_class 𝕜] :

↑1 = 1

source

@[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 : ℕ) :

↑(x ^ n) = ↑x ^ n

source

def submonoid.unit_sphere (𝕜 : Type u_1) [normed_division_ring 𝕜] :

submonoid 𝕜

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

Equations

submonoid.unit_sphere 𝕜 = {carrier := metric.sphere 0 1, mul_mem' := _, one_mem' := _}

source

@[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)⁻¹, _⟩}

source

@[simp, norm_cast]

theorem coe_inv_unit_sphere {𝕜 : Type u_1} [normed_division_ring 𝕜] (x : ↥(metric.sphere 0 1)) :

↑x⁻¹ = (↑x)⁻¹

source

@[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, _⟩}

source

@[simp, norm_cast]

theorem coe_div_unit_sphere {𝕜 : Type u_1} [normed_division_ring 𝕜] (x y : ↥(metric.sphere 0 1)) :

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

source

@[protected, instance]

def int.has_pow {𝕜 : Type u_1} [normed_division_ring 𝕜] :

has_pow ↥(metric.sphere 0 1) ℤ

Equations

int.has_pow = {pow := λ (x : ↥(metric.sphere 0 1)) (n : ℤ), ⟨↑x ^ n, _⟩}

source

@[simp, norm_cast]

theorem coe_zpow_unit_sphere {𝕜 : Type u_1} [normed_division_ring 𝕜] (x : ↥(metric.sphere 0 1)) (n : ℤ) :

↑(x ^ n) = ↑x ^ n

source

@[protected, instance]

def metric.sphere.monoid {𝕜 : Type u_1} [normed_division_ring 𝕜] :

monoid ↥(metric.sphere 0 1)

Equations

metric.sphere.monoid = submonoid_class.to_monoid (submonoid.unit_sphere 𝕜)

source

@[simp, norm_cast]

theorem coe_one_unit_sphere {𝕜 : Type u_1} [normed_division_ring 𝕜] :

↑1 = 1

source

@[simp, norm_cast]

theorem coe_mul_unit_sphere {𝕜 : Type u_1} [normed_division_ring 𝕜] (x y : ↥(metric.sphere 0 1)) :

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

source

@[simp, norm_cast]

theorem coe_pow_unit_sphere {𝕜 : Type u_1} [normed_division_ring 𝕜] (x : ↥(metric.sphere 0 1)) (n : ℕ) :

↑(x ^ n) = ↑x ^ n

source

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 _) _

source

@[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

source

theorem unit_sphere_to_units_injective {𝕜 : Type u_1} [normed_division_ring 𝕜] :

function.injective ⇑(unit_sphere_to_units 𝕜)

source

@[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

source

@[protected, instance]

def metric.sphere.has_distrib_neg {𝕜 : Type u_1} [normed_division_ring 𝕜] :

has_distrib_neg ↥(metric.sphere 0 1)

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

source

@[protected, instance]

def metric.sphere.topological_group {𝕜 : Type u_1} [normed_division_ring 𝕜] :

topological_group ↥(metric.sphere 0 1)

source

@[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 := _}