TypeIEmbedding.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Constructed near inclusions for represented type I factors

Finite signed permutation groups, or their increasing union in the countable case, generate the minimal cyclic representation. Weak generation transports back to the original representation before applying the group correction.

theorem OAI.KadisonKastler.exists_unitary_typeI_embedding line 25

Source documentation

The type I embedding needed by stability, constructed without the general amenable embedding input.

theorem exists_unitary_typeI_embedding {M N : VonNeumannAlgebra H}
    (hM : IsTypeIFactor 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.IsTypeIFactor, OAI.KadisonKastler.NearInclusion, OAI.KadisonKastler.unitaryConj