OAI/Analysis/KadisonSimilarity/Representation/FiniteTypeIStructure.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A finite factor with a nonzero abelian projection is a full matrix algebra. The homogeneous central piece is the unit because the center is scalar.

  1. def OAI.KadisonSimilarity.unitCornerEquiv line 18
  2. def OAI.KadisonSimilarity.matrixUnitsOfSystem line 29
  3. theorem OAI.KadisonSimilarity.matrixSystem_surjective_of_abelian_diagonal line 36
  4. theorem OAI.KadisonSimilarity.finiteMatrixFactorModel_of_homogeneous_unit line 66
  5. theorem OAI.KadisonSimilarity.finiteMatrixFactorModel_of_abelian_projection line 90

    Source documentation

    A finite factor containing a nonzero abelian projection has the exact finite matrix model used in the type-I commutator estimate.

    theorem finiteMatrixFactorModel_of_abelian_projection [Nontrivial H]
    (hfinite : FiniteAlgebra P.toStarSubalgebra)
    (hfactor : ∀ a : P.toStarSubalgebra, (∀ b, a * b = b * a) →
      ∃ c : ℂ, a = algebraMap ℂ P.toStarSubalgebra c)
    (p : P.toStarSubalgebra) (hp : FinitePathMain.AbelianProjection p) (hp0 : p ≠ 0) :
    Nonempty (FiniteMatrixFactorModel P) := by
…

    Mentions: OAI.FinitePathMain.AbelianProjection, OAI.KadisonSimilarity.FiniteMatrixFactorModel