Lasker ring

Main declarations

• IsLasker: A ring R satisfies IsLasker R when any I : Ideal R can be decomposed into finitely many primary ideals.
• IsLasker.minimal: Any I : Ideal R in a ring R satisfying IsLasker R can be decomposed into primary ideals, such that the decomposition is minimal: each primary ideal is necessary, and each primary ideal has an independent radical.
• Ideal.isLasker: Every Noetherian commutative ring is a Lasker ring.

Implementation details

There is a generalization for submodules that needs to be implemented. Also, one needs to prove that the radicals of minimal decompositions are independent of the precise decomposition.

def IsLasker (R : Type u_1) [CommSemiring R] : Prop

A ring R satisfies IsLasker R when any I : Ideal R can be decomposed into finitely many primary ideals.

Equations

• IsLasker R = ∀ (I : Ideal R), ∃ (s : Finset (Ideal R)), s.inf id = I ∧ ∀ ⦃J : Ideal R⦄, J ∈ s → J.IsPrimary

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

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

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

structure Ideal.IsMinimalPrimaryDecomposition {R : Type u_1} [CommSemiring R] [DecidableEq (Ideal R)] (I : Ideal R) (t : Finset (Ideal R)) : Prop

A Finset of ideals is a maximal primary decomposition of I if the ideals intersect to I, are primary, have pairwise distinct radicals, and removing any ideal changes the intersection.

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

theorem Ideal.IsLasker.exists_isMinimalPrimaryDecomposition {R : Type u_1} [CommSemiring R] [DecidableEq (Ideal R)] (h : IsLasker R) (I : Ideal R) : ∃ (t : Finset (Ideal R)), I.IsMinimalPrimaryDecomposition t

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

theorem Ideal.IsLasker.minimal {R : Type u_1} [CommSemiring R] [DecidableEq (Ideal R)] (h : IsLasker R) (I : Ideal R) : ∃ (t : Finset (Ideal R)), I.IsMinimalPrimaryDecomposition t

Alias of Ideal.IsLasker.exists_isMinimalPrimaryDecomposition.

theorem InfIrred.isPrimary {R : Type u_1} [CommRing R] [IsNoetherianRing R] {I : Ideal R} (h : InfIrred I) : I.IsPrimary

theorem Ideal.isLasker (R : Type u_1) [CommRing R] [IsNoetherianRing R] : IsLasker R

The Lasker--Noether theorem: every ideal in a Noetherian ring admits a decomposition into primary ideals.