FullCornerEmbedding.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Constructed embeddings of countable scalar matrix algebras

def OAI.KadisonKastler.FullMatrixCorner.signedGroupUnion line 20
Source documentation
The locally finite group carried by the countable matrix units.
```
def signedGroupUnion : Subgroup (unitary (H →L[ℂ] H)) :=
…
```
theorem OAI.KadisonKastler.FullMatrixCorner.signedGroupUnion_mem line 23

theorem OAI.KadisonKastler.FullMatrixCorner.signedGroupUnion_generates line 30

Source documentation

The finite signed groups generate exactly the scalar matrix algebra.

theorem signedGroupUnion_generates :
    generatedVonNeumannAlgebra (StarAlgebra.adjoin ℂ (Set.range (fun u =>
      (subgroupAlgebraRepresentation F.signedGroupUnion F.scalarMatrixAlgebra
        F.signedGroupUnion_mem u : H →L[ℂ] H)))) = F.scalarMatrixAlgebra := by
…

Mentions: OAI.KadisonKastler.generatedVonNeumannAlgebra, OAI.KadisonKastler.subgroupAlgebraRepresentation

theorem OAI.KadisonKastler.FullMatrixCorner.exists_localized_embedding line 52

Source documentation

A single near-identity unitary embeds all countably many matrix entries. Its location is retained in the algebra generated by the source and target.

theorem exists_localized_embedding (M N : VonNeumannAlgebra H)
    (hF : ∀ i j, F.entry i j ∈ M) {γ : ℝ}
    (hγ : 0 ≤ γ) (hsmall : γ ≤ 1 / 1152) (hnear : NearInclusion M N γ) :
    ∃ w : unitary (H →L[ℂ] H),
      (w : H →L[ℂ] H) ∈ generatedVonNeumannAlgebra (M.toStarSubalgebra ⊔ N.toStarSubalgebra) ∧
      (∀ i j, unitaryConj w (F.entry i j) ∈ N) ∧
      ‖(w : H →L[ℂ] H) - 1‖ ≤ 84 * γ := by
…

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