ℤ/nℤ is an injective module over itself

For n ≠ 0 the ring ℤ/nℤ is self-injective: every ℤ/nℤ-linear map from an ideal of ℤ/nℤ to ℤ/nℤ extends to the whole ring, which is Baer's criterion (Module.Baer) for the module ℤ/nℤ over itself. Consequently Hom(-, ℤ/nℤ) is exact on the abelian groups killed by n, which is what makes the dual M ↦ Hom(M, ℤ/nℤ) of a finite abelian group of exponent dividing n behave like the dual of a vector space; the duality statements for the finite ℤ/pⁱ[G]-modules of a profinite group rest on this.

The proof is the usual one, and adapts Mathlib's Module.Baer.of_divisible (Mathlib/Algebra/Category/Grp/Injective.lean, Baer's criterion for a divisible group over ℤ) from ℤ to ℤ/nℤ. An ideal of ℤ/nℤ is generated by one element d, and a linear map on it is determined by the image x of d, which is killed by every r killing d. In ℤ/nℤ that forces d ∣ x (ZMod.dvd_of_forall_mul_eq_zero, which replaces the division DivisibleBy.div of the divisible case): if g = gcd(d, n), then n/g kills d, hence x, so g divides x, and g is a multiple of d by Bézout. Writing x = d y, the map r ↦ r y is the required extension. The hypothesis n ≠ 0 is necessary: ℤ is not injective over itself, since the map 2ℤ → ℤ, 2 ↦ 1, does not extend.

Main results

• Module.Baer.zmod_self: ℤ/nℤ satisfies Baer's criterion over itself, for n ≠ 0.
• Module.Baer.of_addEquiv_zmod: a ℤ/nℤ-module isomorphic to ℤ/nℤ as an additive group satisfies Baer's criterion, for n ≠ 0.
• Module.Baer.exists_module_of_addEquiv_zmod: an additive group isomorphic to ℤ/nℤ carries a ℤ/nℤ-module structure satisfying Baer's criterion, for n ≠ 0.

theorem Module.Baer.zmod_self (n : ℕ) [NeZero n] : Baer (ZMod n) (ZMod n)

ℤ/nℤ is self-injective, in the form of Baer's criterion: for n ≠ 0, every ZMod n-linear map from an ideal of ZMod n to ZMod n extends to a linear map on ZMod n. By Module.Baer.extension_property, every ZMod n-linear map into ZMod n then extends along any injective linear map of ZMod n-modules. The proof follows Mathlib's Module.Baer.of_divisible with ZMod.dvd_of_forall_mul_eq_zero in place of DivisibleBy.div.

theorem Module.Baer.of_addEquiv_zmod {n : ℕ} [NeZero n] {W : Type u_1} [AddCommGroup W] [Module (ZMod n) W] (e : W ≃+ ZMod n) : Baer (ZMod n) W

A ℤ/nℤ-module additively isomorphic to ℤ/nℤ is self-injective: for n ≠ 0, a ZMod n-module W with an additive isomorphism W ≃+ ZMod n satisfies Baer's criterion over ZMod n. Every additive homomorphism of ZMod n-modules is linear, so the isomorphism transports Module.Baer.zmod_self.

theorem Module.Baer.exists_module_of_addEquiv_zmod {n : ℕ} [NeZero n] {W : Type u_1} [AddCommGroup W] (e : W ≃+ ZMod n) : ∃ (x : Module (ZMod n) W), Baer (ZMod n) W

An additive group isomorphic to ℤ/nℤ is a self-injective ℤ/nℤ-module: for n ≠ 0, an additive group W with W ≃+ ZMod n is killed by n, so it carries a ZMod n-module structure (AddCommGroup.zmodModule), and for it W satisfies Baer's criterion over ZMod n (Module.Baer.of_addEquiv_zmod).