OAI/Analysis/KadisonKastler/SimpleAlgebraIdealSeparation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Separating a simple unital algebra from ideals in an extension

These are the norm-separation steps used in the maximal-ideal construction in Sakai, Derivations of simple C-algebras II*, p.260. A proper closed star ideal in a unital extension has an isometric quotient map on the simple unital subalgebra. In particular it cannot approach a nonzero element of that subalgebra more closely than its norm.

  1. theorem OAI.KadisonKastler.closedStarIdeal_quotient_nontrivial line 24
  2. theorem OAI.KadisonKastler.simple_quotient_composition_injective line 32
  3. theorem OAI.KadisonKastler.simple_quotient_composition_norm line 40
  4. theorem OAI.KadisonKastler.simple_norm_le_sub_ideal line 48