MatrixLiftConjugation.lean`

19 declarations, 0 contain sorry, 0 declared as axioms

Conjugating finite-matrix lifts by a diagonal unitary

Conjugating the inner matrix units changes only the finite matrix algebra in which a representative lies. Both the concrete embedding and its bounded sequence version respect this conjugation exactly.

def OAI.KadisonKastler.conjugatedMatrixUnits line 34
Source documentation
Map the chosen matrix units under the inner star automorphism.
```
def conjugatedMatrixUnits (E : Generator.MatrixUnitSystem ι A) (z : unitary A) :
    Generator.MatrixUnitSystem ι A :=
…
```
Mentions: OAI.Generator.MatrixUnitSystem
theorem OAI.KadisonKastler.conjugatedMatrixUnits_entry line 39
theorem OAI.KadisonKastler.matrixUnitsEmbedding_map_hom line 44
Source documentation
Matrix-unit embeddings commute with every star algebra homomorphism.
```
theorem matrixUnitsEmbedding_map_hom (E : Generator.MatrixUnitSystem ι A)
    (φ : A →⋆ₐ[ℂ] B) (x : CStarMatrix ι ι ℂ) :
    matrixUnitsEmbedding (E.map φ) x = φ (matrixUnitsEmbedding E x) := by
…
```
Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.matrixUnitsEmbedding
theorem OAI.KadisonKastler.matrixScalarHom_mul_apply line 51
theorem OAI.KadisonKastler.mul_matrixScalarHom_apply line 57

theorem OAI.KadisonKastler.coefficientMatrixMap_inner line 63

Source documentation

Diagonal conjugation is entrywise conjugation.

theorem coefficientMatrixMap_inner (z : unitary A) (x : CStarMatrix κ κ A) :
    coefficientMatrixMap (Unitary.conjStarAlgAut ℂ A z).toStarAlgHom x =
      matrixScalarHom (z : A) * x * star (matrixScalarHom (z : A)) := by
…

Mentions: OAI.KadisonKastler.coefficientMatrixMap, OAI.KadisonKastler.matrixScalarHom

theorem OAI.KadisonKastler.coefficientMatrixMap_conjugatedMatrixUnits line 73

Source documentation

The matrix-coefficient embeddings transform by the same diagonal conjugation.

theorem coefficientMatrixMap_conjugatedMatrixUnits
    (E : Generator.MatrixUnitSystem ι A) (z : unitary A)
    (x : CStarMatrix κ κ (CStarMatrix ι ι ℂ)) :
    coefficientMatrixMap (matrixUnitsEmbedding (conjugatedMatrixUnits E z)) x =
      matrixScalarHom (z : A) * coefficientMatrixMap (matrixUnitsEmbedding E) x *
        star (matrixScalarHom (z : A)) := by
…

Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.coefficientMatrixMap, OAI.KadisonKastler.matrixUnitsEmbedding, OAI.KadisonKastler.conjugatedMatrixUnits, OAI.KadisonKastler.matrixScalarHom

def OAI.KadisonKastler.concreteDiagonalUnitary line 94
Source documentation
The concrete diagonal amplification of an inner unitary.
```
def concreteDiagonalUnitary (z : unitary (Algebra M)) :
    unitary (Algebra (matrixVonNeumann (ι := Fin n) M)) :=
…
```
Mentions: OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann
theorem OAI.KadisonKastler.concreteDiagonalUnitary_coe line 101
theorem OAI.KadisonKastler.finiteMatrixEmbedding_conjugatedMatrixUnits line 108
Source documentation
Conjugation by the concrete diagonal unitary is exactly the finite embedding made from the conjugated inner matrix units.
```
theorem finiteMatrixEmbedding_conjugatedMatrixUnits
    (E : Generator.MatrixUnitSystem (Fin (j + 1)) (Algebra M))
    (z : unitary (Algebra M)) (x : FiniteMatrixModel n j) :
    finiteMatrixEmbedding (conjugatedMatrixUnits E z) x =
      (concreteDiagonalUnitary (n := n) z : Algebra (matrixVonNeumann (ι := Fin n) M)) *
