MatrixChainEmbedding.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Embedding an increasing full-matrix closure

Compatible frames give an increasing sequence of finite unitary groups. Their union generates the original von Neumann algebra, so its invariant mean provides a single simultaneous embedding of the entire closure.

def OAI.KadisonKastler.increasingSubgroupUnion line 20
Source documentation
The union of a monotone sequence of subgroups, as a subgroup.
```
def increasingSubgroupUnion (K : ℕ → Subgroup U) (hK : Monotone K) : Subgroup U where
…
```
def OAI.KadisonKastler.increasingUnionStage line 32
Source documentation
The original stages, regarded inside their union.
```
def increasingUnionStage (K : ℕ → Subgroup U) (hK : Monotone K) (n : ℕ) :
    Subgroup (increasingSubgroupUnion K hK) :=
…
```
Mentions: OAI.KadisonKastler.increasingSubgroupUnion
instance OAI.KadisonKastler.increasingUnionStage_finite line 36
theorem OAI.KadisonKastler.increasingUnionStage_monotone line 41
theorem OAI.KadisonKastler.increasingUnionStage_covers line 46
def OAI.KadisonKastler.subgroupAlgebraRepresentation line 53
Source documentation
Regard an ambient unitary subgroup contained in an algebra as internal unitaries.
```
def subgroupAlgebraRepresentation (G : Subgroup (unitary (H →L[ℂ] H)))
    (M : VonNeumannAlgebra H) (hG : ∀ u : G, (u : H →L[ℂ] H) ∈ M) :
    G →* unitary (Algebra M) where
…
```
Mentions: OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.matrixChainGroup_mem line 63
Source documentation
Every element of the finite-group union belongs to the original matrix closure.
```
theorem matrixChainGroup_mem (F : ∀ n, FullMatrixFrame (A n)) (hA : Monotone A)
    (u : increasingSubgroupUnion
      (fun n => (compatibleMatrixFrames F hA n).group)
      (compatibleMatrixFrames_group_monotone F hA)) :
    (u : H →L[ℂ] H) ∈ generatedVonNeumannAlgebra (⨆ n, A n) := by
…
```
Mentions: OAI.KadisonKastler.FullMatrixFrame, OAI.KadisonKastler.increasingSubgroupUnion, OAI.KadisonKastler.compatibleMatrixFrames, OAI.KadisonKastler.compatibleMatrixFrames_group_monotone, OAI.KadisonKastler.generatedVonNeumannAlgebra
theorem OAI.KadisonKastler.matrixChainGroup_generates line 73
Source documentation
The increasing union of finite frame groups generates the entire matrix closure.
```
theorem matrixChainGroup_generates (F : ∀ n, FullMatrixFrame (A n)) (hA : Monotone A) :
    generatedVonNeumannAlgebra (StarAlgebra.adjoin ℂ (Set.range (fun u =>
      (subgroupAlgebraRepresentation _ _ (matrixChainGroup_mem F hA) u : H →L[ℂ] H)))) =
      generatedVonNeumannAlgebra (⨆ n, A n) := by
…
```
Mentions: OAI.KadisonKastler.FullMatrixFrame, OAI.KadisonKastler.generatedVonNeumannAlgebra, OAI.KadisonKastler.subgroupAlgebraRepresentation, OAI.KadisonKastler.matrixChainGroup_mem

theorem OAI.KadisonKastler.exists_unitary_matrixChain_embedding line 105

Source documentation

The whole increasing matrix closure embeds with a dimension-independent near-identity bound. No injectivity or amenable embedding hypothesis is used.

theorem exists_unitary_matrixChain_embedding
    (F : ∀ n, FullMatrixFrame (A n)) (hA : Monotone A)
    {N : VonNeumannAlgebra H} {γ : ℝ} (hγ : 0 ≤ γ) (hsmall : γ ≤ 1 / 1152)
    (hnear : NearInclusion (generatedVonNeumannAlgebra (⨆ n, A n)) N γ) :
    ∃ w : unitary (H →L[ℂ] H),
      (∀ x ∈ generatedVonNeumannAlgebra (⨆ n, A n), unitaryConj w x ∈ N) ∧
      ‖(w : H →L[ℂ] H) - 1‖ ≤ 84 * γ := by
…

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