Physicslib4.Analysis.CStarDenseExtend

Extending a *-homomorphism from a dense *-subalgebra

This file proves the analytic core needed to lift fiberwise actions to a quasilocal C*-algebra: a uniformly continuous *-homomorphism defined on a dense *-subalgebra S of a C*-algebra A, valued in a (complete) C*-algebra B, extends to a *-homomorphism on all of A.

Main results

• Physicslib4.exists_starAlgHom_extend_of_dense: existence of the extension F : A →⋆ₐ[ℂ] B agreeing with f on S.

The construction uses the uniform-space extension of a uniformly continuous map to a complete codomain (uniformContinuous_uniformly_extend); all algebraic structure (+, *, 1, 0, ℂ-scaling, star) is transported to the extension by continuity and agreement on the dense subalgebra.

theorem Physicslib4.exists_starAlgHom_extend_of_dense {A : Type u_1} {B : Type u_2} [CStarAlgebra A] [CStarAlgebra B] (S : StarSubalgebra ℂ A) (hS : Dense ↑S) (f : ↥S →⋆ₐ[ℂ] B) (hf : UniformContinuous ⇑f) : ∃ (F : A →⋆ₐ[ℂ] B), Continuous ⇑F ∧ ∀ (x : ↥S), F ↑x = f x

A uniformly continuous *-homomorphism from a dense *-subalgebra S of a C*-algebra A into a C*-algebra B extends to a *-homomorphism on all of A, agreeing with the original on S.