MatrixCommutant.lean`

7 declarations, 0 contain sorry, 0 declared as axioms

The commutant of the scalar matrix copy

Commuting with all scalar matrix units forces a matrix over any complex C⋆-algebra to be a constant diagonal matrix. The corresponding statement for unitaries retains an actual unitary coefficient.

def OAI.KadisonKastler.matrixScalarHom line 19
Source documentation
The constant diagonal copy of the coefficient algebra.
```
def matrixScalarHom : A →⋆ₐ[ℂ] CStarMatrix ι ι A :=
…
```
theorem OAI.KadisonKastler.matrixScalarHom_apply line 29
theorem OAI.KadisonKastler.matrixScalarHom_injective line 32

theorem OAI.KadisonKastler.coefficientMatrixMap_scalar_single line 43

Source documentation

The scalar matrix units, viewed in a matrix algebra over A.

theorem coefficientMatrixMap_scalar_single (i j : ι) :
    coefficientMatrixMap (StarAlgHom.ofId ℂ A)
      (CStarMatrix.ofMatrix (Matrix.single i j (1 : ℂ))) =
        CStarMatrix.ofMatrix (Matrix.single i j (1 : A)) := by
…

Mentions: OAI.KadisonKastler.coefficientMatrixMap

theorem OAI.KadisonKastler.matrixScalarHom_commutes_scalar line 52
Source documentation
Every constant diagonal matrix commutes with the scalar matrix copy.
```
theorem matrixScalarHom_commutes_scalar (a : A) (s : CStarMatrix ι ι ℂ) :
    coefficientMatrixMap (StarAlgHom.ofId ℂ A) s * matrixScalarHom a =
      matrixScalarHom a * coefficientMatrixMap (StarAlgHom.ofId ℂ A) s := by
…
```
Mentions: OAI.KadisonKastler.coefficientMatrixMap, OAI.KadisonKastler.matrixScalarHom

theorem OAI.KadisonKastler.exists_matrixScalarHom_of_commutes line 63

Source documentation

It is enough to commute with the scalar matrix copy to be constant diagonal.

theorem exists_matrixScalarHom_of_commutes (x : CStarMatrix ι ι A)
    (hx : ∀ s : CStarMatrix ι ι ℂ,
      coefficientMatrixMap (StarAlgHom.ofId ℂ A) s * x =
        x * coefficientMatrixMap (StarAlgHom.ofId ℂ A) s) :
    ∃ a : A, x = matrixScalarHom a := by
…

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

theorem OAI.KadisonKastler.exists_unitary_matrixScalarHom_of_commutes line 78

Source documentation

A unitary in the scalar-matrix commutant has a unitary coefficient.

theorem exists_unitary_matrixScalarHom_of_commutes [Nonempty ι]
    (u : unitary (CStarMatrix ι ι A))
    (hu : ∀ s : CStarMatrix ι ι ℂ,
      coefficientMatrixMap (StarAlgHom.ofId ℂ A) s * (u : CStarMatrix ι ι A) =
        (u : CStarMatrix ι ι A) * coefficientMatrixMap (StarAlgHom.ofId ℂ A) s) :
    ∃ v : unitary A, (u : CStarMatrix ι ι A) = matrixScalarHom (v : A) := by
…

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