Even-degree cohomology of a finite cyclic group

For a finite cyclic group G generated by g and a representation A, Mathlib's Rep.FiniteCyclicGroup.groupCohomologyπEven maps Ker(ρ(g) - 𝟙) to Hⁱ(G, A) for every positive even i, and Rep.FiniteCyclicGroup.groupCohomologyπEven_eq_zero_iff identifies its kernel with the image of the norm. This file records that the map is surjective, so that Hⁱ(G, A) is the quotient Ker(ρ(g) - 𝟙) / Im(N); this is the form in which a homomorphism out of Hⁱ(G, A) is defined by its values on g-fixed elements.

In degree 2 it then makes the map explicit on cocycles. Let n be the order of G. A g-fixed element a is sent to the class of the carry cocycle

(gⁱ, gʲ) ↦ a if i + j ≥ n, and 0 otherwise (0 ≤ i, j < n),

which records the carry in the addition of exponents modulo n (Rep.FiniteCyclicGroup.groupCohomologyπEven_two_apply). Mathlib defines groupCohomologyπEven through the periodic resolution ⋯ → k[G] --N--> k[G] --(g - 1)--> k[G] → k; the identification comes from a comparison map from the bar resolution, which in degrees 1 and 2 sends [gⁱ] to 1 + g + ⋯ + gⁱ⁻¹ and [gⁱ | gʲ] to the carry of i + j.

The cocycle description makes the periodicity class computable under change of groups. If f : G → G' is a homomorphism of finite cyclic groups sending the generator g to g' ^ d, for a generator g' of G', and d · |G| = m · |G'|, then the class of b is sent to the class of m • b (Rep.FiniteCyclicGroup.map_groupCohomologyπEven_two). For d = 1, f is a surjection with kernel of order m. In the cohomology of local fields this is the statement that inflation along a tower of unramified extensions preserves the local invariant; general d covers the change of ground field, where arithmetic Frobenius restricts to a power of arithmetic Frobenius.

Main definitions

• Rep.FiniteCyclicGroup.carryCocycle: the carry cocycle of a g-fixed element, as a k-linear map into the 2-cocycles.

Main results

• Rep.FiniteCyclicGroup.groupCohomologyπEven_surjective: in positive even degree every class is represented by an element fixed by the generator.
• Rep.FiniteCyclicGroup.ρ_apply_of_mem_ker: an element of the kernel of ρ(g) - 1 is fixed by g.
• Rep.FiniteCyclicGroup.carryCocycle_apply_pow: the values of the carry cocycle.
• Rep.FiniteCyclicGroup.groupCohomologyπEven_two, Rep.FiniteCyclicGroup.groupCohomologyπEven_two_apply: in degree 2, groupCohomologyπEven sends a fixed element to the class of its carry cocycle.
• Rep.FiniteCyclicGroup.map_groupCohomologyπEven_two: a homomorphism of finite cyclic groups sending g to g' ^ d, with d · |G| = m · |G'|, sends the class of b to the class of m • b.

References

• K. S. Brown, Cohomology of Groups, Graduate Texts in Mathematics 87, Springer (1982), Chapter I, §6 (the periodic resolution of a cyclic group) and Chapter I, §7 (comparison of projective resolutions).
• J.-P. Serre, Local Fields, Graduate Texts in Mathematics 67, Springer (1979), Chapter VIII, §4 (the cohomology of cyclic groups).

theorem Rep.FiniteCyclicGroup.groupCohomologyπEven_surjective {k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep.{u, u, u} k G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (i : ℕ) [NeZero i] (hi : Even i) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (groupCohomologyπEven A g hg i hi))

In positive even degree, every class in the cohomology of a finite cyclic group is represented by an element fixed by the generator.

The comparison map from the bar resolution to the periodic resolution

The periodicity class in degree two

theorem Rep.FiniteCyclicGroup.ρ_apply_of_mem_ker {k G : Type u} [CommRing k] [CommGroup G] (A : Rep.{u_1, u, u} k G) (g : G) (x : ↥(Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A)).ker) : (A.ρ g) ↑x = ↑x

