Documentation

TauCeti.Algebra.MonoidAlgebra.RelationModule.FractionRing

The rational representation of a relation module #

Let R be a domain with field of fractions Q, let G be a finite group whose order is nonzero in R, and let g : ι → G be a generating family with n + 1 members. The relation module of g is the kernel of R[G]^ι → I_G, e_i ↦ g_i - 1, so it sits in Lyndon's exact sequence

0 → relationModule R G g → R[G]^ι → I_G → 0.

After tensoring with Q this sequence and the augmentation sequence 0 → I_G → R[G] → R → 0 split (Maschke's theorem, TauCeti.MonoidAlgebra.nonempty_tensor_linearEquiv_prod_of_exact), and cancelling the rational regular representation gives

relationModule R G g ⊗ Q ≃ (R[G]^n ⊕ R) ⊗ Q,

that is, the rationalized relation module is Q[G]^n ⊕ Q: n copies of the regular representation and one trivial representation. Its rational representation depends only on the number of generators, not on the group-theoretic relations among them.

For R = ℤ_p and n + 1 = [K : ℚ_p] + 2 this is the rational shape of R^ab(p) for a finite Galois layer of a p-adic field K. Comparing it with the rational decomposition of the p-adic completion of the units of that layer computes the rational representation of the kernel of a surjection between them, which is how that kernel is identified integrally in the proof of NSW (7.4.2)(i).

Main results #

References #

theorem TauCeti.MonoidAlgebra.nonempty_relationModule_tensor_linearEquiv {R : Type u_1} [CommRing R] (Q : Type u_2) [Field Q] [Algebra R Q] [IsFractionRing R Q] {G : Type u_3} [Group G] [Finite G] {ι : Type u_4} [Fintype ι] [NeZero ↑(Nat.card G)] {g : ι → G} (hg : Subgroup.closure (Set.range g) = ⊤) {n : ℕ} (hι : Fintype.card ι = n + 1) :

The rational representation of a relation module (Gaschütz). Let R be a domain with field of fractions Q and G a finite group whose order is nonzero in R. For a generating family g of G with n + 1 members, the rationalized relation module of g is R[G]-linearly isomorphic to (R[G]^n × R[G] ⧸ I_G) ⊗[R] Q, that is, to Q[G]^n ⊕ Q.