The splitting module of a degree-two cohomology class

For a representation A of a group G and a class u ∈ H²(G, A), this file constructs the splitting module A(u). Its underlying module is I_G × A, where I_G is the augmentation ideal. A cocycle representing u twists the diagonal action on this product. There is a short exact sequence

0 → A → A(u) → I_G → 0,

and the image of u in H²(G, A(u)) is zero. This is the second dimension shift in Tate's cup-product criterion: once the hypotheses of that criterion show that A(u) has vanishing cohomology in two consecutive degrees for every subgroup, Tate's cohomological triviality criterion makes it acyclic in every Tate degree.

The construction follows J. S. Milne, Class Field Theory, Chapter II, proof of Theorem 3.11. It is adapted to Mathlib's Rep and low-degree cohomology API from kbuzzard/ClassFieldTheory, commit ccc3323c6750abca25b49b35106f54eb3a398509, file ClassFieldTheory/Cohomology/SplittingModule.lean (Apache-2.0).

Main definitions

• Rep.splittingModule: the splitting module of a degree-two class.
• Rep.splittingModuleSES: its short exact sequence with the augmentation ideal.

Main results

• Rep.splittingModuleSES_shortExact, Rep.splittingModuleSES_res_shortExact: the splitting-module sequence is short exact, also after restriction.
• Rep.map_splittingModuleIncl_res_eq_zero: after restriction along any group homomorphism, the defining class maps to zero in the splitting module's second cohomology.
• Rep.surjective_connecting_res_splittingModule: the connecting map H¹(H, I_G) → H²(H, A) of the splitting-module sequence restricted along f : H → G is onto when H²(H, A) is generated by the restriction of the defining class.