An element of the kernel of ρ(g) - 1, the degree-2 cycles of the periodic complex, is fixed by g.

noncomputable def Rep.FiniteCyclicGroup.carryCocycle {k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep.{u_1, u, u} k G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) : ↥(Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A)).ker →ₗ[k] ↥(groupCohomology.cocycles₂ A)

The carry cocycle of an element a fixed by the generator g of a finite cyclic group of order n: the 2-cocycle (gⁱ, gʲ) ↦ a if i + j ≥ n and 0 otherwise, for 0 ≤ i, j < n (carryCocycle_apply_pow). Its class is the periodicity class of a (groupCohomologyπEven_two_apply).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Rep.FiniteCyclicGroup.carryCocycle_apply_pow {k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep.{u_1, u, u} k G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (x : ↥(Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A)).ker) {i j : ℕ} (hi : i < orderOf g) (hj : j < orderOf g) : ((carryCocycle A g hg) x) (g ^ i, g ^ j) = if orderOf g ≤ i + j then ↑x else 0

The values of the carry cocycle: on (gⁱ, gʲ) with i, j < n it is a if i + j ≥ n and 0 otherwise.

theorem Rep.FiniteCyclicGroup.groupCohomologyπEven_two {k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep.{u, u, u} k G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) : groupCohomologyπEven A g hg 2 ⋯ = CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (carryCocycle A g hg)) (groupCohomology.H2π A)

The periodicity class in degree 2 is the class of the carry cocycle: Mathlib's groupCohomologyπEven in degree 2 factors through the carry cocycle.

@[simp]

theorem Rep.FiniteCyclicGroup.groupCohomologyπEven_two_apply {k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep.{u, u, u} k G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) (x : ↥(Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A)).ker) : (CategoryTheory.ConcreteCategory.hom (groupCohomologyπEven A g hg 2 ⋯)) x = (CategoryTheory.ConcreteCategory.hom (groupCohomology.H2π A)) ((carryCocycle A g hg) x)

The periodicity class in degree 2 is the class of the carry cocycle: an element a fixed by the generator g is sent to the class of (gⁱ, gʲ) ↦ a if i + j ≥ n, and 0 otherwise.

Change of group between finite cyclic groups

theorem Rep.FiniteCyclicGroup.map_groupCohomologyπEven_two {k G : Type u} [CommRing k] [CommGroup G] [Fintype G] (A : Rep.{u, u, u} k G) (g : G) (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {G' : Type u} [CommGroup G'] [Fintype G'] {B : Rep.{u, u, u} k G'} (f : G →* G') {g' : G'} (hg' : ∀ (x : G'), x ∈ Subgroup.zpowers g') (d : ℕ) (hfg : f g = g' ^ d) (φ : res f B ⟶ A) (m : ℕ) (hm : d * Nat.card G = m * Nat.card G') (y : ↥(Hom.hom (B.applyAsHom g' - CategoryTheory.CategoryStruct.id B)).ker) (z : ↥(Hom.hom (A.applyAsHom g - CategoryTheory.CategoryStruct.id A)).ker) (hz : ↑z = m • (Hom.hom φ) ↑y) : (CategoryTheory.ConcreteCategory.hom (groupCohomology.map f φ 2)) ((CategoryTheory.ConcreteCategory.hom (groupCohomologyπEven B g' hg' 2 ⋯)) y) = (CategoryTheory.ConcreteCategory.hom (groupCohomologyπEven A g hg 2 ⋯)) z

Change of group for the periodicity class between finite cyclic groups. Let f : G →* G' be a homomorphism of finite cyclic groups sending the generator g to g' ^ d, where g' generates G', let m satisfy d · |G| = m · |G'|, and let φ : Res_f B ⟶ A. Then H²(G', B) → H²(G, A) sends the class of a g'-fixed element y to the class of the g-fixed element m • φ y. For d = 1 this is inflation along a surjection with kernel of order m.