Exact sequences of group-algebra modules split over the field of fractions

Let R be a domain with field of fractions Q and let G be a finite group whose order is nonzero in R. A short exact sequence 0 → M → N → P → 0 of R[G]-modules need not split, but it does after tensoring with Q: this is Maschke's theorem for Q[G]. This file proves it in the form used for integral representations, where the rationalizations are written M ⊗[R] Q and remain modules over R[G] rather than over Q[G].

No finiteness or projectivity is needed. Since Q is flat over R, the sequence stays exact after tensoring with Q, and P ⊗[R] Q is a Q-vector space, so N ⊗ Q → P ⊗ Q has an R-linear section s. Averaged over G, t = ∑_g g⁻¹ s g is R[G]-linear and satisfies g ∘ t = #G. As #G is invertible on P ⊗[R] Q, the map (m, x) ↦ f m + t x from (M ⊗ Q) × (P ⊗ Q) to N ⊗ Q is then an R[G]-linear bijection.

For R = ℤ_p and Q = ℚ_p this computes the rational representation of an extension of ℤ_p[G]-lattices from those of its two ends.

Main results

• TauCeti.IsFractionRing.nonempty_tensor_linearEquiv_prod_of_exact: for an exact sequence 0 → M → N → P → 0 of R[G]-modules, the rationalization N ⊗[R] Q is R[G]-linearly isomorphic to (M × P) ⊗[R] Q.

References

• J.-P. Serre, Linear Representations of Finite Groups, Springer GTM 42 (1977), §1.3 and §15.

theorem TauCeti.IsFractionRing.nonempty_tensor_linearEquiv_prod_of_exact {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] {M : Type u_4} {N : Type u_5} {P : Type u_6} [AddCommGroup M] [Module R M] [Module (MonoidAlgebra R G) M] [IsScalarTower R (MonoidAlgebra R G) M] [AddCommGroup N] [Module R N] [Module (MonoidAlgebra R G) N] [IsScalarTower R (MonoidAlgebra R G) N] [AddCommGroup P] [Module R P] [Module (MonoidAlgebra R G) P] [IsScalarTower R (MonoidAlgebra R G) P] [NeZero ↑(Nat.card G)] {f : M →ₗ[MonoidAlgebra R G] N} {g : N →ₗ[MonoidAlgebra R G] P} (hfg : Function.Exact ⇑f ⇑g) (hf : Function.Injective ⇑f) (hg : Function.Surjective ⇑g) : Nonempty (TensorProduct R N Q ≃ₗ[MonoidAlgebra R G] TensorProduct R (M × P) Q)

Short exact sequences of group-algebra modules split over the field of fractions. Let R be a domain with field of fractions Q and G a finite group whose order is nonzero in R. For an exact sequence 0 → M → N → P → 0 of R[G]-modules, the rationalization N ⊗[R] Q is R[G]-linearly isomorphic to (M × P) ⊗[R] Q.