OAI/Analysis/BoundedHochschild/TypeIIStructure.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Projection comparison and matrix structure in finite type-II algebras.

  1. lemma OAI.HochschildTypeII.central_annihilator_chain line 27
  2. lemma OAI.HochschildTypeII.abelian_of_le line 74
  3. lemma OAI.HochschildTypeII.projection_orthogonal_of_le_complement line 83
  4. theorem OAI.HochschildTypeII.exists_typeI_support line 91
  5. theorem OAI.HochschildTypeII.no_abelian_projection line 125
  6. lemma OAI.HochschildTypeII.projection_orthogonal_of_le_sub line 131
  7. theorem OAI.HochschildTypeII.exists_orthogonal_equivalent line 143