OAI/Analysis/BoundedHochschild/FiniteBarHomotopy.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The bounded finite-group bar homotopy from the identity to the full cochain average.

  1. lemma OAI.BoundedHochschild.KadisonRingrose.finiteGroupBarOperator_sum line 14
  2. lemma OAI.BoundedHochschild.KadisonRingrose.finiteGroupBarOperator_leftCoboundary line 19
  3. lemma OAI.BoundedHochschild.KadisonRingrose.finiteGroupBarOperator_rightCoboundary line 43
  4. lemma OAI.BoundedHochschild.KadisonRingrose.finiteGroupBarOperator_middleSum line 63
  5. theorem OAI.BoundedHochschild.KadisonRingrose.finiteGroupBarOperator_homotopy line 89

    Source documentation

    The explicit degree-bounded finite-group operator is a cochain homotopy.

    theorem finiteGroupBarOperator_homotopy {n : ℕ} (ρ : G →* unitary M)
    (f : Cochain M (n + 2)) :
    differential (finiteGroupBarOperator ρ f) + finiteGroupBarOperator ρ (differential f) =
      f - finiteGroupCochainAverage ρ f := by
…

    Mentions: OAI.BoundedHochschild.Cochain, OAI.BoundedHochschild.differential, OAI.BoundedHochschild.KadisonRingrose.finiteGroupBarOperator, OAI.BoundedHochschild.KadisonRingrose.finiteGroupCochainAverage