Lasker ring

Main declarations

• IsLasker: An R-module M satisfies IsLasker R M when any N : Submodule R M can be decomposed into finitely many primary submodules.
• IsLasker.exists_isMinimalPrimaryDecomposition: Any N : Submodule R N in an R-module M satisfying IsLasker R M can be decomposed into finitely many primary submodules Nᵢ, such that the decomposition is minimal: each Nᵢ is necessary, and the √Ann(M/Nᵢ) are distinct.
• Submodule.isLasker: Every Noetherian module is Lasker.

TODO

One needs to prove that the radicals of minimal decompositions are independent of the precise decomposition.

def IsLasker (R : Type u_1) (M : Type u_2) [CommSemiring R] [AddCommMonoid M] [Module R M] : Prop

An R-module M satisfies IsLasker R M when any N : Submodule R M can be decomposed into finitely many primary submodules.

theorem Submodule.decomposition_erase_inf {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq (Submodule R M)] {N : Submodule R M} {s : Finset (Submodule R M)} (hs : s.inf id = N) : ∃ t ⊆ s, t.inf id = N ∧ ∀ ⦃J : Submodule R M⦄, J ∈ t → ¬(t.erase J).inf id ≤ J

theorem Submodule.isPrimary_decomposition_pairwise_ne_radical {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} {s : Finset (Submodule R M)} (hs : s.inf id = N) (hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary) : ∃ (t : Finset (Submodule R M)), t.inf id = N ∧ (∀ ⦃J : Submodule R M⦄, J ∈ t → J.IsPrimary) ∧ (↑t).Pairwise (Function.onFun (fun (x1 x2 : Ideal R) => x1 ≠ x2) fun (J : Submodule R M) => (J.colon Set.univ).radical)

theorem Submodule.exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq (Submodule R M)] {N : Submodule R M} {s : Finset (Submodule R M)} (hs : s.inf id = N) (hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary) : ∃ (t : Finset (Submodule R M)), t.inf id = N ∧ (∀ ⦃J : Submodule R M⦄, J ∈ t → J.IsPrimary) ∧ (↑t).Pairwise (Function.onFun (fun (x1 x2 : Ideal R) => x1 ≠ x2) fun (J : Submodule R M) => (J.colon Set.univ).radical) ∧ ∀ ⦃J : Submodule R M⦄, J ∈ t → ¬(t.erase J).inf id ≤ J

structure Submodule.IsMinimalPrimaryDecomposition {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq (Submodule R M)] (N : Submodule R M) (t : Finset (Submodule R M)) : Prop

A Finset of submodules is a minimal primary decomposition of N if the submodules Nᵢ intersect to N, are primary, the √Ann(M/Nᵢ) are distinct, and each Nᵢ is necessary.

• inf_eq : t.inf id = N
• primary ⦃J : Submodule R M⦄ : J ∈ t → J.IsPrimary
• distinct : (↑t).Pairwise (Function.onFun (fun (x1 x2 : Ideal R) => x1 ≠ x2) fun (J : Submodule R M) => (J.colon Set.univ).radical)
• minimal ⦃J : Submodule R M⦄ : J ∈ t → ¬(t.erase J).inf id ≤ J

theorem Submodule.IsLasker.exists_isMinimalPrimaryDecomposition {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq (Submodule R M)] (h : IsLasker R M) (N : Submodule R M) : ∃ (t : Finset (Submodule R M)), N.IsMinimalPrimaryDecomposition t

theorem Ideal.IsMinimalPrimaryDecomposition.minimalPrimes_subset_image_radical {R : Type u_1} [CommSemiring R] [DecidableEq (Ideal R)] {I : Ideal R} {t : Finset (Ideal R)} (ht : Submodule.IsMinimalPrimaryDecomposition I t) : I.minimalPrimes ⊆ radical '' ↑t

@[deprecated Submodule.decomposition_erase_inf (since := "2026-01-19")]

