The relation module of a family of group elements

For a family g : ι → G of elements of a group, indexed by a finite type, the left R[G]-linear map R[G]^ι → R[G], e_i ↦ g_i - 1, lands in the augmentation ideal I_G, the kernel of TauCeti.MonoidAlgebra.augmentation R G. Its kernel is the relation module of the family. When the g_i generate G, the map is onto I_G, giving Lyndon's exact sequence 0 → relationModule R G g → R[G]^ι → I_G → 0.

When G is a group, the g_i generate G and R = ℤ, the relation module is the abelianised relation group N^ab of the presentation 1 → N → F → G → 1 of G by the free group F on the g_i, with its conjugation action of G (Lyndon's identification, NSW (5.6.6)). Since ℤ[G]^ι and I_G are free abelian groups, for a general ring R it is the scalar extension R ⊗_ℤ N^ab. Here the kernel is taken as the definition, so no group-theoretic carrier is needed. The module R^ab(p) compared with the p-completed units of a local field in the computation of the generator rank of its absolute Galois group (NSW (7.4.1)) is its analogue over R = ℤ_p.

Main definitions

• TauCeti.MonoidAlgebra.relationModule: the kernel of R[G]^ι → R[G], e_i ↦ g_i - 1.

Main statements

• TauCeti.MonoidAlgebra.relationModule_def: the relation module as the kernel of e_i ↦ g_i - 1.
• TauCeti.MonoidAlgebra.mem_relationModule_iff: membership as the relation ∑ c_i (g_i - 1) = 0.
• TauCeti.MonoidAlgebra.range_linearCombination_le_ker_augmentation: the map lands in I_G.
• TauCeti.MonoidAlgebra.mapRingHom_linearCombination: the map commutes with changing coefficients along a ring homomorphism.
• TauCeti.MonoidAlgebra.range_linearCombination_eq_ker_augmentation: the map is onto I_G when the g_i generate G, and range_linearCombination_eq_ker_augmentation_iff is the converse over a nontrivial ring.

References

• J. Neukirch, A. Schmidt, K. Wingberg, Cohomology of Number Fields, (5.6.6) and (7.4.1).
• R. C. Lyndon, Cohomology theory of groups with a single defining relation, Ann. of Math. 52 (1950).

noncomputable def TauCeti.MonoidAlgebra.relationModule (R : Type u) [Ring R] (G : Type v) {ι : Type w} [Fintype ι] [Monoid G] (g : ι → G) : Submodule (MonoidAlgebra R G) (ι → MonoidAlgebra R G)

The relation module of a family g : ι → G: the kernel of the left R[G]-linear map R[G]^ι → R[G] sending the i-th basis vector to g_i - 1. For a generating family of a group it is R ⊗_ℤ N^ab, for N^ab the relation module of the presentation of G on the g_i (NSW (5.6.6)); for R = ℤ it is N^ab itself.

Equations

• TauCeti.MonoidAlgebra.relationModule R G g = (Fintype.linearCombination (MonoidAlgebra R G) fun (i : ι) => MonoidAlgebra.single (g i) 1 - 1).ker

theorem TauCeti.MonoidAlgebra.relationModule_def {R : Type u} [Ring R] {G : Type v} {ι : Type w} [Fintype ι] [Monoid G] (g : ι → G) : relationModule R G g = (Fintype.linearCombination (MonoidAlgebra R G) fun (i : ι) => MonoidAlgebra.single (g i) 1 - 1).ker

The relation module of g is the kernel of the map R[G]^ι → R[G], e_i ↦ g_i - 1.

@[simp]

theorem TauCeti.MonoidAlgebra.mem_relationModule_iff {R : Type u} [Ring R] {G : Type v} {ι : Type w} [Fintype ι] [Monoid G] {g : ι → G} {c : ι → MonoidAlgebra R G} : c ∈ relationModule R G g ↔ ∑ i : ι, c i * (MonoidAlgebra.single (g i) 1 - 1) = 0

A family of coefficients lies in the relation module of g exactly when ∑ c_i (g_i - 1) = 0.

theorem TauCeti.MonoidAlgebra.range_linearCombination_le_ker_augmentation {R : Type u} [Ring R] {G : Type v} {ι : Type w} [Fintype ι] [Monoid G] (g : ι → G) : (Fintype.linearCombination (MonoidAlgebra R G) fun (i : ι) => MonoidAlgebra.single (g i) 1 - 1).range ≤ RingHom.ker (augmentation R G)

The map e_i ↦ g_i - 1 lands in the augmentation ideal.

@[simp]

theorem TauCeti.MonoidAlgebra.mapRingHom_linearCombination {R : Type u} [Ring R] {G : Type v} {ι : Type w} [Fintype ι] [Monoid G] {S : Type u_1} [Ring S] (f : R →+* S) (g : ι → G) (c : ι → MonoidAlgebra R G) : (MonoidAlgebra.mapRingHom G f) ((Fintype.linearCombination (MonoidAlgebra R G) fun (i : ι) => MonoidAlgebra.single (g i) 1 - 1) c) = (Fintype.linearCombination (MonoidAlgebra S G) fun (i : ι) => MonoidAlgebra.single (g i) 1 - 1) fun (i : ι) => (MonoidAlgebra.mapRingHom G f) (c i)

Changing coefficients along a ring homomorphism f : R →+* S commutes with the map e_i ↦ g_i - 1.

theorem TauCeti.MonoidAlgebra.range_linearCombination_eq_ker_augmentation {R : Type u} [Ring R] {G : Type v} {ι : Type w} [Fintype ι] [Group G] {g : ι → G} (hg : Subgroup.closure (Set.range g) = ⊤) : (Fintype.linearCombination (MonoidAlgebra R G) fun (i : ι) => MonoidAlgebra.single (g i) 1 - 1).range = RingHom.ker (augmentation R G)

Lyndon's sequence is exact at I_G. When the g_i generate G, the map e_i ↦ g_i - 1 is onto the augmentation ideal, so 0 → relationModule R G g → R[G]^ι → I_G → 0 is exact.

theorem TauCeti.MonoidAlgebra.range_linearCombination_eq_ker_augmentation_iff {R : Type u} [Ring R] {G : Type v} {ι : Type w} [Fintype ι] [Group G] [Nontrivial R] {g : ι → G} : (Fintype.linearCombination (MonoidAlgebra R G) fun (i : ι) => MonoidAlgebra.single (g i) 1 - 1).range = RingHom.ker (augmentation R G) ↔ Subgroup.closure (Set.range g) = ⊤

Over a nontrivial ring, the map e_i ↦ g_i - 1 is onto the augmentation ideal exactly when the g_i generate G.