OAI/Analysis/KadisonKastler/TypeIIIUltraproduct.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Simplicity and commutator correction for type III norm ultraproducts

Spectral cuts, projection comparison, and Sakai innerness give simplicity of the norm ultraproduct and a uniform coordinate correction for its invariant derivations.

  1. theorem OAI.KadisonKastler.TypeIIIFactor.algebraNontrivial line 25
  2. theorem OAI.KadisonKastler.typeIII_normUltraproduct_simple line 35
  3. theorem OAI.KadisonKastler.exists_typeIII_uniform_commutator_correction line 50