OAI/Analysis/KadisonKastler/TypeIIIPrescribedRank.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Prescribed finite matrix ranks for type III projections

Every nonzero projection splits into any positive finite number of nonzero pieces. Consequently a nontrivial projection can occupy either chosen positive block size in a unital full matrix algebra.

  1. theorem OAI.KadisonKastler.TypeIIIFactor.exists_proper_subprojection line 22
  2. theorem OAI.KadisonKastler.TypeIIIFactor.exists_nonzero_fin_partition line 42
  3. theorem OAI.KadisonKastler.TypeIIIFactor.exists_matrixUnits_prescribed_projection_rank line 92