Documentation

TauCeti.RepresentationTheory.Homological.GroupCohomology.LowDegree

Low-degree group cohomology #

For a trivial representation A of a group G, Mathlib identifies H¹(G, A) with the group of additive homomorphisms G →+ A. This file records the consequence that H¹(G, A) vanishes when G is finite and A has no additive torsion, since a homomorphism from a finite group into a torsion-free group is zero.

It also records the H¹ criterion for taking invariants to preserve a short exact sequence 0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0. The general result for G-invariants follows from the degree-zero part of Mathlib's long exact cohomology sequence. The result for a normal subgroup S applies it to the restricted sequence and retains the quotient-group action.

Finally, it records an identity satisfied by a 2-cocycle f of a monoid along two adjacent commuting squares d * a' = a * d₁ and d₁ * b' = b * d₂: three instances of the cocycle law express d • f (a', b') through the values of f at the sides and diagonals of the squares. It also records that a 2-cocycle of a group G vanishing on G × N and on N × G, for a normal subgroup N, is constant on the cosets of N in both variables and takes N-fixed values: the input for descending such a cocycle to G ⧸ N. Summing the identity along the squares over a finite normal subgroup N shows that the norm of N multiplies a 2-cocycle by the order of N up to an explicit coboundary.

Main statements #

source
noncomputable def Rep.h2Representative {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (u : ↑(groupCohomology A 2)) :
↥(groupCohomology.cocycles₂ A)

A chosen two-cocycle representing u ∈ H²(G, A).

Equations
Instances For
    source
    @[simp]
    theorem Rep.H2π_h2Representative {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (u : ↑(groupCohomology A 2)) :
    (CategoryTheory.ConcreteCategory.hom (groupCohomology.H2π A)) (A.h2Representative u) = u

    The chosen two-cocycle represents the original second-cohomology class.

    source
    theorem TauCeti.groupCohomology.isZero_H1_of_isTrivial {k G : Type u} [CommRing k] [Group G] [Finite G] (A : Rep k G) [A.IsTrivial] [IsAddTorsionFree ↑A] :
    CategoryTheory.Limits.IsZero (groupCohomology A 1)

    H¹(G, A) = 0 for a trivial representation A of a finite group G whose underlying module has no additive torsion.

    source
    theorem TauCeti.groupCohomology.shortExact_map_invariantsFunctor (k G : Type u) [CommRing k] [Group G] {X : CategoryTheory.ShortComplex (Rep k G)} (hX : X.ShortExact) (h1 : CategoryTheory.Limits.IsZero (groupCohomology X.X₁ 1)) :
    (X.map (Rep.invariantsFunctor k G)).ShortExact

    Taking invariants preserves a short exact sequence of G-representations when the first cohomology of its kernel vanishes.

    source
    theorem TauCeti.groupCohomology.shortExact_map_quotientToInvariantsFunctor {k G : Type u} [CommRing k] [Group G] (S : Subgroup G) [S.Normal] {X : CategoryTheory.ShortComplex (Rep k G)} (hX : X.ShortExact) (h1 : CategoryTheory.Limits.IsZero (groupCohomology (Rep.res S.subtype X.X₁) 1)) :
    (X.map (Rep.quotientToInvariantsFunctor k S)).ShortExact

    If 0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0 is short exact and H¹(S, X₁) = 0, then taking S-invariants preserves short exactness as a sequence of representations of G ⧸ S.

    source
    theorem TauCeti.groupCohomology.smul_map_eq_of_isCocycle₂_of_mul_eq_mul {K : Type u_1} {A : Type u_2} [Monoid K] [AddCommGroup A] [MulAction K A] {f : K × K → A} (hf : groupCohomology.IsCocycle₂ f) {d a' b' a b d₁ d₂ : K} (h₁ : d * a' = a * d₁) (h₂ : d₁ * b' = b * d₂) :
    d • f (a', b') = a • f (d₁, b') - a • f (b, d₂) - f (d, a' * b') + f (a * b, d₂) + f (d, a') - f (a, d₁) + f (a, b)

    A 2-cocycle identity along two adjacent commuting squares: if d * a' = a * d₁ and d₁ * b' = b * d₂ in a monoid K, then for a 2-cocycle f : K × K → A, d • f (a', b') is an alternating sum of the values of f at the sides of the two squares and at the products a' * b' and a * b.

    source
    theorem TauCeti.groupCohomology.apply_mul_snd_of_isCocycle₂_of_vanishing {K : Type u_3} {A : Type u_4} [Monoid K] [AddCommGroup A] [DistribMulAction K A] {N : Set K} {f : K × K → A} (hf : groupCohomology.IsCocycle₂ f) (hR : ∀ (g : K) (n : ↑N), f (g, ↑n) = 0) (g h : K) (n : ↑N) :
    f (g, h * ↑n) = f (g, h)

    A 2-cocycle of a monoid K vanishing on K × N, for a subset N, is unchanged by right multiplication of its second argument by N.

    source
    theorem TauCeti.groupCohomology.apply_mul_fst_of_isCocycle₂_of_vanishing {G : Type u_3} {A : Type u_4} [Group G] [AddCommGroup A] [DistribMulAction G A] {N : Subgroup G} [N.Normal] {f : G × G → A} (hf : groupCohomology.IsCocycle₂ f) (hR : ∀ (g : G) (n : ↥N), f (g, ↑n) = 0) (hL : ∀ (n : ↥N) (g : G), f (↑n, g) = 0) (g h : G) (n : ↥N) :
    f (g * ↑n, h) = f (g, h)

    A 2-cocycle vanishing on G × N and on N × G, for a normal subgroup N, is unchanged by right multiplication of its first argument by N.

    source
    theorem TauCeti.groupCohomology.smul_apply_of_isCocycle₂_of_vanishing {G : Type u_3} {A : Type u_4} [Group G] [AddCommGroup A] [DistribMulAction G A] {N : Subgroup G} [N.Normal] {f : G × G → A} (hf : groupCohomology.IsCocycle₂ f) (hR : ∀ (g : G) (n : ↥N), f (g, ↑n) = 0) (hL : ∀ (n : ↥N) (g : G), f (↑n, g) = 0) (n : ↥N) (g h : G) :
    ↑n • f (g, h) = f (g, h)

    The values of a 2-cocycle vanishing on G × N and on N × G, for a normal subgroup N, are fixed by N.

    source
    theorem TauCeti.groupCohomology.sum_smul_apply_of_isCocycle₂ {G : Type u_3} {A : Type u_4} [Group G] [AddCommGroup A] [DistribMulAction G A] (N : Subgroup G) [N.Normal] [Fintype ↥N] {f : G × G → A} (hf : groupCohomology.IsCocycle₂ f) (g h : G) :
    ∑ n : ↥N, ↑n • f (g, h) = Nat.card ↥N • f (g, h) + (g • ∑ n : ↥N, (f (↑n, h) - f (h, ↑n)) - ∑ n : ↥N, (f (↑n, g * h) - f (g * h, ↑n)) + ∑ n : ↥N, (f (↑n, g) - f (g, ↑n)))

    The norm of a finite normal subgroup N multiplies a 2-cocycle f by the order of N up to a coboundary: ∑ n : N, n • f (g, h) = #N • f (g, h) + (g • b h - b (g * h) + b g) for b k = ∑ n : N, (f (n, k) - f (k, n)).