FiniteMatrixEmbedding.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Embedding a nearby full matrix algebra

A finite signed permutation group spans the matrix entries. Correcting that group therefore moves the whole matrix algebra into the neighbour. The displacement bound is independent of the matrix size.

def OAI.KadisonKastler.matrixSystemOfUnits line 24
Source documentation
The same concrete matrix units in the signed-group construction.
```
def matrixSystemOfUnits (E : Generator.MatrixUnitSystem (Fin n) (Algebra M)) :
    HochschildMatrixSystems.MatrixSystem (Algebra M) n where
…
```
Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.Algebra, OAI.HochschildMatrixSystems.MatrixSystem
theorem OAI.KadisonKastler.exists_unitary_matrixStage_embedding line 33
Source documentation
A full matrix stage in a one-sided near inclusion is unitarily embedded in the neighbouring algebra, with a dimension-independent bound.
```
theorem exists_unitary_matrixStage_embedding
    (E : Generator.MatrixUnitSystem (Fin n) (Algebra M)) {γ : ℝ}
    (hγ : 0 ≤ γ) (hsmall : γ ≤ 1 / 1152) (hnear : NearInclusion M N γ) :
    ∃ w : unitary (H →L[ℂ] H),
      (∀ x ∈ E.concreteAlgebra, unitaryConj w x ∈ N) ∧
      ‖(w : H →L[ℂ] H) - 1‖ ≤ 84 * γ := by
…
```
Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.NearInclusion, OAI.KadisonKastler.unitaryConj

theorem OAI.KadisonKastler.exists_unitary_finiteMatrix_embedding line 72

Source documentation

The preceding construction for an entire represented full matrix algebra.

theorem exists_unitary_finiteMatrix_embedding
    (E : Generator.MatrixUnitSystem (Fin n) (Algebra M))
    (hE : Function.Surjective E.hom) {γ : ℝ}
    (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.Generator.MatrixUnitSystem, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.NearInclusion, OAI.KadisonKastler.unitaryConj