Second cohomology in Lyndon's relation-module coordinates

For a finite group presented by a finite generating family, Lyndon's isomorphism identifies its pro-p relation group with the integral group-algebra relation module. This file reads explicit continuous second cohomology of the former as algebraic second cohomology of the latter, retaining the action of the presented group. Thus a map of algebraic relation modules can be compared with a coefficient map on the kernels of profinite extensions.

The coefficient identification is abelianizationProPEquivRelationModule, and the cohomology identification is ContCohomology.explicitH2AddEquivGroupCohomology at that compatible pair.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, 2nd ed., (5.6.6) and the proof of (7.4.1).

noncomputable def TauCeti.freeProfiniteGroup.explicitH2EquivRelationModule (p : ℕ) [Fact (Nat.Prime p)] {G ι : Type} [Group G] [Finite G] [TopologicalSpace G] [DiscreteTopology G] [Fintype ι] [DecidableEq ι] {g : ι → G} (hg : Subgroup.closure (Set.range g) = ⊤) : ContCohomology.H2 G (Additive (abelianizationProP p (↑(freeProfiniteGroup ι).toProfinite.toTop) (↑(lift g)).ker)) ≃+ ↑(groupCohomology (Rep.ofModuleMonoidAlgebra.obj ↧↥(MonoidAlgebra.relationModule ℤ_[p] G g)) 2)

Explicit second cohomology of the pro-p relation group, with the presented group's conjugation action, is second cohomology of its integral relation-module representation.

theorem TauCeti.freeProfiniteGroup.explicitH2EquivRelationModule_eq_explicitH2AddEquivGroupCohomology (p : ℕ) [Fact (Nat.Prime p)] {G ι : Type} [Group G] [Finite G] [TopologicalSpace G] [DiscreteTopology G] [Fintype ι] [DecidableEq ι] {g : ι → G} (hg : Subgroup.closure (Set.range g) = ⊤) : let B := Rep.ofModuleMonoidAlgebra.obj ↧↥(MonoidAlgebra.relationModule ℤ_[p] G g); ∀ (ψ : Additive (abelianizationProP p (↑(freeProfiniteGroup ι).toProfinite.toTop) (↑(lift g)).ker) ≃+ ↑B) (hψ : ∀ (t : G) (x : Additive (abelianizationProP p (↑(freeProfiniteGroup ι).toProfinite.toTop) (↑(lift g)).ker)), ψ (t • x) = (B.ρ t) (ψ x)), ψ = (abelianizationProPEquivRelationModule p hg).trans (RestrictScalars.addEquiv ℤ_[p] (MonoidAlgebra ℤ_[p] G) ↥(MonoidAlgebra.relationModule ℤ_[p] G g)).symm → explicitH2EquivRelationModule p hg = ContCohomology.explicitH2AddEquivGroupCohomology (MulEquiv.refl G) ψ hψ

The relation-module comparison is the generic comparison in any equal coefficient coordinates. This characterization keeps its construction opaque to consumers.

theorem TauCeti.freeProfiniteGroup.explicitH2EquivRelationModule_mk (p : ℕ) [Fact (Nat.Prime p)] {G ι : Type} [Group G] [Finite G] [TopologicalSpace G] [DiscreteTopology G] [Fintype ι] [DecidableEq ι] {g : ι → G} (hg : Subgroup.closure (Set.range g) = ⊤) (z : ↥(ContCohomology.Z2 G (Additive (abelianizationProP p (↑(freeProfiniteGroup ι).toProfinite.toTop) (↑(lift g)).ker)))) (c : ↥(groupCohomology.cocycles₂ (Rep.ofModuleMonoidAlgebra.obj ↧↥(MonoidAlgebra.relationModule ℤ_[p] G g)))) : (∀ (t : G × G), c t = (abelianizationProPEquivRelationModule p hg) (↑z t)) → (explicitH2EquivRelationModule p hg) ↑z = (CategoryTheory.ConcreteCategory.hom (groupCohomology.H2π (Rep.ofModuleMonoidAlgebra.obj ↧↥(MonoidAlgebra.relationModule ℤ_[p] G g)))) c

The comparison sends a cocycle class to that same cocycle in Lyndon's coordinates.