OAI/Analysis/BoundedHochschild/CountableMatrixPrimitives.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

The type-I matrix subalgebra and the final cohomological step for its multimodular cocycles. Reduction of an ordinary cocycle to such a representative is a separate obligation; no such reduction is assumed to be proved here.

  1. theorem OAI.BoundedHochschild.KadisonRingrose.exists_typeI_countable_matrix_closure line 20
  2. theorem OAI.BoundedHochschild.KadisonRingrose.primitive_of_countableMatrix_multimodular line 29