FullMatrixRefinement.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Compatible refinement inside a full matrix algebra

Pass to a finite Hilbert-space representation, use the adapted basis, and transport its rank-one matrix units back. The old signed group is retained.

theorem OAI.KadisonKastler.matrixUnits_map_hom line 21

theorem OAI.KadisonKastler.exists_matrix_refinement_of_finite_representation line 31

Source documentation

A matrix system in a finite full operator algebra extends to a full system whose signed group contains the original one.

theorem exists_matrix_refinement_of_finite_representation
    {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
    [FiniteDimensional ℂ H] (θ : A ≃⋆ₐ[ℂ] (H →L[ℂ] H))
    (E : Generator.MatrixUnitSystem ι A) (o : ι) :
    ∃ (r : ℕ) (F : Generator.MatrixUnitSystem (ι × Fin r) A),
      0 < r ∧ Function.Surjective F.hom ∧
      (∀ i j, ∑ k, F.entry (i, k) (j, k) = E.entry i j) ∧
      matrixSignedGroup E ≤ matrixSignedGroup F := by
…

Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.matrixSignedGroup

theorem OAI.KadisonKastler.exists_matrix_refinement_in_full_matrix_algebra line 65

Source documentation

The only representation data needed above are supplied by any full matrix system for the containing algebra.

theorem exists_matrix_refinement_in_full_matrix_algebra
    {κ : Type*} [Fintype κ] [DecidableEq κ] [Nonempty κ]
    (P : Generator.MatrixUnitSystem κ A) (hP : Function.Surjective P.hom)
    (E : Generator.MatrixUnitSystem ι A) (o : ι) :
    ∃ (r : ℕ) (F : Generator.MatrixUnitSystem (ι × Fin r) A),
      0 < r ∧ Function.Surjective F.hom ∧
      (∀ i j, ∑ k, F.entry (i, k) (j, k) = E.entry i j) ∧
      matrixSignedGroup E ≤ matrixSignedGroup F := by
…

Mentions: OAI.Generator.MatrixUnitSystem, OAI.KadisonKastler.matrixSignedGroup