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 satisifying 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 indepedent 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 ((fun (x1 x2 : Ideal R) => x1 ≠ x2) on Ideal.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 ((fun (x1 x2 : Ideal R) => x1 ≠ x2) on Ideal.radical) ∧ ∀ ⦃J : Ideal R⦄, J ∈ t → ¬(t.erase J).inf id ≤ J

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

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.