CountablyGeneratedCStarAlgebra.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

A separable C-star algebra generating a separably represented algebra

The complex linear span of the words in a countable family and its adjoints is separable. Its norm closure is therefore a separable C-star algebra. Applying this to the countable weakly dense contraction tests gives an actual norm-separable C-star subalgebra whose bicommutant is the original von Neumann algebra.

theorem OAI.KadisonSimilarity.isSeparable_starAlgebra_adjoin line 26
Source documentation
Words in a countable generating set and its adjoints span a separable complex star algebra.
```
theorem isSeparable_starAlgebra_adjoin {s : Set A} (hs : s.Countable) :
    TopologicalSpace.IsSeparable (StarAlgebra.adjoin ℂ s : Set A) := by
…
```
abbrev OAI.KadisonSimilarity.sequenceGeneratedCStarAlgebra line 42
Source documentation
The concrete norm-closed C-star algebra generated by a sequence.
```
abbrev sequenceGeneratedCStarAlgebra (g : ℕ → A) : StarSubalgebra ℂ A :=
…
```
instance OAI.KadisonSimilarity.sequenceGeneratedCStarAlgebra_isClosed line 45
instance OAI.KadisonSimilarity.sequenceGeneratedCStarAlgebra_separable line 49
theorem OAI.KadisonSimilarity.mem_sequenceGeneratedCStarAlgebra line 54
theorem OAI.KadisonSimilarity.mem_vonNeumannAlgebra_of_mem_weakClosure line 63
Source documentation
A concrete von Neumann algebra contains the weak closure of any of its subsets, proved directly from commutation with its commutant.
```
theorem mem_vonNeumannAlgebra_of_mem_weakClosure
    (P : VonNeumannAlgebra H) (S : Set (H →L[ℂ] H)) (hS : S ⊆ P)
    (T : H →L[ℂ] H) (hT : ofCLM T ∈ closure (ofCLM '' S)) : T ∈ P := by
…
```

theorem OAI.KadisonSimilarity.representationVonNeumannAlgebra_subtype_eq_of_dense_tests line 78

Source documentation

A norm-closed star subalgebra contained in P, containing a weakly dense family of contractions, has bicommutant exactly P.

theorem representationVonNeumannAlgebra_subtype_eq_of_dense_tests
    (P : VonNeumannAlgebra H) (B : StarSubalgebra ℂ (H →L[ℂ] H))
    [IsClosed (B : Set (H →L[ℂ] H))]
    (hB : B ≤ P.toStarSubalgebra) (g : ℕ → H →L[ℂ] H) (hg : ∀ n, g n ∈ B)
    (hdense : ∀ T : H →L[ℂ] H, T ∈ P → ‖T‖ ≤ 1 →
      ofCLM T ∈ closure (Set.range fun n => ofCLM (g n))) :
    representationVonNeumannAlgebra B.subtype = P := by
…

Mentions: OAI.KadisonSimilarity.representationVonNeumannAlgebra

theorem OAI.KadisonSimilarity.exists_separable_generating_cstar_subalgebra line 123

Source documentation

Every concretely separably represented von Neumann algebra is the bicommutant of an actual norm-separable unital C-star subalgebra.

theorem exists_separable_generating_cstar_subalgebra
    [TopologicalSpace.SeparableSpace H] (P : VonNeumannAlgebra H) :
    ∃ B : StarSubalgebra ℂ (H →L[ℂ] H),
      IsClosed (B : Set (H →L[ℂ] H)) ∧ TopologicalSpace.SeparableSpace B ∧
      B ≤ P.toStarSubalgebra ∧ (starSubalgebraCommutant B).commutant = P := by
…

Mentions: OAI.KadisonSimilarity.starSubalgebraCommutant