theorem Ideal.decomposition_erase_inf {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq (Submodule R M)] {N : Submodule R M} {s : Finset (Submodule R M)} (hs : s.inf id = N) : ∃ t ⊆ s, t.inf id = N ∧ ∀ ⦃J : Submodule R M⦄, J ∈ t → ¬(t.erase J).inf id ≤ J

Alias of Submodule.decomposition_erase_inf.

@[deprecated Submodule.isPrimary_decomposition_pairwise_ne_radical (since := "2026-01-19")]

theorem Ideal.isPrimary_decomposition_pairwise_ne_radical {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} {s : Finset (Submodule R M)} (hs : s.inf id = N) (hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary) : ∃ (t : Finset (Submodule R M)), t.inf id = N ∧ (∀ ⦃J : Submodule R M⦄, J ∈ t → J.IsPrimary) ∧ (↑t).Pairwise (Function.onFun (fun (x1 x2 : Ideal R) => x1 ≠ x2) fun (J : Submodule R M) => (J.colon Set.univ).radical)

Alias of Submodule.isPrimary_decomposition_pairwise_ne_radical.

@[deprecated Submodule.exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition (since := "2026-01-19")]

theorem Ideal.exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq (Submodule R M)] {N : Submodule R M} {s : Finset (Submodule R M)} (hs : s.inf id = N) (hs' : ∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary) : ∃ (t : Finset (Submodule R M)), t.inf id = N ∧ (∀ ⦃J : Submodule R M⦄, J ∈ t → J.IsPrimary) ∧ (↑t).Pairwise (Function.onFun (fun (x1 x2 : Ideal R) => x1 ≠ x2) fun (J : Submodule R M) => (J.colon Set.univ).radical) ∧ ∀ ⦃J : Submodule R M⦄, J ∈ t → ¬(t.erase J).inf id ≤ J

Alias of Submodule.exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition.

@[deprecated Submodule.IsMinimalPrimaryDecomposition (since := "2026-01-19")]

def Ideal.IsMinimalPrimaryDecomposition {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq (Submodule R M)] (N : Submodule R M) (t : Finset (Submodule R M)) : Prop

Alias of Submodule.IsMinimalPrimaryDecomposition.

---

A Finset of submodules is a minimal primary decomposition of N if the submodules Nᵢ intersect to N, are primary, the √Ann(M/Nᵢ) are distinct, and each Nᵢ is necessary.

@[deprecated Submodule.IsLasker.exists_isMinimalPrimaryDecomposition (since := "2026-01-19")]

theorem Ideal.IsLasker.exists_isMinimalPrimaryDecomposition {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq (Submodule R M)] (h : IsLasker R M) (N : Submodule R M) : ∃ (t : Finset (Submodule R M)), N.IsMinimalPrimaryDecomposition t

Alias of Submodule.IsLasker.exists_isMinimalPrimaryDecomposition.

@[deprecated Submodule.IsLasker.exists_isMinimalPrimaryDecomposition (since := "2026-01-19")]

theorem Ideal.IsLasker.minimal {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] [DecidableEq (Submodule R M)] (h : IsLasker R M) (N : Submodule R M) : ∃ (t : Finset (Submodule R M)), N.IsMinimalPrimaryDecomposition t

Alias of Submodule.IsLasker.exists_isMinimalPrimaryDecomposition.

theorem InfIrred.isPrimary {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [IsNoetherian R M] {N : Submodule R M} (h : InfIrred N) : N.IsPrimary

theorem Submodule.isLasker (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] [IsNoetherian R M] : IsLasker R M

The Lasker--Noether theorem: every submodule in a Noetherian module admits a decomposition into primary submodules.

@[deprecated Submodule.isLasker (since := "2026-01-19")]

theorem Ideal.isLasker (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] [IsNoetherian R M] : IsLasker R M

Alias of Submodule.isLasker.

---

The Lasker--Noether theorem: every submodule in a Noetherian module admits a decomposition into primary submodules.