…
```
Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.FiniteMatrixModel, OAI.KadisonKastler.finiteMatrixEmbedding, OAI.KadisonKastler.conjugatedMatrixUnits, OAI.KadisonKastler.concreteDiagonalUnitary, OAI.KadisonKastler.matrixVonNeumann
def OAI.KadisonKastler.matrixLiftUnitaryAt line 121
Source documentation
The coordinate unitary of a bounded unitary sequence.
```
def matrixLiftUnitaryAt (z : unitary (BoundedSequence (Algebra M))) (k : ℕ) :
    unitary (Algebra M) :=
…
```
Mentions: OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.Algebra
theorem OAI.KadisonKastler.matrixLiftUnitaryAt_coe line 126
def OAI.KadisonKastler.conjugatedMatrixUnitsSequence line 130
Source documentation
Conjugated matrix units are chosen separately at every coordinate.
```
def conjugatedMatrixUnitsSequence
    (E : ∀ k, Generator.MatrixUnitSystem (Fin (k + 1)) (Algebra M))
    (z : unitary (BoundedSequence (Algebra M)))
    (k : ℕ) : Generator.MatrixUnitSystem (Fin (k + 1)) (Algebra M) :=
…
```
Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.BoundedSequence
def OAI.KadisonKastler.concreteDiagonalSequence line 137
Source documentation
The diagonal bounded sequence, represented on the concrete Hilbert matrix space.
```
def concreteDiagonalSequence (z : BoundedSequence (Algebra M)) :
    BoundedSequence (Algebra (matrixVonNeumann (ι := Fin n) M)) :=
…
```
Mentions: OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann
theorem OAI.KadisonKastler.concreteDiagonalSequence_apply line 143
def OAI.KadisonKastler.concreteDiagonalSequenceUnitary line 152
Source documentation
The diagonal sequence remains an actual unitary before passing to a quotient.
```
def concreteDiagonalSequenceUnitary (z : unitary (BoundedSequence (Algebra M))) :
    unitary (BoundedSequence (Algebra (matrixVonNeumann (ι := Fin n) M))) :=
…
```
Mentions: OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann
theorem OAI.KadisonKastler.concreteDiagonalSequenceUnitary_coe line 160
theorem OAI.KadisonKastler.finiteMatrixSequence_conjugatedMatrixUnits line 167
Source documentation
The second unitary lift preserves the exact finite-matrix representative form.
```
theorem finiteMatrixSequence_conjugatedMatrixUnits
    (E : ∀ k, Generator.MatrixUnitSystem (Fin (k + 1)) (Algebra M))
    (z : unitary (BoundedSequence (Algebra M)))
    (x : VaryingBoundedSequence (FiniteMatrixModel n)) :
    varyingSequenceMap (fun k => finiteMatrixEmbedding (n := n)
…
```
Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.VaryingBoundedSequence, OAI.KadisonKastler.FiniteMatrixModel, OAI.KadisonKastler.varyingSequenceMap, OAI.KadisonKastler.finiteMatrixEmbedding
theorem OAI.KadisonKastler.finiteMatrixSequence_conjugatedMatrixUnits_quotient line 186
Source documentation
The same identity descends through any star quotient of the bounded sequences.
```
theorem finiteMatrixSequence_conjugatedMatrixUnits_quotient
    {Q : Type*} [CStarAlgebra Q]
    (π : BoundedSequence (Algebra (matrixVonNeumann (ι := Fin n) M)) →⋆ₐ[ℂ] Q)
…
```
Mentions: OAI.KadisonKastler.BoundedSequence, OAI.KadisonKastler.Algebra, OAI.KadisonKastler.matrixVonNeumann