OAI/Analysis/KadisonSimilarity/Representation/CountableDenseStarSubring.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Countable dense star subrings

A separable complex C-star algebra has a countable norm-dense subring, closed under star and containing the scalar i. This supplies the domain on which countably many almost-everywhere algebra identities suffice.

  1. theorem OAI.KadisonSimilarity.countable_subringClosure line 18
  2. theorem OAI.KadisonSimilarity.star_mem_subringClosure_union line 26
  3. theorem OAI.KadisonSimilarity.exists_countable_dense_star_subring line 42

    Source documentation

    A concrete countable domain for gathering the pointwise fiber laws.

    theorem exists_countable_dense_star_subring (A : Type*) [CStarAlgebra A]
    [TopologicalSpace.SeparableSpace A] :
    ∃ S : Subring A, (S : Set A).Countable ∧ Dense (S : Set A) ∧
      (∀ a ∈ S, star a ∈ S) ∧ algebraMap ℂ A Complex.I ∈ S := by
…