DenseStarRepresentation.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Extending the pointwise algebra in a fiber

This is the norm-continuity step in Blackadar, III.5.1.11. A contractive unital ring representation on a dense subring extends to the C-star algebra. Preservation of star and of i · 1 makes that extension a complex star representation. Countability is needed only to gather almost-everywhere relations on a common conull set, not for the extension itself.

theorem OAI.KadisonSimilarity.denseSubring_uniformContinuous line 25

def OAI.KadisonSimilarity.denseSubringRepresentation line 33

Source documentation

The uniform extension, retaining its ring structure.

def denseSubringRepresentation (S : Subring A) (hdense : Dense (S : Set A))
    (f : S →+* (H →L[ℂ] H)) (hnorm : ∀ a : S, ‖f a‖ ≤ ‖a‖) :
    A →+* (H →L[ℂ] H) :=
…

theorem OAI.KadisonSimilarity.denseSubringRepresentation_continuous line 40
theorem OAI.KadisonSimilarity.denseSubringRepresentation_apply line 48

theorem OAI.KadisonSimilarity.continuousRingHom_commutes_complex line 59

Source documentation

Continuity of an additive map gives real linearity; preserving i · 1 then forces preservation of every complex scalar.

theorem continuousRingHom_commutes_complex
    (F : A →+* (H →L[ℂ] H)) (hF : Continuous F)
    (hI : F (algebraMap ℂ A Complex.I) = algebraMap ℂ (H →L[ℂ] H) Complex.I) :
    ∀ z : ℂ, F (algebraMap ℂ A z) = algebraMap ℂ (H →L[ℂ] H) z := by
…

theorem OAI.KadisonSimilarity.exists_starRepresentation_of_ring_extension line 85

Source documentation

A continuous ring extension is a complex star representation when its dense restriction preserves star and the scalar i.

theorem exists_starRepresentation_of_ring_extension
    (S : Subring A) (hdense : Dense (S : Set A))
    (hstarS : ∀ a ∈ S, star a ∈ S) (hIS : algebraMap ℂ A Complex.I ∈ S)
    (f : S →+* (H →L[ℂ] H)) (F : A →+* (H →L[ℂ] H))
    (hF : Continuous F) (hext : ∀ a : S, F a = f a)
    (hstar : ∀ a : S, f ⟨star a.val, hstarS a.val a.property⟩ = star (f a))
    (hI : f ⟨algebraMap ℂ A Complex.I, hIS⟩ = algebraMap ℂ (H →L[ℂ] H) Complex.I) :
    ∃ σ : A →⋆ₐ[ℂ] (H →L[ℂ] H), ∀ a : S, σ a = f a := by
…

theorem OAI.KadisonSimilarity.exists_starRepresentation_of_dense_subring line 115

Source documentation

A contractive unital ring representation on a dense star subring extends to a complex star representation when it preserves the scalar i.

theorem exists_starRepresentation_of_dense_subring
    (S : Subring A) (hdense : Dense (S : Set A))
    (hstarS : ∀ a ∈ S, star a ∈ S) (hIS : algebraMap ℂ A Complex.I ∈ S)
    (f : S →+* (H →L[ℂ] H)) (hnorm : ∀ a : S, ‖f a‖ ≤ ‖a‖)
    (hstar : ∀ a : S, f ⟨star a.val, hstarS a.val a.property⟩ = star (f a))
    (hI : f ⟨algebraMap ℂ A Complex.I, hIS⟩ = algebraMap ℂ (H →L[ℂ] H) Complex.I) :
    ∃ σ : A →⋆ₐ[ℂ] (H →L[ℂ] H), ∀ a : S, σ a = f a :=
…

theorem OAI.KadisonSimilarity.starRepresentation_ext_dense_subring line 128

Source documentation

An extension from a norm-dense subring is unique.

theorem starRepresentation_ext_dense_subring
    (S : Subring A) (hdense : Dense (S : Set A))
    (σ ρ : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (h : ∀ a : S, σ a = ρ a) : σ = ρ := by
…