Normed star rings and algebras #

A normed star monoid is a star_add_monoid endowed with a norm such that the star operation is isometric.

A C⋆-ring is a normed star monoid that is also a ring and that verifies the stronger condition ∥x⋆ * x∥ = ∥x∥^2 for all x. If a C⋆-ring is also a star algebra, then it is a C⋆-algebra.

To get a C⋆-algebra E over field 𝕜, use [normed_field 𝕜] [star_ring 𝕜] [normed_ring E] [star_ring E] [cstar_ring E] [normed_algebra 𝕜 E] [star_module 𝕜 E].

TODO #

Show that ∥x⋆ * x∥ = ∥x∥^2 is equivalent to ∥x⋆ * x∥ = ∥x⋆∥ * ∥x∥, which is used as the definition of C*-algebras in some sources (e.g. Wikipedia).

source

@[class]

structure normed_star_monoid (E : Type u_1) [normed_group E] [star_add_monoid E] :

Type

norm_star : ∀ {x : E}, ∥star x∥ = ∥x∥

A normed star ring is a star ring endowed with a norm such that star is isometric.

Instances

source

@[class]

structure cstar_ring (E : Type u_1) [normed_ring E] [star_ring E] :

Type

norm_star_mul_self : ∀ {x : E}, ∥(star x) * x∥ = ∥x∥ * ∥x∥

A C*-ring is a normed star ring that satifies the stronger condition ∥x⋆ * x∥ = ∥x∥^2 for every x.

Instances

source

@[protected, instance]

noncomputable def real.cstar_ring :

cstar_ring ℝ

Equations

real.cstar_ring = {norm_star_mul_self := real.cstar_ring._proof_1}

source

def star_normed_group_hom {E : Type u_2} [normed_group E] [star_add_monoid E] [normed_star_monoid E] :

normed_group_hom E E

The star map in a normed star group is a normed group homomorphism.

Equations

star_normed_group_hom = {to_fun := star_add_equiv.to_fun, map_add' := _, bound' := _}

source

theorem star_isometry {E : Type u_2} [normed_group E] [star_add_monoid E] [normed_star_monoid E] :

isometry star

The star map in a normed star group is an isometry

source

theorem continuous_star {E : Type u_2} [normed_group E] [star_add_monoid E] [normed_star_monoid E] :

continuous star

source

theorem continuous_on_star {E : Type u_2} [normed_group E] [star_add_monoid E] [normed_star_monoid E] {s : set E} :

continuous_on star s

source

theorem continuous_at_star {E : Type u_2} [normed_group E] [star_add_monoid E] [normed_star_monoid E] {x : E} :

continuous_at star x

source

theorem continuous_within_at_star {E : Type u_2} [normed_group E] [star_add_monoid E] [normed_star_monoid E] {s : set E} {x : E} :

continuous_within_at star s x

source

theorem tendsto_star {E : Type u_2} [normed_group E] [star_add_monoid E] [normed_star_monoid E] (x : E) :

filter.tendsto star (𝓝 x) (𝓝 (star x))

source

theorem filter.tendsto.star {E : Type u_2} {α : Type u_3} [normed_group E] [star_add_monoid E] [normed_star_monoid E] {f : α → E} {l : filter α} {y : E} (h : filter.tendsto f l (𝓝 y)) :

filter.tendsto (λ (x : α), star (f x)) l (𝓝 (star y))

source

theorem continuous.star {E : Type u_2} {α : Type u_3} [normed_group E] [star_add_monoid E] [normed_star_monoid E] [topological_space α] {f : α → E} (hf : continuous f) :

continuous (λ (y : α), star (f y))

source

theorem continuous_at.star {E : Type u_2} {α : Type u_3} [normed_group E] [star_add_monoid E] [normed_star_monoid E] [topological_space α] {f : α → E} {x : α} (hf : continuous_at f x) :

continuous_at (λ (x : α), star (f x)) x

source

theorem continuous_on.star {E : Type u_2} {α : Type u_3} [normed_group E] [star_add_monoid E] [normed_star_monoid E] [topological_space α] {f : α → E} {s : set α} (hf : continuous_on f s) :

continuous_on (λ (x : α), star (f x)) s

source

theorem continuous_within_at.star {E : Type u_2} {α : Type u_3} [normed_group E] [star_add_monoid E] [normed_star_monoid E] [topological_space α] {f : α → E} {s : set α} {x : α} (hf : continuous_within_at f s x) :

