Relation modules of a finite group over a local ring

Let G be a finite group and R a local ring. A generating family g : ι → G indexed by a finite type gives Lyndon's exact sequence 0 → relationModule R G g → R[G]^ι → I_G → 0. This file proves that for two generating families g and g' indexed by finite types of the same cardinality the presentation maps onto I_G differ by an isomorphism of the free modules, so that the relation module depends, up to isomorphism, only on the group and the number of generators. No completeness of R is needed. For R = ℤ_p this is the independence of R^ab(p) from the chosen generators used in the computation of the generator rank of the absolute Galois group of a p-adic field (NSW (5.6.6), (7.4.1)).

Main results

• TauCeti.MonoidAlgebra.exists_linearEquiv_linearCombination_comp_eq: the presentation maps e_i ↦ g_i - 1 and e_k ↦ g'_k - 1 of two generating families of the same size differ by an isomorphism of free modules.
• TauCeti.MonoidAlgebra.nonempty_relationModule_linearEquiv_of_closure: two generating families of the same size have isomorphic relation modules.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, second edition, (5.6.6), (5.6.10) and (7.4.1).
• K. W. Gruenberg, Relation modules of finite groups, CBMS Regional Conference Series in Mathematics 25, American Mathematical Society (1976).

theorem TauCeti.MonoidAlgebra.exists_linearEquiv_linearCombination_comp_eq (R : Type u) [CommRing R] [IsLocalRing R] {G : Type v} [Group G] {ι : Type w} [Fintype ι] [Finite G] {κ : Type u_1} [Fintype κ] (hcard : Nat.card ι = Nat.card κ) {g : ι → G} {g' : κ → G} (hg : Subgroup.closure (Set.range g) = ⊤) (hg' : Subgroup.closure (Set.range g') = ⊤) : ∃ (θ : (ι → MonoidAlgebra R G) ≃ₗ[MonoidAlgebra R G] κ → MonoidAlgebra R G), (Fintype.linearCombination (MonoidAlgebra R G) fun (k : κ) => MonoidAlgebra.single (g' k) 1 - 1) ∘ₗ ↑θ = Fintype.linearCombination (MonoidAlgebra R G) fun (i : ι) => MonoidAlgebra.single (g i) 1 - 1

Two generating families of the same size give isomorphic presentations. For generating families g : ι → G and g' : κ → G of a finite group G, indexed by finite types of the same cardinality, and a local ring R, the maps R[G]^ι → R[G], e_i ↦ g_i - 1, and R[G]^κ → R[G], e_k ↦ g'_k - 1, differ by an isomorphism R[G]^ι ≃ R[G]^κ.

theorem TauCeti.MonoidAlgebra.nonempty_relationModule_linearEquiv_of_closure (R : Type u) [CommRing R] [IsLocalRing R] {G : Type v} [Group G] {ι : Type w} [Fintype ι] [Finite G] {κ : Type u_1} [Fintype κ] (hcard : Nat.card ι = Nat.card κ) {g : ι → G} {g' : κ → G} (hg : Subgroup.closure (Set.range g) = ⊤) (hg' : Subgroup.closure (Set.range g') = ⊤) : Nonempty (↥(relationModule R G g) ≃ₗ[MonoidAlgebra R G] ↥(relationModule R G g'))

The relation module depends only on the number of generators. Two generating families of a finite group G, indexed by finite types of the same cardinality, have isomorphic relation modules over the group algebra R[G] of G over a local ring R.