OAI/Analysis/KadisonKastler/DiffuseInfiniteDimensional.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Diffuse projection algebras are infinite dimensional

Splitting a nonzero projection strictly decreases the dimension of its right ideal. Finite dimensionality therefore contradicts diffuseness.

  1. def OAI.KadisonKastler.projectionRightIdeal line 19
  2. theorem OAI.KadisonKastler.projectionRightIdeal_strict line 25
  3. theorem OAI.KadisonKastler.not_finiteDimensional_of_isII1Factor line 41

    Source documentation

    The ordinary II₁-factor projection predicate forces its concrete operator algebra to be infinite dimensional.

    theorem not_finiteDimensional_of_isII1Factor (hM : Generator.IsII1Factor M.toStarSubalgebra) :
    ¬ FiniteDimensional ℂ (Algebra M) := by
…

    Mentions: OAI.Generator.IsII1Factor, OAI.KadisonKastler.Algebra