OAI/Analysis/BoundedHochschild/FiniteGroupPrefixAverages.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Contractive prefix averages interpolate between the identity and the finite-group cochain average. They use the same independent vertex variables as the bar-insertion operators.

  1. def OAI.BoundedHochschild.KadisonRingrose.finiteGroupPrefixAverage line 15
  2. lemma OAI.BoundedHochschild.KadisonRingrose.finiteGroupPrefixAverage_norm line 20
  3. lemma OAI.BoundedHochschild.KadisonRingrose.finiteGroupPrefixAverage_zero line 34
  4. lemma OAI.BoundedHochschild.KadisonRingrose.finiteGroupPrefixAverage_full line 45
  5. lemma OAI.BoundedHochschild.KadisonRingrose.finiteGroupPrefixAverage_add line 53
  6. lemma OAI.BoundedHochschild.KadisonRingrose.finiteGroupPrefixAverage_smul line 59
  7. def OAI.BoundedHochschild.KadisonRingrose.finiteGroupPrefixAverageCLM line 65
  8. lemma OAI.BoundedHochschild.KadisonRingrose.finiteGroupPrefixAverage_telescope line 77

    Source documentation

    The successive prefix changes sum to the difference between a cochain and its full finite-group average.

    lemma finiteGroupPrefixAverage_telescope {n : ℕ} (ρ : G →* unitary M)
    (f : Cochain M n) :
    (∑ i : Fin (n + 1), (finiteGroupPrefixAverage ρ i.val f -
      finiteGroupPrefixAverage ρ (i.val + 1) f)) = f - finiteGroupCochainAverage ρ f := by
…

    Mentions: OAI.BoundedHochschild.Cochain, OAI.BoundedHochschild.KadisonRingrose.finiteGroupPrefixAverage, OAI.BoundedHochschild.KadisonRingrose.finiteGroupCochainAverage