continuous_within_at (λ (x : α), star (f x)) s x

source

@[protected, instance]

def ring_hom_isometric.star_ring_end {E : Type u_2} [normed_comm_ring E] [star_ring E] [normed_star_monoid E] :

ring_hom_isometric conj

source

@[protected, instance]

def cstar_ring.to_normed_star_monoid {E : Type u_2} [normed_ring E] [star_ring E] [cstar_ring E] :

normed_star_monoid E

In a C*-ring, star preserves the norm.

Equations

cstar_ring.to_normed_star_monoid = {norm_star := _}

source

theorem cstar_ring.norm_self_mul_star {E : Type u_2} [normed_ring E] [star_ring E] [cstar_ring E] {x : E} :

∥x * star x∥ = ∥x∥ * ∥x∥

source

theorem cstar_ring.norm_star_mul_self' {E : Type u_2} [normed_ring E] [star_ring E] [cstar_ring E] {x : E} :

∥(star x) * x∥ = ∥star x∥ * ∥x∥

source

@[simp]

theorem cstar_ring.norm_one {E : Type u_2} [normed_ring E] [star_ring E] [cstar_ring E] [nontrivial E] :

∥1∥ = 1

source

@[protected, instance]

def cstar_ring.norm_one_class {E : Type u_2} [normed_ring E] [star_ring E] [cstar_ring E] [nontrivial E] :

norm_one_class E

source

theorem cstar_ring.norm_coe_unitary {E : Type u_2} [normed_ring E] [star_ring E] [cstar_ring E] [nontrivial E] (U : ↥(unitary E)) :

∥↑U∥ = 1

source

@[simp]

theorem cstar_ring.norm_of_mem_unitary {E : Type u_2} [normed_ring E] [star_ring E] [cstar_ring E] [nontrivial E] {U : E} (hU : U ∈ unitary E) :

∥U∥ = 1

source

@[simp]

theorem cstar_ring.norm_coe_unitary_mul {E : Type u_2} [normed_ring E] [star_ring E] [cstar_ring E] (U : ↥(unitary E)) (A : E) :

∥(↑U) * A∥ = ∥A∥

source

@[simp]

theorem cstar_ring.norm_unitary_smul {E : Type u_2} [normed_ring E] [star_ring E] [cstar_ring E] (U : ↥(unitary E)) (A : E) :

∥U • A∥ = ∥A∥

source

theorem cstar_ring.norm_mem_unitary_mul {E : Type u_2} [normed_ring E] [star_ring E] [cstar_ring E] {U : E} (A : E) (hU : U ∈ unitary E) :

∥U * A∥ = ∥A∥

source

@[simp]

theorem cstar_ring.norm_mul_coe_unitary {E : Type u_2} [normed_ring E] [star_ring E] [cstar_ring E] (A : E) (U : ↥(unitary E)) :

∥A * ↑U∥ = ∥A∥

source

theorem cstar_ring.norm_mul_mem_unitary {E : Type u_2} [normed_ring E] [star_ring E] [cstar_ring E] (A : E) {U : E} (hU : U ∈ unitary E) :

∥A * U∥ = ∥A∥

source

def starₗᵢ (𝕜 : Type u_1) {E : Type u_2} [comm_semiring 𝕜] [star_ring 𝕜] [normed_ring E] [star_ring E] [normed_star_monoid E] [module 𝕜 E] [star_module 𝕜 E] :

E ≃ₗᵢ⋆[𝕜] E

star bundled as a linear isometric equivalence

Equations

starₗᵢ 𝕜 = {to_linear_equiv := {to_fun := star_add_equiv.to_fun, map_add' := _, map_smul' := _, inv_fun := star_add_equiv.inv_fun, left_inv := _, right_inv := _}, norm_map' := _}

source

@[simp]

theorem coe_starₗᵢ {𝕜 : Type u_1} {E : Type u_2} [comm_semiring 𝕜] [star_ring 𝕜] [normed_ring E] [star_ring E] [normed_star_monoid E] [module 𝕜 E] [star_module 𝕜 E] :

⇑(starₗᵢ 𝕜) = star

source

theorem starₗᵢ_apply {𝕜 : Type u_1} {E : Type u_2} [comm_semiring 𝕜] [star_ring 𝕜] [normed_ring E] [star_ring E] [normed_star_monoid E] [module 𝕜 E] [star_module 𝕜 E] {x : E} :

⇑(starₗᵢ 𝕜) x = star x