Primary submodules

A proper submodule S : Submodule R M is primary iff r • x ∈ S implies x ∈ S or ∃ n : ℕ, r ^ n • (⊤ : Submodule R M) ≤ S.

Main results

• Submodule.isPrimary_iff_zero_divisor_quotient_imp_nilpotent_smul: A N : Submodule R M is primary if any zero divisor on M ⧸ N is nilpotent. See https://mathoverflow.net/questions/3910/primary-decomposition-for-modules for a comparison of this definition (a la Atiyah-Macdonald) vs "locally nilpotent" (Matsumura).

Implementation details

This is a generalization of Ideal.IsPrimary. For brevity, the pointwise instances are used to define the nilpotency of r : R.

References

• M. F. Atiyah and I. G. Macdonald, Introduction to commutative algebra Chapter 4, Exercise 21.

def Submodule.IsPrimary {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (S : Submodule R M) : Prop

A proper submodule S : Submodule R M is primary iff r • x ∈ S implies x ∈ S or ∃ n : ℕ, r ^ n • (⊤ : Submodule R M) ≤ S. This generalizes Ideal.IsPrimary.

Equations

• S.IsPrimary = (S ≠ ⊤ ∧ ∀ {r : R} {x : M}, r • x ∈ S → x ∈ S ∨ ∃ (n : ℕ), r ^ n • ⊤ ≤ S)

theorem Submodule.IsPrimary.ne_top {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {S : Submodule R M} (h : S.IsPrimary) : S ≠ ⊤

theorem Submodule.isPrimary_iff_zero_divisor_quotient_imp_nilpotent_smul {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] {S : Submodule R M} : S.IsPrimary ↔ S ≠ ⊤ ∧ ∀ (r : R) (x : M ⧸ S), x ≠ 0 → r • x = 0 → ∃ (n : ℕ), r ^ n • ⊤ = ⊥