Documentation

Mathlib.Analysis.CStarAlgebra.Basic

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.

To get a C⋆-algebra E over field 𝕜, use [NormedField 𝕜] [StarRing 𝕜] [NormedRing E] [StarRing E] [CStarRing E] [NormedAlgebra 𝕜 E] [StarModule 𝕜 E].

TODO #

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} :
    ∀ {inst : SeminormedAddCommGroup E} {inst_1 : StarAddMonoid E} [self : NormedStarGroup E] (x : E), star x = x

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

    Equations
    • starNormedAddGroupHom = { toFun := starAddEquiv.toFun, map_add' := , bound' := }
    Instances For

      The star map in a normed star group is an isometry

      @[instance 100]
      Equations
      • =

      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.

      Instances
        theorem CStarRing.norm_mul_self_le {E : Type u_4} :
        ∀ {inst : NonUnitalNormedRing E} {inst_1 : StarRing E} [self : CStarRing E] (x : E), x * x star x * x
        @[deprecated CStarRing]

        Alias of CStarRing.


        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.

        Equations
        Instances For
          @[instance 100]

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

          Equations
          • =
          @[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
          @[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
          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} [NonUnitalNormedRing R₁] [StarRing R₁] [CStarRing R₁] [NonUnitalNormedRing R₂] [StarRing R₂] [CStarRing R₂] :
          CStarRing (R₁ × R₂)
          Equations
          • =
          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)
          Equations
          • =
          instance Pi.cstarRing' {ι : Type u_4} {R₁ : Type u_5} [NonUnitalNormedRing R₁] [StarRing R₁] [CStarRing R₁] [Fintype ι] :
          CStarRing (ιR₁)
          Equations
          • =
          @[simp]
          theorem CStarRing.norm_one {E : Type u_2} [NormedRing E] [StarRing E] [CStarRing E] [Nontrivial E] :
          @[instance 100]
          Equations
          • =
          theorem CStarRing.norm_coe_unitary {E : Type u_2} [NormedRing E] [StarRing E] [CStarRing E] [Nontrivial E] (U : (unitary E)) :
          U = 1
          @[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) :
          @[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
          @[simp]
          theorem CStarRing.norm_unitary_smul {E : Type u_2} [NormedRing E] [StarRing E] [CStarRing E] (U : (unitary E)) (A : E) :
          theorem CStarRing.norm_mem_unitary_mul {E : Type u_2} [NormedRing E] [StarRing E] [CStarRing E] {U : E} (A : E) (hU : U unitary E) :
          @[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
          theorem CStarRing.norm_mul_mem_unitary {E : Type u_2} [NormedRing E] [StarRing E] [CStarRing E] (A : E) {U : E} (hU : U unitary E) :
          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
          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
          def starₗᵢ (𝕜 : Type u_1) {E : Type u_2} [CommSemiring 𝕜] [StarRing 𝕜] [SeminormedAddCommGroup E] [StarAddMonoid E] [NormedStarGroup E] [Module 𝕜 E] [StarModule 𝕜 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
            @[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
            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
            @[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 𝕜
            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
            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) :
            Equations
            • =