IncreasingGroupEmbedding.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Embedding a weakly generated locally finite group algebra

The group correction is simultaneous on the entire group. Bicommutant generation then passes its inclusion into the target to the full algebra.

theorem OAI.KadisonKastler.exists_unitary_embedding_of_invariant_group line 21

Source documentation

Near inclusion embeds a von Neumann algebra weakly generated by a unitary representation of a group carrying the supplied invariant mean.

theorem exists_unitary_embedding_of_invariant_group
    (m : ScalarInvariantMean G) {M N : VonNeumannAlgebra H}
    (U : G →* unitary (Algebra M))
    (hgen : generatedVonNeumannAlgebra
      (StarAlgebra.adjoin ℂ (Set.range (fun g => (U g : H →L[ℂ] H)))) = M)
    {γ : ℝ} (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.ScalarInvariantMean, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.generatedVonNeumannAlgebra, OAI.KadisonKastler.NearInclusion, OAI.KadisonKastler.unitaryConj

theorem OAI.KadisonKastler.exists_unitary_embedding_of_increasing_finite_groups line 51

Source documentation

The invariant mean is constructed from the increasing finite subgroups; no amenability hypothesis is retained.

theorem exists_unitary_embedding_of_increasing_finite_groups
    (K : ℕ → Subgroup G) [∀ n, Finite (K n)] (hmono : Monotone K)
    (hcover : ∀ g : G, ∃ n, g ∈ K n) {M N : VonNeumannAlgebra H}
    (U : G →* unitary (Algebra M))
    (hgen : generatedVonNeumannAlgebra
      (StarAlgebra.adjoin ℂ (Set.range (fun g => (U g : H →L[ℂ] H)))) = M)
    {γ : ℝ} (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 * γ :=
…

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