OAI/Analysis/KadisonKastler/NearSeparableGenerators.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Nearby separable C-star algebras generating the original pair

In a separable representation, the alternating construction can retain countable strong generators of both original algebras. This supplies the norm-separable algebras needed for simultaneous fiber representations.

  1. theorem OAI.KadisonKastler.generated_eq_of_strong_tests line 23
  2. theorem OAI.KadisonKastler.exists_near_separable_generators line 49
  3. theorem OAI.KadisonKastler.exists_norm_dense_unitBall_sequence line 67
  4. theorem OAI.KadisonKastler.exists_closed_separable_common_superalgebra line 79
  5. theorem OAI.KadisonKastler.exists_closed_separable_common_superalgebra_in line 92

    Source documentation

    The common separable algebra can be chosen inside any common ambient von Neumann algebra, in particular inside the common central commutant.

    theorem exists_closed_separable_common_superalgebra_in
    (A B : StarSubalgebra ℂ (H →L[ℂ] H)) (D : VonNeumannAlgebra H)
    (hA : IsSeparable (A : Set (H →L[ℂ] H)))
    (hB : IsSeparable (B : Set (H →L[ℂ] H)))
    (hAD : A ≤ D.toStarSubalgebra) (hBD : B ≤ D.toStarSubalgebra) :
    ∃ C : StarSubalgebra ℂ (H →L[ℂ] H),
      IsClosed (C : Set (H →L[ℂ] H)) ∧ IsSeparable (C : Set (H →L[ℂ] H)) ∧
      A ≤ C ∧ B ≤ C ∧ C ≤ D.toStarSubalgebra := by
…