Exact sequences of group-algebra modules split after a flat division-ring extension

Let R be a commutative ring, Q a division ring that is a flat R-algebra, and G a finite group whose order is nonzero in Q. 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 over Q. 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]. The main example is a domain R with field of fractions Q, where the order of G is nonzero in Q as soon as it is nonzero in R.

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 free Q-module, 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.MonoidAlgebra.nonempty_tensor_linearEquiv_prod_of_exact: for an exact sequence 0 → M → N → P → 0 of R[G]-modules, the scalar extension 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.MonoidAlgebra.nonempty_tensor_linearEquiv_prod_of_exact {R : Type u_1} [CommRing R] (Q : Type u_2) [DivisionRing Q] [Algebra R Q] [Module.Flat 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 after a flat division-ring extension. Let Q be a division ring that is a flat R-algebra and G a finite group whose order is nonzero in Q. For an exact sequence 0 → M → N → P → 0 of R[G]-modules, the scalar extension N ⊗[R] Q is R[G]-linearly isomorphic to (M × P) ⊗[R] Q.