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.mem_or_mem {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {S : Submodule R M} (h : S.IsPrimary) {r : R} {m : M} (hrm : r • m ∈ S) : m ∈ S ∨ r ∈ (S.colon Set.univ).radical

theorem Submodule.IsPrimary.inf {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {S T : Submodule R M} (hS : S.IsPrimary) (hT : T.IsPrimary) (h : (S.colon Set.univ).radical = (T.colon Set.univ).radical) : (S ⊓ T).IsPrimary

theorem Submodule.isPrimary_finsetInf {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {ι : Type u_3} {s : Finset ι} {f : ι → Submodule R M} {i : ι} (hi : i ∈ s) (hs : ∀ ⦃y : ι⦄, y ∈ s → (f y).IsPrimary) (hs' : ∀ ⦃y : ι⦄, y ∈ s → ((f y).colon Set.univ).radical = ((f i).colon Set.univ).radical) : (s.inf f).IsPrimary

theorem Submodule.IsPrimary.isPrime_radical_colon {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {S : Submodule R M} (hI : S.IsPrimary) : (S.colon Set.univ).radical.IsPrime

theorem Submodule.IsPrimary.radical_colon_singleton_of_notMem {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {S : Submodule R M} (hI : S.IsPrimary) {m : M} (hm : m ∉ S) : (S.colon {m}).radical = (S.colon Set.univ).radical

theorem Submodule.IsPrimary.radical_colon_singleton_eq_ite {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {S : Submodule R M} (hS : S.IsPrimary) (m : M) [Decidable (m ∈ S)] : (S.colon {m}).radical = if m ∈ S then ⊤ else (S.colon Set.univ).radical

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 • ⊤ = ⊥