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‖^2 ≤ ‖x⋆ * x‖ for all x (which actually implies equality). If a C⋆-ring is also a star algebra, then it is a C⋆-algebra.

Note that the type classes corresponding to C⋆-algebras are defined in Mathlib/Analysis/CStarAlgebra/Classes.

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 NormedStarGroup (E : Type u_1) [SeminormedAddCommGroup E] [StarAddMonoid E] :

Prop

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

norm_star_le (x : E) : ‖star x‖ ≤ ‖x‖

Instances

source

@[simp]

theorem norm_star {E : Type u_2} [SeminormedAddCommGroup E] [StarAddMonoid E] [NormedStarGroup E] (x : E) :

‖star x‖ = ‖x‖

source

@[simp]

theorem nnnorm_star {E : Type u_2} [SeminormedAddCommGroup E] [StarAddMonoid E] [NormedStarGroup E] (x : E) :

‖star x‖₊ = ‖x‖₊

source

def starNormedAddGroupHom {E : Type u_2} [SeminormedAddCommGroup E] [StarAddMonoid E] [NormedStarGroup E] :

NormedAddGroupHom E E

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

Equations

starNormedAddGroupHom = { toFun := starAddEquiv.toFun, map_add' := ⋯, bound' := ⋯ }

Instances For

source

theorem star_isometry {E : Type u_2} [SeminormedAddCommGroup E] [StarAddMonoid E] [NormedStarGroup E] :

Isometry star

The star map in a normed star group is an isometry

source

@[instance 100]

instance NormedStarGroup.to_continuousStar {E : Type u_2} [SeminormedAddCommGroup E] [StarAddMonoid E] [NormedStarGroup E] :

ContinuousStar E

source

instance RingHomIsometric.starRingEnd {E : Type u_2} [NormedCommRing E] [StarRing E] [NormedStarGroup E] :

RingHomIsometric (_root_.starRingEnd E)

source

class CStarRing (E : Type u_4) [NonUnitalNormedRing E] [StarRing E] :

Prop

A C*-ring is a normed star ring that satisfies the stronger condition ‖x‖ ^ 2 ≤ ‖x⋆ * x‖ for every x. Note that this condition actually implies equality, as is shown in norm_star_mul_self below.

norm_mul_self_le (x : E) : ‖x‖ * ‖x‖ ≤ ‖star x * x‖

Instances

source

instance instCStarRingReal :

CStarRing ℝ

source

theorem CStarRing.of_le_norm_mul_star_self {E : Type u_2} [NonUnitalNormedRing E] [StarRing E] (h : ∀ (x : E), ‖x‖ * ‖x‖ ≤ ‖x * star x‖) :

CStarRing E

source

@[instance 100]

instance CStarRing.to_normedStarGroup {E : Type u_2} [NonUnitalNormedRing E] [StarRing E] [CStarRing E] :

NormedStarGroup E

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

source

theorem CStarRing.norm_star_mul_self {E : Type u_2} [NonUnitalNormedRing E] [StarRing E] [CStarRing E] {x : E} :

‖star x * x‖ = ‖x‖ * ‖x‖

source

theorem CStarRing.norm_self_mul_star {E : Type u_2} [NonUnitalNormedRing E] [StarRing E] [CStarRing E] {x : E} :

‖x * star x‖ = ‖x‖ * ‖x‖

source

theorem CStarRing.norm_star_mul_self' {E : Type u_2} [NonUnitalNormedRing E] [StarRing E] [CStarRing E] {x : E} :

‖star x * x‖ = ‖star x‖ * ‖x‖

source

theorem CStarRing.nnnorm_self_mul_star {E : Type u_2} [NonUnitalNormedRing E] [StarRing E] [CStarRing E] {x : E} :

‖x * star x‖₊ = ‖x‖₊ * ‖x‖₊

source

theorem CStarRing.nnnorm_star_mul_self {E : Type u_2} [NonUnitalNormedRing E] [StarRing E] [CStarRing E] {x : E} :

‖star x * x‖₊ = ‖x‖₊ * ‖x‖₊

source

@[simp]

theorem CStarRing.star_mul_self_eq_zero_iff {E : Type u_2} [NonUnitalNormedRing E] [StarRing E] [CStarRing E] (x : E) :

star x * x = 0 ↔ x = 0

source

theorem CStarRing.star_mul_self_ne_zero_iff {E : Type u_2} [NonUnitalNormedRing E] [StarRing E] [CStarRing E] (x : E) :

star x * x ≠ 0 ↔ x ≠ 0

source

@[simp]

theorem CStarRing.mul_star_self_eq_zero_iff {E : Type u_2} [NonUnitalNormedRing E] [StarRing E] [CStarRing E] (x : E) :

x * star x = 0 ↔ x = 0

source

theorem CStarRing.mul_star_self_ne_zero_iff {E : Type u_2} [NonUnitalNormedRing E] [StarRing E] [CStarRing E] (x : E) :

x * star x ≠ 0 ↔ x ≠ 0

source

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

source

instance Prod.cstarRing {R₁ : Type u_5} {R₂ : Type u_6} [NonUnitalNormedRing R₁] [StarRing R₁] [CStarRing R₁] [NonUnitalNormedRing R₂] [StarRing R₂] [CStarRing R₂] :

CStarRing (R₁ × R₂)

source

instance Pi.cstarRing {ι : Type u_4} {R : ι → Type u_7} [(i : ι) → NonUnitalNormedRing (R i)] [(i : ι) → StarRing (R i)] [Fintype ι] [∀ (i : ι), CStarRing (R i)] :

CStarRing ((i : ι) → R i)

source

