JointCStarSource.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

A common separable source for an algebra and its commutant

Taking the norm closure of the joint star algebra preserves norm separability. When the two sources generate P and P', the common source generates the commutant of the center. This puts both sources in one fiber representation.

abbrev OAI.KadisonSimilarity.jointCStarSource line 21
Source documentation
The norm-closed star algebra containing the two given sources.
```
abbrev jointCStarSource (B C : StarSubalgebra ℂ A) : StarSubalgebra ℂ A :=
…
```
instance OAI.KadisonSimilarity.jointCStarSource_isClosed line 24
theorem OAI.KadisonSimilarity.le_jointCStarSource_left line 28
theorem OAI.KadisonSimilarity.le_jointCStarSource_right line 32
theorem OAI.KadisonSimilarity.jointCStarSource_minimal line 36

theorem OAI.KadisonSimilarity.jointCStarSource_eq_dense_generators line 43

Source documentation

Countable dense subsets of the two algebras already generate their joint norm closure.

theorem jointCStarSource_eq_dense_generators
    (B C : StarSubalgebra ℂ A)
    (b : ℕ → B) (hb : DenseRange b) (c : ℕ → C) (hc : DenseRange c) :
    jointCStarSource B C =
      (StarAlgebra.adjoin ℂ
        (Set.range (fun n => (b n : A)) ∪ Set.range (fun n => (c n : A)))).topologicalClosure := by
…

Mentions: OAI.KadisonSimilarity.jointCStarSource

instance OAI.KadisonSimilarity.jointCStarSource_separable line 72
theorem OAI.KadisonSimilarity.source_commutant_eq line 84

theorem OAI.KadisonSimilarity.jointCStarSource_commutant line 92

Source documentation

The joint source has exactly the original center as commutant.

theorem jointCStarSource_commutant
    (P : VonNeumannAlgebra H) (B C : StarSubalgebra ℂ (H →L[ℂ] H))
    (hB : B ≤ P.toStarSubalgebra) (hC : C ≤ P.commutant.toStarSubalgebra)
    (hBgen : (starSubalgebraCommutant B).commutant = P)
    (hCgen : (starSubalgebraCommutant C).commutant = P.commutant) :
    starSubalgebraCommutant (jointCStarSource B C) = vonNeumannCenter P := by
…

Mentions: OAI.KadisonSimilarity.starSubalgebraCommutant, OAI.KadisonSimilarity.jointCStarSource, OAI.KadisonSimilarity.vonNeumannCenter

theorem OAI.KadisonSimilarity.jointCStarSource_bicommutant line 140

theorem OAI.KadisonSimilarity.exists_separable_joint_cstar_source line 151

Source documentation

Simultaneously choose weak generators for the algebra and commutant, with a norm-separable common source generating the central commutant.

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

Mentions: OAI.KadisonSimilarity.starSubalgebraCommutant, OAI.KadisonSimilarity.jointCStarSource, OAI.KadisonSimilarity.vonNeumannCenter