OAI/Analysis/BoundedHochschild/TypeIBlocks.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Homogeneous central blocks in finite type-I algebras

Cutting a full packing by a central projection gives matrix units with an abelian diagonal. Every nonzero central cut containing an abelian projection therefore contains such a block.

  1. lemma OAI.HochschildTypeILocal.centralCornerMap_star line 34
  2. lemma OAI.HochschildTypeILocal.abelian_centralCorner line 41
  3. def OAI.HochschildTypeILocal.Packing.cutMatrixSystem line 52
  4. lemma OAI.HochschildTypeILocal.Packing.cutMatrix_diagonal_abelian line 80
  5. lemma OAI.HochschildTypeILocal.Packing.total_le_central line 87
  6. structure OAI.HochschildTypeILocal.HomogeneousBlock line 101
  7. theorem OAI.HochschildTypeILocal.exists_homogeneous_block_below line 110