Injective modules over principal ideal rings

If multiplication by each nonzero scalar is surjective on a module over a principal ideal ring, the module satisfies Baer's criterion and is injective.

A division algebra faithfully containing the scalar ring has this divisibility property, as does its quotient by any submodule. In particular, ℚ_p / ℤ_p is injective over ℤ_p. Thus a ℚ_p / ℤ_p-valued character of a torsion submodule extends to the whole module, without a splitting or finite-generation assumption. This is the extension property used in torsion duality.

Main results

• Module.Baer.of_surjective_smul: scalar divisibility implies Baer's criterion.
• Submodule.injective_quotient_of_divisionRing: quotients of a faithful division algebra are injective over a principal ideal ring.

theorem Module.Baer.of_surjective_smul {R : Type u_1} {M : Type u_2} [Ring R] [IsPrincipalIdealRing R] [AddCommGroup M] [Module R M] (h : ∀ (r : R), r ≠ 0 → Function.Surjective fun (x : M) => r • x) : Baer R M

A module over a principal ideal ring satisfies Baer's criterion if multiplication by each nonzero scalar is surjective.

instance Submodule.injective_quotient_of_divisionRing {R : Type u_1} {K : Type u_2} [CommRing R] [IsPrincipalIdealRing R] [DivisionRing K] [Algebra R K] [FaithfulSMul R K] (S : Submodule R K) : Module.Injective R (K ⧸ S)

Every quotient of a division algebra faithfully containing a principal ideal ring is injective as a module over that ring. In particular, this applies to the quotient of a fraction field by any submodule, such as ℚ_p / ℤ_p over ℤ_p.