OAI/Analysis/BoundedHochschild/RightModuleProjection.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

The right-module averaging projection, with its linearity, norm bound, and covariance under input and output left multiplication. This is the specialization of Sinclair–Smith (1998), Theorem 3.4, used in cohomology.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.norm_le_of_weakRightAverageOrbit line 19
  2. lemma OAI.BoundedHochschild.KadisonRingrose.module_map_weakRightAverageOrbit_singleton line 28
  3. structure OAI.BoundedHochschild.KadisonRingrose.RightModuleAveragingProjection line 37
  4. theorem OAI.BoundedHochschild.KadisonRingrose.exists_rightModuleAveragingProjection line 44