OAI/Analysis/BoundedHochschild/MultimodularColumns.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The algebraic column identity for a cochain that is multimodular over a star subalgebra. This is the matrix estimate used in the properly infinite reduction; all module identities are the usual adjacent-input identities.

  1. structure OAI.BoundedHochschild.KadisonRingrose.MultimodularOver line 17
  2. def OAI.BoundedHochschild.KadisonRingrose.shiftedColumnTuple line 27
  3. lemma OAI.BoundedHochschild.KadisonRingrose.shiftedColumnTuple_zero line 31
  4. lemma OAI.BoundedHochschild.KadisonRingrose.multimodular_slide_column line 38
  5. def OAI.BoundedHochschild.KadisonRingrose.columnDiagonal line 71
  6. lemma OAI.BoundedHochschild.KadisonRingrose.columnDiagonal_mul_column line 74
  7. lemma OAI.BoundedHochschild.KadisonRingrose.multimodular_column_term line 82