Documentation

TauCeti.RepresentationTheory.Homological.GroupCohomology.Averaging

The averaging contraction of the inhomogeneous cochains of a finite group #

Let G be a finite group whose order is invertible in the commutative ring k, and let A be a k-linear representation of G. Averaging an (n + 1)-cochain over its last argument, $$(hf)(g_1, \dots, g_n) = \frac{1}{|G|} \sum_{g \in G} f(g_1, \dots, g_n, g),$$ is a contracting homotopy of the complex of inhomogeneous cochains inhomogeneousCochains A in positive degrees, in Mathlib's convention for the differential inhomogeneousCochains.d, whose first face is g_0 • f(g_1, …, g_n). In degree 0 the same operator recovers the averaging projection Representation.averageMap onto the invariants.

Precisely, with the sign (-1)^(n+1) on the component of degree n + 1 → n, the identity of inhomogeneousCochains A is homotopic to the chain map that is Representation.averageMap in degree 0 and zero in positive degrees, the projection onto the invariants placed in degree 0. In particular every positive-degree cocycle has an explicit primitive, (-1)^(n+1) times its average over the last argument. Both are assembled from the two identities of the average with the differential by TauCeti.groupCohomology.homotopyOfDCompEq and TauCeti.inhomogeneousCochains.d_smul_of_d_comp_eq. The vanishing of positive-degree cohomology that this implies is groupCohomology.subsingleton_of_isUnit_natCard, proved there by corestriction. The chain-level contraction, rather than the vanishing alone, is what a comparison of cochain complexes built from finite-group actions with their invariants uses.

The last argument is used because the last face of the differential, f(g_0, …, g_{n-1}), does not involve the action, while the translation g ↦ g_n g absorbs the face that multiplies g_n into the averaged variable.

Main declarations #

References #

source
def TauCeti.inhomogeneousCochains.averageLast {k G : Type u} [CommRing k] [Group G] [Fintype G] [Invertible ↑(Fintype.card G)] (A : Rep k G) (n : ℕ) :
↧((Fin (n + 1) → G) → ↑A) ⟶ ↧((Fin n → G) → ↑A)

The average x ↦ ⅟|G| • ∑ g, f (Fin.snoc x g) of an (n + 1)-cochain f over its last argument, an n-cochain.

Instances For
    source
    @[simp]
    theorem TauCeti.inhomogeneousCochains.averageLast_hom_apply {k G : Type u} [CommRing k] [Group G] [Fintype G] [Invertible ↑(Fintype.card G)] (A : Rep k G) (n : ℕ) (f : ↑↧((Fin (n + 1) → G) → ↑A)) (x : Fin n → G) :
    (ModuleCat.Hom.hom (averageLast A n)) f x = ⅟↑(Fintype.card G) • ∑ g : G, f (Fin.snoc x g)

    The value of the average over the last argument.

    source
    theorem TauCeti.inhomogeneousCochains.d_comp_averageLast {k G : Type u} [CommRing k] [Group G] [Fintype G] [Invertible ↑(Fintype.card G)] (A : Rep k G) (n : ℕ) :
    CategoryTheory.CategoryStruct.comp (inhomogeneousCochains.d A (n + 1)) (averageLast A (n + 1)) = CategoryTheory.CategoryStruct.comp (averageLast A n) (inhomogeneousCochains.d A n) + (-1) ^ n • CategoryTheory.CategoryStruct.id ↧((Fin (n + 1) → G) → ↑A)

    Averaging over the last argument is a homotopy relation with the differential. On (n + 1)-cochains, h ∘ d = d ∘ h + (-1)^n.

    source
    theorem TauCeti.inhomogeneousCochains.d_zero_comp_averageLast {k G : Type u} [CommRing k] [Group G] [Fintype G] [Invertible ↑(Fintype.card G)] (A : Rep k G) :
    CategoryTheory.CategoryStruct.comp (inhomogeneousCochains.d A 0) (averageLast A 0) = ModuleCat.ofHom (A.ρ.averageMap.compLeft (Fin 0 → G)) - CategoryTheory.CategoryStruct.id ↧((Fin 0 → G) → ↑A)

    Averaging over the last argument of a coboundary of degree one. On 0-cochains, h ∘ d is the averaging projection minus the identity.

    source
    theorem TauCeti.inhomogeneousCochains.d_smul_averageLast_of_d_eq_zero {k G : Type u} [CommRing k] [Group G] [Fintype G] [Invertible ↑(Fintype.card G)] (A : Rep k G) {n : ℕ} {f : ↑↧((Fin (n + 1) → G) → ↑A)} (hf : (ModuleCat.Hom.hom (inhomogeneousCochains.d A (n + 1))) f = 0) :
    (ModuleCat.Hom.hom (inhomogeneousCochains.d A n)) ((-1) ^ (n + 1) • (ModuleCat.Hom.hom (averageLast A n)) f) = f

    The explicit primitive of a positive-degree cocycle. An (n + 1)-cocycle f is the coboundary of (-1)^(n+1) times its average over the last argument.

    source
    noncomputable def TauCeti.groupCohomology.averageCochainMap {k G : Type u} [CommRing k] [Group G] [Fintype G] [Invertible ↑(Fintype.card G)] (A : Rep k G) :
    groupCohomology.inhomogeneousCochains A ⟶ groupCohomology.inhomogeneousCochains A

    The averaging projection onto the invariants placed in degree 0, as an endomorphism of the complex of inhomogeneous cochains: it is Representation.averageMap on 0-cochains and zero in positive degrees.

    Instances For
      source
      @[simp]
      theorem TauCeti.groupCohomology.averageCochainMap_f_zero {k G : Type u} [CommRing k] [Group G] [Fintype G] [Invertible ↑(Fintype.card G)] (A : Rep k G) :
      (averageCochainMap A).f 0 = ModuleCat.ofHom (A.ρ.averageMap.compLeft (Fin 0 → G))

      In degree 0, TauCeti.groupCohomology.averageCochainMap is the averaging projection.

      source
      @[simp]
      theorem TauCeti.groupCohomology.averageCochainMap_f_succ {k G : Type u} [CommRing k] [Group G] [Fintype G] [Invertible ↑(Fintype.card G)] (A : Rep k G) (n : ℕ) :
      (averageCochainMap A).f (n + 1) = 0

      In positive degrees, TauCeti.groupCohomology.averageCochainMap is zero.

      source
      noncomputable def TauCeti.groupCohomology.averagingHomotopy {k G : Type u} [CommRing k] [Group G] [Fintype G] [Invertible ↑(Fintype.card G)] (A : Rep k G) :
      Homotopy (CategoryTheory.CategoryStruct.id (groupCohomology.inhomogeneousCochains A)) (averageCochainMap A)

      The averaging contraction. The identity of the complex of inhomogeneous cochains is homotopic to the averaging projection onto the invariants placed in degree 0, through the homotopy whose component from degree n + 1 to degree n is (-1)^(n+1) times the average over the last argument (TauCeti.groupCohomology.averagingHomotopy_hom_succ).

      Instances For
        source
        @[simp]
        theorem TauCeti.groupCohomology.averagingHomotopy_hom_succ {k G : Type u} [CommRing k] [Group G] [Fintype G] [Invertible ↑(Fintype.card G)] (A : Rep k G) (n : ℕ) :
        (averagingHomotopy A).hom (n + 1) n = (-1) ^ (n + 1) • inhomogeneousCochains.averageLast A n

        The component of TauCeti.groupCohomology.averagingHomotopy from degree n + 1 to degree n is (-1)^(n+1) times the average over the last argument.