instance Pi.cstarRing' {ι : Type u_4} {R₁ : Type u_5} [NonUnitalNormedRing R₁] [StarRing R₁] [CStarRing R₁] [Fintype ι] :

CStarRing (ι → R₁)

source

instance CStarRing.MulOpposite.instMulOpposite {E : Type u_4} [NonUnitalNormedRing E] [StarRing E] [CStarRing E] :

CStarRing Eᵐᵒᵖ

source

theorem CStarRing.norm_one {E : Type u_2} [NormedRing E] [StarRing E] [CStarRing E] [Nontrivial E] :

‖1‖ = 1

source

@[instance 100]

instance CStarRing.instNormOneClassOfNontrivial {E : Type u_2} [NormedRing E] [StarRing E] [CStarRing E] [Nontrivial E] :

NormOneClass E

source

theorem CStarRing.norm_coe_unitary {E : Type u_2} [NormedRing E] [StarRing E] [CStarRing E] [Nontrivial E] (U : ↥(unitary E)) :

‖↑U‖ = 1

source

@[simp]

theorem CStarRing.norm_of_mem_unitary {E : Type u_2} [NormedRing E] [StarRing E] [CStarRing E] [Nontrivial E] {U : E} (hU : U ∈ unitary E) :

‖U‖ = 1

source

@[simp]

theorem CStarRing.norm_coe_unitary_mul {E : Type u_2} [NormedRing E] [StarRing E] [CStarRing E] (U : ↥(unitary E)) (A : E) :

‖↑U * A‖ = ‖A‖

source

@[simp]

theorem CStarRing.norm_unitary_smul {E : Type u_2} [NormedRing E] [StarRing E] [CStarRing E] (U : ↥(unitary E)) (A : E) :

‖U • A‖ = ‖A‖

source

theorem CStarRing.norm_mem_unitary_mul {E : Type u_2} [NormedRing E] [StarRing E] [CStarRing E] {U : E} (A : E) (hU : U ∈ unitary E) :

‖U * A‖ = ‖A‖

source

@[simp]

theorem CStarRing.norm_mul_coe_unitary {E : Type u_2} [NormedRing E] [StarRing E] [CStarRing E] (A : E) (U : ↥(unitary E)) :

‖A * ↑U‖ = ‖A‖

source

theorem CStarRing.norm_mul_mem_unitary {E : Type u_2} [NormedRing E] [StarRing E] [CStarRing E] (A : E) {U : E} (hU : U ∈ unitary E) :

‖A * U‖ = ‖A‖

source

theorem IsSelfAdjoint.nnnorm_pow_two_pow {E : Type u_2} [NormedRing E] [StarRing E] [CStarRing E] {x : E} (hx : IsSelfAdjoint x) (n : ℕ) :

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

source

theorem selfAdjoint.nnnorm_pow_two_pow {E : Type u_2} [NormedRing E] [StarRing E] [CStarRing E] (x : ↥(selfAdjoint E)) (n : ℕ) :

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

source

def starₗᵢ (𝕜 : Type u_1) {E : Type u_2} [CommSemiring 𝕜] [StarRing 𝕜] [SeminormedAddCommGroup E] [StarAddMonoid E] [NormedStarGroup E] [Module 𝕜 E] [StarModule 𝕜 E] :

E ≃ₗᵢ⋆[𝕜] E

star bundled as a linear isometric equivalence

Equations

starₗᵢ 𝕜 = { toFun := starAddEquiv.toFun, map_add' := ⋯, map_smul' := ⋯, invFun := starAddEquiv.invFun, left_inv := ⋯, right_inv := ⋯, norm_map' := ⋯ }

Instances For

source

@[simp]

theorem coe_starₗᵢ {𝕜 : Type u_1} {E : Type u_2} [CommSemiring 𝕜] [StarRing 𝕜] [SeminormedAddCommGroup E] [StarAddMonoid E] [NormedStarGroup E] [Module 𝕜 E] [StarModule 𝕜 E] :

⇑(starₗᵢ 𝕜) = star

source

theorem starₗᵢ_apply {𝕜 : Type u_1} {E : Type u_2} [CommSemiring 𝕜] [StarRing 𝕜] [SeminormedAddCommGroup E] [StarAddMonoid E] [NormedStarGroup E] [Module 𝕜 E] [StarModule 𝕜 E] {x : E} :

(starₗᵢ 𝕜) x = star x

source

@[simp]

theorem starₗᵢ_toContinuousLinearEquiv {𝕜 : Type u_1} {E : Type u_2} [CommSemiring 𝕜] [StarRing 𝕜] [SeminormedAddCommGroup E] [StarAddMonoid E] [NormedStarGroup E] [Module 𝕜 E] [StarModule 𝕜 E] :

(starₗᵢ 𝕜).toContinuousLinearEquiv = starL 𝕜

source

instance StarSubalgebra.toNormedAlgebra {𝕜 : Type u_4} {A : Type u_5} [NormedField 𝕜] [StarRing 𝕜] [SeminormedRing A] [StarRing A] [NormedAlgebra 𝕜 A] [StarModule 𝕜 A] (S : StarSubalgebra 𝕜 A) :

NormedAlgebra 𝕜 ↥S

Equations

S.toNormedAlgebra = NormedAlgebra.induced 𝕜 (↥S) A S.subtype

source

instance StarSubalgebra.to_cstarRing {R : Type u_4} {A : Type u_5} [CommRing R] [StarRing R] [NormedRing A] [StarRing A] [CStarRing A] [Algebra R A] [StarModule R A] (S : StarSubalgebra R A) :

CStarRing ↥S

Documentation

Mathlib.Analysis.CStarAlgebra.Basic

Normed star rings and algebras #

TODO #