OAI/Analysis/BoundedHochschild/TypeILocalMatrices.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Local matrix packing beneath abelian projections

A packing either extends by an orthogonal equivalent projection or fills a nonzero central cut. Faithfulness and finiteness of the trace rule out arbitrarily large packings.

  1. lemma OAI.HochschildTypeILocal.abelian_orthogonal_corner line 34
  2. lemma OAI.HochschildTypeILocal.central_initial_zero_final line 51
  3. lemma OAI.HochschildTypeILocal.packing_step line 62
  4. theorem OAI.HochschildTypeILocal.exists_local_full_packing line 133