noncomputable def Rep.splittingTwist {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (u : ↑(groupCohomology A 2)) (g : G) : ↑(augmentationIdeal k G) →ₗ[k] ↑A

The linear correction term contributed by a cocycle to the action on its splitting module.

theorem Rep.splittingTwist_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (u : ↑(groupCohomology A 2)) (g : G) (x : ↑(augmentationIdeal k G)) : (A.splittingTwist u g) x = ((Hom.hom (augmentationι k G)) x).coeff.sum fun (h : G) (a : k) => a • (A.h2Representative u) (g, h)

The correction term is the coefficientwise pairing with the chosen cocycle representative.

@[simp]

theorem Rep.splittingTwist_one {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (u : ↑(groupCohomology A 2)) : A.splittingTwist u 1 = 0

The correction term at the identity is zero.

theorem Rep.splittingTwist_mul {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (u : ↑(groupCohomology A 2)) (g₁ g₂ : G) (x : ↑(augmentationIdeal k G)) : (A.splittingTwist u (g₁ * g₂)) x = (A.ρ g₁) ((A.splittingTwist u g₂) x) + (A.splittingTwist u g₁) (((augmentationIdeal k G).ρ g₂) x)

The cocycle identity is precisely the identity needed for the twisted maps to form a group action on the splitting module.

noncomputable def Rep.splittingModule {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (u : ↑(groupCohomology A 2)) : Rep k G

The splitting module A(u) of a class u ∈ H²(G, A). Its underlying module is linearly equivalent to I_G × A; the action is twisted by a chosen cocycle representing u.

noncomputable def Rep.splittingModuleEquiv {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (u : ↑(groupCohomology A 2)) : ↑(A.splittingModule u) ≃ₗ[k] ↑(augmentationIdeal k G) × ↑A

The underlying linear equivalence from the splitting module to I_G × A.

noncomputable def Rep.splittingModuleMk {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (u : ↑(groupCohomology A 2)) (x : ↑(augmentationIdeal k G)) (a : ↑A) : ↑(A.splittingModule u)

Construct an element of the splitting module from its augmentation-ideal and coefficient coordinates.

@[simp]

theorem Rep.splittingModuleEquiv_mk {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (u : ↑(groupCohomology A 2)) (x : ↑(augmentationIdeal k G)) (a : ↑A) : (A.splittingModuleEquiv u) (A.splittingModuleMk u x a) = (x, a)

The coordinates of an element constructed by splittingModuleMk.

@[simp]

theorem Rep.splittingModuleEquiv_ρ_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (u : ↑(groupCohomology A 2)) (g : G) (x : ↑(A.splittingModule u)) : (A.splittingModuleEquiv u) (((A.splittingModule u).ρ g) x) = (((augmentationIdeal k G).ρ g) ((A.splittingModuleEquiv u) x).1, (A.ρ g) ((A.splittingModuleEquiv u) x).2 + (A.splittingTwist u g) ((A.splittingModuleEquiv u) x).1)

The action on the splitting module, transported to I_G × A.

noncomputable def Rep.splittingModuleIncl {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (u : ↑(groupCohomology A 2)) : A ⟶ A.splittingModule u

The inclusion A → A(u) into the second factor of the splitting module.

@[simp]

theorem Rep.splittingModuleEquiv_incl_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (u : ↑(groupCohomology A 2)) (a : ↑A) : (A.splittingModuleEquiv u) ((CategoryTheory.ConcreteCategory.hom (A.splittingModuleIncl u)) a) = (0, a)

Under splittingModuleEquiv, the inclusion sends a to (0, a).

noncomputable def Rep.splittingModuleProj {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (u : ↑(groupCohomology A 2)) : A.splittingModule u ⟶ augmentationIdeal k G

The projection A(u) → I_G from the splitting module to the augmentation ideal.

@[simp]

theorem Rep.splittingModuleProj_apply {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (u : ↑(groupCohomology A 2)) (x : ↑(A.splittingModule u)) : (CategoryTheory.ConcreteCategory.hom (A.splittingModuleProj u)) x = ((A.splittingModuleEquiv u) x).1

The projection from the splitting module returns the first transported coordinate.

@[simp]

theorem Rep.splittingModuleIncl_comp_splittingModuleProj {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (u : ↑(groupCohomology A 2)) : CategoryTheory.CategoryStruct.comp (A.splittingModuleIncl u) (A.splittingModuleProj u) = 0

The inclusion of A followed by the projection to I_G is zero.

@[simp]

theorem Rep.splittingModuleIncl_comp_splittingModuleProj_assoc {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (u : ↑(groupCohomology A 2)) {Z : Rep k G} (h : augmentationIdeal k G ⟶ Z) : CategoryTheory.CategoryStruct.comp (A.splittingModuleIncl u) (CategoryTheory.CategoryStruct.comp (A.splittingModuleProj u) h) = CategoryTheory.CategoryStruct.comp 0 h

The inclusion of A followed by the projection to I_G is zero.

theorem Rep.splittingModuleIncl_injective {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (u : ↑(groupCohomology A 2)) : Function.Injective ⇑(Hom.hom (A.splittingModuleIncl u))

The inclusion of A into the splitting module is injective.

theorem Rep.ker_splittingModuleProj_eq_range {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (u : ↑(groupCohomology A 2)) : (Hom.hom (A.splittingModuleProj u)).ker = (Hom.hom (A.splittingModuleIncl u)).range

The kernel of the projection to I_G is the image of the inclusion of A.

noncomputable def Rep.splittingModuleSES {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (u : ↑(groupCohomology A 2)) : CategoryTheory.ShortComplex (Rep k G)

The short complex A → A(u) → I_G associated to the splitting module.

theorem Rep.splittingModuleSES_def {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (u : ↑(groupCohomology A 2)) : A.splittingModuleSES u = { X₁ := A, X₂ := A.splittingModule u, X₃ := augmentationIdeal k G, f := A.splittingModuleIncl u, g := A.splittingModuleProj u, zero := ⋯ }

The splitting-module sequence has maps the inclusion of A and the projection to I_G.

@[simp]

theorem Rep.splittingModuleSES_X₁ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (u : ↑(groupCohomology A 2)) : (A.splittingModuleSES u).X₁ = A

The left object of the splitting-module sequence is the original representation.

@[simp]

theorem Rep.splittingModuleSES_X₂ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (u : ↑(groupCohomology A 2)) : (A.splittingModuleSES u).X₂ = A.splittingModule u

The middle object of the splitting-module sequence is the splitting module.

@[simp]

theorem Rep.splittingModuleSES_X₃ {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (u : ↑(groupCohomology A 2)) : (A.splittingModuleSES u).X₃ = augmentationIdeal k G

The right object of the splitting-module sequence is the augmentation ideal.

@[simp]

theorem Rep.splittingModuleSES_f {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (u : ↑(groupCohomology A 2)) : (A.splittingModuleSES u).f ≍ A.splittingModuleIncl u

The first map of the splitting-module sequence is the inclusion into the second factor.

@[simp]

theorem Rep.splittingModuleSES_g {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (u : ↑(groupCohomology A 2)) : (A.splittingModuleSES u).g ≍ A.splittingModuleProj u

The second map of the splitting-module sequence is projection onto the first factor.

theorem Rep.splittingModuleSES_shortExact {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (u : ↑(groupCohomology A 2)) : (A.splittingModuleSES u).ShortExact

The splitting-module sequence 0 → A → A(u) → I_G → 0 is short exact.

theorem Rep.splittingModuleSES_res_shortExact {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (u : ↑(groupCohomology A 2)) {H : Type u_1} [Monoid H] (f : H →* G) : ((A.splittingModuleSES u).map (resFunctor f)).ShortExact

The splitting-module sequence stays short exact after restriction along any monoid homomorphism f : H →* G.

noncomputable def Rep.splittingModuleCochain {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (u : ↑(groupCohomology A 2)) (g : G) : ↑(A.splittingModule u)

The one-cochain g ↦ ([g]-[1], g • c(1,1)) in the splitting module. Its coboundary is the image of the chosen representative c of u.

theorem Rep.splittingModuleCochain_coboundary {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (u : ↑(groupCohomology A 2)) (g h : G) : ((A.splittingModule u).ρ g) (A.splittingModuleCochain u h) - A.splittingModuleCochain u (g * h) + A.splittingModuleCochain u g = (CategoryTheory.ConcreteCategory.hom (A.splittingModuleIncl u)) ((A.h2Representative u) (g, h))

The coboundary of splittingModuleCochain is the image of the chosen cocycle representative under the inclusion A → A(u).

theorem Rep.splittingModuleIncl_comp_h2Representative_mem_coboundaries {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (u : ↑(groupCohomology A 2)) : ⇑(CategoryTheory.ConcreteCategory.hom (A.splittingModuleIncl u)) ∘ ⇑(A.h2Representative u) ∈ groupCohomology.coboundaries₂ (A.splittingModule u)

The composite of the chosen representative of u with the splitting-module inclusion is a coboundary.

@[simp]

theorem Rep.map_splittingModuleIncl_res_eq_zero {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (u : ↑(groupCohomology A 2)) {H : Type u} [Group H] (f : H →* G) : (CategoryTheory.ConcreteCategory.hom (groupCohomology.map f ((resFunctor f).map (A.splittingModuleIncl u)) 2)) u = 0

After restriction along any group homomorphism, the defining class u maps to zero in the second cohomology of the restricted splitting module.

@[simp]

theorem Rep.map_splittingModuleIncl_eq_zero {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (u : ↑(groupCohomology A 2)) : (CategoryTheory.ConcreteCategory.hom (groupCohomology.map (MonoidHom.id G) (A.splittingModuleIncl u) 2)) u = 0

The defining class u maps to zero in H²(G, A(u)).

theorem Rep.surjective_connecting_res_splittingModule {k G : Type u} [CommRing k] [Group G] (A : Rep k G) (u : ↑(groupCohomology A 2)) {H : Type u} [Group H] (f : H →* G) (hgen : ∀ (x : ↑(groupCohomology (res f A) 2)), ∃ (r : k), r • (CategoryTheory.ConcreteCategory.hom (groupCohomology.map f (CategoryTheory.CategoryStruct.id (res f A)) 2)) u = x) (hX : ({ X₁ := A, X₂ := A.splittingModule u, X₃ := augmentationIdeal k G, f := A.splittingModuleIncl u, g := A.splittingModuleProj u, zero := ⋯ }.map (resFunctor f)).ShortExact) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (groupCohomology.δ hX 1 2 ⋯))

The connecting map H¹(H, I_G) → H²(H, A) of the splitting module sequence restricted along a group homomorphism f : H → G is onto: u restricts to a generator of H²(H, A) and dies in the splitting module.