# Normed star rings and algebras #

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 [NormedField 𝕜] [StarRing 𝕜] [NormedRing E] [StarRing E] [CstarRing E] [NormedAlgebra 𝕜 E] [StarModule 𝕜 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).
class NormedStarGroup (E : Type u_1) [] :

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

Instances
@[simp]
theorem NormedStarGroup.norm_star {E : Type u_1} [] [self : ] (x : E) :
@[simp]
theorem nnnorm_star {E : Type u_2} [] [] (x : E) :
def starNormedAddGroupHom {E : Type u_2} [] [] :

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

Equations
• starNormedAddGroupHom = let __src := starAddEquiv; { toFun := __src.toFun, map_add' := , bound' := }
Instances For
theorem star_isometry {E : Type u_2} [] [] :

The star map in a normed star group is an isometry

@[instance 100]
instance NormedStarGroup.to_continuousStar {E : Type u_2} [] [] :
Equations
• =
instance RingHomIsometric.starRingEnd {E : Type u_2} [] [] [] :
Equations
• =
class CstarRing (E : Type u_4) [] :

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

Instances
theorem CstarRing.norm_star_mul_self {E : Type u_4} [] [self : ] {x : E} :
Equations
@[instance 100]
instance CstarRing.to_normedStarGroup {E : Type u_2} [] [] :

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

Equations
• =
theorem CstarRing.norm_self_mul_star {E : Type u_2} [] [] {x : E} :
theorem CstarRing.norm_star_mul_self' {E : Type u_2} [] [] {x : E} :
@[simp]
theorem CstarRing.star_mul_self_eq_zero_iff {E : Type u_2} [] [] (x : E) :
star x * x = 0 x = 0
theorem CstarRing.star_mul_self_ne_zero_iff {E : Type u_2} [] [] (x : E) :
star x * x 0 x 0
@[simp]
theorem CstarRing.mul_star_self_eq_zero_iff {E : Type u_2} [] [] (x : E) :
x * star x = 0 x = 0
theorem CstarRing.mul_star_self_ne_zero_iff {E : Type u_2} [] [] (x : E) :
x * star x 0 x 0
instance Pi.starRing' {ι : Type u_4} {R : ιType u_7} [(i : ι) → NonUnitalNormedRing (R i)] [(i : ι) → StarRing (R i)] :
StarRing ((i : ι) → R i)

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

Equations
• Pi.starRing' = inferInstance
instance Prod.cstarRing {R₁ : Type u_5} {R₂ : Type u_6} [] [StarRing R₁] [] [] [StarRing R₂] [] :
CstarRing (R₁ × R₂)
Equations
• =
instance Pi.cstarRing {ι : Type u_4} {R : ιType u_7} [(i : ι) → NonUnitalNormedRing (R i)] [(i : ι) → StarRing (R i)] [] [∀ (i : ι), CstarRing (R i)] :
CstarRing ((i : ι) → R i)
Equations
• =
instance Pi.cstarRing' {ι : Type u_4} {R₁ : Type u_5} [] [StarRing R₁] [] [] :
CstarRing (ιR₁)
Equations
• =
@[simp]
theorem CstarRing.norm_one {E : Type u_2} [] [] [] [] :
@[instance 100]
instance CstarRing.instNormOneClassOfNontrivial {E : Type u_2} [] [] [] [] :
Equations
• =
theorem CstarRing.norm_coe_unitary {E : Type u_2} [] [] [] [] (U : ()) :
U = 1
@[simp]
theorem CstarRing.norm_of_mem_unitary {E : Type u_2} [] [] [] [] {U : E} (hU : U ) :
@[simp]
theorem CstarRing.norm_coe_unitary_mul {E : Type u_2} [] [] [] (U : ()) (A : E) :
U * A = A
@[simp]
theorem CstarRing.norm_unitary_smul {E : Type u_2} [] [] [] (U : ()) (A : E) :
theorem CstarRing.norm_mem_unitary_mul {E : Type u_2} [] [] [] {U : E} (A : E) (hU : U ) :
@[simp]
theorem CstarRing.norm_mul_coe_unitary {E : Type u_2} [] [] [] (A : E) (U : ()) :
A * U = A
theorem CstarRing.norm_mul_mem_unitary {E : Type u_2} [] [] [] (A : E) {U : E} (hU : U ) :
theorem IsSelfAdjoint.nnnorm_pow_two_pow {E : Type u_2} [] [] [] {x : E} (hx : ) (n : ) :
x ^ 2 ^ n‖₊ = x‖₊ ^ 2 ^ n
theorem selfAdjoint.nnnorm_pow_two_pow {E : Type u_2} [] [] [] (x : ()) (n : ) :
x ^ 2 ^ n‖₊ = x‖₊ ^ 2 ^ n
def starₗᵢ (𝕜 : Type u_1) {E : Type u_2} [] [] [] [] [Module 𝕜 E] [] :

star bundled as a linear isometric equivalence

Equations
• = let __src := starAddEquiv; { toFun := __src.toFun, map_add' := , map_smul' := , invFun := __src.invFun, left_inv := , right_inv := , norm_map' := }
Instances For
@[simp]
theorem coe_starₗᵢ {𝕜 : Type u_1} {E : Type u_2} [] [] [] [] [Module 𝕜 E] [] :
() = star
theorem starₗᵢ_apply {𝕜 : Type u_1} {E : Type u_2} [] [] [] [] [Module 𝕜 E] [] {x : E} :
() x = star x
@[simp]
theorem starₗᵢ_toContinuousLinearEquiv {𝕜 : Type u_1} {E : Type u_2} [] [] [] [] [Module 𝕜 E] [] :
().toContinuousLinearEquiv =
instance StarSubalgebra.toNormedAlgebra {𝕜 : Type u_4} {A : Type u_5} [] [] [] [] [] [] (S : ) :
Equations
instance StarSubalgebra.to_cstarRing {R : Type u_4} {A : Type u_5} [] [] [] [] [] [Algebra R A] [] (S : ) :
Equations
• =