Documentation

TauCeti.Analysis.CStarAlgebra.Hom

Topological properties of C⋆-algebra homomorphisms and equivalences #

A ⋆-algebra homomorphism between complex C⋆-algebras is automatically continuous, so its two-sided ideal kernel is closed (NonUnitalStarAlgHom.isClosed_ker, StarAlgHom.isClosed_ker). A ⋆-algebra equivalence of complex C⋆-algebras is isometric (StarAlgEquiv.isometry), so it bundles as a continuous linear equivalence StarAlgEquiv.toContinuousLinearEquiv.

source
instance NonUnitalStarAlgHom.isClosed_ker {A : Type u_1} {B : Type u_2} [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] (φ : A →⋆ₙₐ[ℂ] B) :
IsClosed ↑(TwoSidedIdeal.ker φ)

The two-sided ideal kernel of any ⋆-homomorphism between C⋆-algebras is closed.

source
instance StarAlgHom.isClosed_ker {A : Type u_1} {B : Type u_2} [CStarAlgebra A] [CStarAlgebra B] (φ : A →⋆ₐ[ℂ] B) :
IsClosed ↑(TwoSidedIdeal.ker φ)

The two-sided ideal kernel of any unital ⋆-homomorphism between C⋆-algebras is closed.

source
def StarAlgEquiv.toContinuousLinearEquiv {A : Type u_1} {B : Type u_2} [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] (e : A ≃⋆ₐ[ℂ] B) :
A ≃L[ℂ] B

A star-algebra equivalence of C⋆-algebras as a continuous linear equivalence. Both directions are continuous because star-algebra equivalences of C⋆-algebras are isometric.

Instances For
    source
    @[simp]
    theorem StarAlgEquiv.coe_toContinuousLinearEquiv {A : Type u_1} {B : Type u_2} [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] (e : A ≃⋆ₐ[ℂ] B) :
    ⇑e.toContinuousLinearEquiv = ⇑e
    source
    @[simp]
    theorem StarAlgEquiv.toContinuousLinearEquiv_symm {A : Type u_1} {B : Type u_2} [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B] (e : A ≃⋆ₐ[ℂ] B) :
    e.toContinuousLinearEquiv.symm = e.symm.toContinuousLinearEquiv