MatrixRelativeCommutant.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Irreducibility of an entrywise matrix inclusion

The scalar matrix units force any relative commutant element to be a constant diagonal matrix. Its diagonal entry commutes with the original inclusion, so scalarity of the original relative commutant proves scalarity after matrix amplification. No normality or factor classification is used.

theorem OAI.KadisonSimilarity.matrixEntryHom_single line 19

theorem OAI.KadisonSimilarity.matrix_diagonal_of_commutes_units line 28

Source documentation

Commutation with all scalar matrix units forces a constant diagonal.

theorem matrix_diagonal_of_commutes_units
    (X : CStarMatrix (Fin n) (Fin n) B)
    (hX : ∀ i j : Fin n,
      X * CStarMatrix.ofMatrix (Matrix.single i j (1 : B)) =
        CStarMatrix.ofMatrix (Matrix.single i j (1 : B)) * X) :
    ∃ b : B, X = matrixDiagonalHom n b := by
…

Mentions: OAI.KadisonSimilarity.matrixDiagonalHom

theorem OAI.KadisonSimilarity.scalar_of_matrix_relative_commutant line 50

Source documentation

An irreducible inclusion remains irreducible after finite matrix amplification. Scalars refer to the actual complex algebra maps.

theorem scalar_of_matrix_relative_commutant
    (ρ : R →⋆ₐ[ℂ] B)
    (hρ : ∀ b : B, (∀ a : R, b * ρ a = ρ a * b) →
      ∃ z : ℂ, b = algebraMap ℂ B z)
    (X : CStarMatrix (Fin n) (Fin n) B)
    (hX : ∀ Y : CStarMatrix (Fin n) (Fin n) R,
      X * matrixEntryHom ρ Y = matrixEntryHom ρ Y * X) :
    ∃ z : ℂ, X = algebraMap ℂ (CStarMatrix (Fin n) (Fin n) B) z := by
…

Mentions: OAI.KadisonSimilarity.matrixEntryHom