Normed star rings and algebras #

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

A normed star group is a normed group with a compatible star which is isometric.

A C⋆-ring is a normed star group 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_group (E : Type u_1) [seminormed_add_comm_group E] [star_add_monoid E] :

Prop

norm_star : ∀ (x : E), ‖has_star.star x‖ = ‖x‖

A normed star group is a normed group with a compatible star which is isometric.

Instances of this typeclass

cstar_ring.to_normed_star_group

source

@[simp]

theorem nnnorm_star {E : Type u_2} [seminormed_add_comm_group E] [star_add_monoid E] [normed_star_group E] (x : E) :

‖has_star.star x‖₊ = ‖x‖₊

source

def star_normed_add_group_hom {E : Type u_2} [seminormed_add_comm_group E] [star_add_monoid E] [normed_star_group E] :

normed_add_group_hom E E

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

Equations

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

source

theorem star_isometry {E : Type u_2} [seminormed_add_comm_group E] [star_add_monoid E] [normed_star_group E] :

isometry has_star.star

The star map in a normed star group is an isometry

source

@[protected, instance]

def normed_star_group.to_has_continuous_star {E : Type u_2} [seminormed_add_comm_group E] [star_add_monoid E] [normed_star_group E] :

has_continuous_star E

source

@[protected, instance]

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

ring_hom_isometric (star_ring_end E)

source

@[class]

structure cstar_ring (E : Type u_4) [non_unital_normed_ring E] [star_ring E] :

Prop

norm_star_mul_self : ∀ {x : E}, ‖has_star.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 of this typeclass

source

@[protected, instance]

def real.cstar_ring :

cstar_ring ℝ

source

@[protected, instance]

def cstar_ring.to_normed_star_group {E : Type u_2} [non_unital_normed_ring E] [star_ring E] [cstar_ring E] :

normed_star_group E

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

source

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

‖x * has_star.star x‖ = ‖x‖ * ‖x‖

source

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

‖has_star.star x * x‖ = ‖has_star.star x‖ * ‖x‖

source

theorem cstar_ring.nnnorm_self_mul_star {E : Type u_2} [non_unital_normed_ring E] [star_ring E] [cstar_ring E] {x : E} :

‖x * has_star.star x‖₊ = ‖x‖₊ * ‖x‖₊

source

theorem cstar_ring.nnnorm_star_mul_self {E : Type u_2} [non_unital_normed_ring E] [star_ring E] [cstar_ring E] {x : E} :

‖has_star.star x * x‖₊ = ‖x‖₊ * ‖x‖₊

source

@[simp]

theorem cstar_ring.star_mul_self_eq_zero_iff {E : Type u_2} [non_unital_normed_ring E] [star_ring E] [cstar_ring E] (x : E) :

has_star.star x * x = 0 ↔ x = 0

source

theorem cstar_ring.star_mul_self_ne_zero_iff {E : Type u_2} [non_unital_normed_ring E] [star_ring E] [cstar_ring E] (x : E) :

has_star.star x * x ≠ 0 ↔ x ≠ 0

source

@[simp]

theorem cstar_ring.mul_star_self_eq_zero_iff {E : Type u_2} [non_unital_normed_ring E] [star_ring E] [cstar_ring E] (x : E) :

x * has_star.star x = 0 ↔ x = 0

source

theorem cstar_ring.mul_star_self_ne_zero_iff {E : Type u_2} [non_unital_normed_ring E] [star_ring E] [cstar_ring E] (x : E) :

x * has_star.star x ≠ 0 ↔ x ≠ 0

source

@[protected, instance]

def pi.star_ring' {ι : Type u_4} {R : ι → Type u_7} [Π (i : ι), non_unital_normed_ring (R i)] [Π (i : ι), star_ring (R i)] :

star_ring (Π (i : ι), R i)

This instance exists to short circuit type class resolution because of problems with inference involving Π-types.

Equations

pi.star_ring' = infer_instance

source

@[protected, instance]

def prod.cstar_ring {R₁ : Type u_5} {R₂ : Type u_6} [non_unital_normed_ring R₁] [star_ring R₁] [cstar_ring R₁] [non_unital_normed_ring R₂] [star_ring R₂] [cstar_ring R₂] :

cstar_ring (R₁ × R₂)

source

@[protected, instance]

def pi.cstar_ring {ι : Type u_4} {R : ι → Type u_7} [Π (i : ι), non_unital_normed_ring (R i)] [Π (i : ι), star_ring (R i)] [fintype ι] [∀ (i : ι), cstar_ring (R i)] :

cstar_ring (Π (i : ι), R i)

source

@[protected, instance]

def pi.cstar_ring' {ι : Type u_4} {R₁ : Type u_5} [non_unital_normed_ring R₁] [star_ring R₁] [cstar_ring R₁] [fintype ι] :

cstar_ring (ι → R₁)

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

theorem is_self_adjoint.nnnorm_pow_two_pow {E : Type u_2} [normed_ring E] [star_ring E] [cstar_ring E] {x : E} (hx : is_self_adjoint x) (n : ℕ) :

‖x ^ 2 ^ n‖₊ = ‖x‖₊ ^ 2 ^ n

source

theorem self_adjoint.nnnorm_pow_two_pow {E : Type u_2} [normed_ring E] [star_ring E] [cstar_ring E] (x : ↥(self_adjoint E)) (n : ℕ) :

‖x ^ 2 ^ n‖₊ = ‖x‖₊ ^ 2 ^ n

source

def starₗᵢ (𝕜 : Type u_1) {E : Type u_2} [comm_semiring 𝕜] [star_ring 𝕜] [seminormed_add_comm_group E] [star_add_monoid E] [normed_star_group 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 𝕜] [seminormed_add_comm_group E] [star_add_monoid E] [normed_star_group E] [module 𝕜 E] [star_module 𝕜 E] :

⇑(starₗᵢ 𝕜) = has_star.star

source

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

⇑(starₗᵢ 𝕜) x = has_star.star x

source

@[simp]

theorem starₗᵢ_to_continuous_linear_equiv {𝕜 : Type u_1} {E : Type u_2} [comm_semiring 𝕜] [star_ring 𝕜] [seminormed_add_comm_group E] [star_add_monoid E] [normed_star_group E] [module 𝕜 E] [star_module 𝕜 E] :

(starₗᵢ 𝕜).to_continuous_linear_equiv = starL 𝕜

source

@[protected, instance]

def star_subalgebra.to_normed_algebra {𝕜 : Type u_1} {A : Type u_2} [normed_field 𝕜] [star_ring 𝕜] [semi_normed_ring A] [star_ring A] [normed_algebra 𝕜 A] [star_module 𝕜 A] (S : star_subalgebra 𝕜 A) :

normed_algebra 𝕜 ↥S

Equations

S.to_normed_algebra = normed_algebra.induced 𝕜 ↥S A S.subtype

source

@[protected, instance]

def star_subalgebra.to_cstar_ring {R : Type u_1} {A : Type u_2} [comm_ring R] [star_ring R] [normed_ring A] [star_ring A] [cstar_ring A] [algebra R A] [star_module R A] (S : star_subalgebra R A) :

cstar_ring ↥S