AbelianEmbedding.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Constructed embeddings for commutative von Neumann algebras

theorem OAI.KadisonKastler.generated_internal_unitaries line 17
Source documentation
All internal unitaries generate the represented algebra.
```
theorem generated_internal_unitaries (M : VonNeumannAlgebra H) :
    generatedVonNeumannAlgebra (StarAlgebra.adjoin ℂ
      (Set.range (fun u : unitary (Algebra M) => (u : H →L[ℂ] H)))) = M := by
…
```
Mentions: OAI.KadisonKastler.generatedVonNeumannAlgebra, OAI.KadisonKastler.Algebra

theorem OAI.KadisonKastler.exists_unitary_abelian_embedding line 42

Source documentation

The abelian unitary group mean gives an actual embedding, without an injectivity or published amenable-embedding premise.

theorem exists_unitary_abelian_embedding {M N : VonNeumannAlgebra H}
    (hcomm : ∀ x y : Algebra M, x * y = y * x)
    {γ : ℝ} (hγ : 0 ≤ γ) (hsmall : γ ≤ 1 / 1152) (hnear : NearInclusion M N γ) :
    ∃ w : unitary (H →L[ℂ] H), (∀ x ∈ M, unitaryConj w x ∈ N) ∧
      ‖(w : H →L[ℂ] H) - 1‖ ≤ 84 * γ := by
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.NearInclusion, OAI.KadisonKastler.unitaryConj

theorem OAI.KadisonKastler.exists_abelian_conjugacy_of_kkDistance_lt line 56

Source documentation

At small ordinary distance the constructed inclusion is onto.

theorem exists_abelian_conjugacy_of_kkDistance_lt {M N : VonNeumannAlgebra H}
    (hcomm : ∀ x y : Algebra M, x * y = y * x)
    {γ : ℝ} (hγ : γ ≤ 1 / 1152) (hgap : kkDistance M N < γ) :
    ∃ w : unitary (H →L[ℂ] H), Conjugates w M N ∧
      ‖(w : H →L[ℂ] H) - 1‖ ≤ 84 * γ := by
…

Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.kkDistance, OAI.KadisonKastler.Conjugates