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.
• IsMinimalPrimaryDecomposition.image_radical_eq_associated_primes: The first uniqueness theorem for primary decomposition, Theorem 4.5 in Atiyah-Macdonald: In any minimal primary decomposition I = ⨅ i, q_i, the ideals radical (q_i.colon M) are exactly the associated primes of I.
• Submodule.isLasker: Every Noetherian module is Lasker.

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.

Equations

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

theorem Submodule.decomposition_erase_inf {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) : ∃ 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] {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] (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] (h : IsLasker R M) (N : Submodule R M) : ∃ (t : Finset (Submodule R M)), N.IsMinimalPrimaryDecomposition t

theorem Submodule.IsMinimalPrimaryDecomposition.injOn {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] (N : Submodule R M) (t : Finset (Submodule R M)) (ht : N.IsMinimalPrimaryDecomposition t) : Set.InjOn (fun (J : Submodule R M) => (J.colon Set.univ).radical) ↑t

theorem Submodule.IsMinimalPrimaryDecomposition.image_radical_eq_associated_primes {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} {t : Finset (Submodule R M)} (ht : N.IsMinimalPrimaryDecomposition t) : (fun (J : Submodule R M) => (J.colon Set.univ).radical) '' ↑t = N.associatedPrimes

The first uniqueness theorem for primary decomposition, Theorem 4.5 in Atiyah-Macdonald: In any minimal primary decomposition I = ⨅ i, q_i, the ideals radical (q_i.colon M) are exactly the associated primes of I.

theorem Submodule.IsMinimalPrimaryDecomposition.mem_associatedPrimes {R : Type u_1} {M : Type u_2} [CommSemiring R] [AddCommMonoid M] [Module R M] {N : Submodule R M} {t : Finset (Submodule R M)} (ht : N.IsMinimalPrimaryDecomposition t) {q : Submodule R M} (hq : q ∈ t) : (q.colon Set.univ).radical ∈ N.associatedPrimes

theorem Submodule.IsMinimalPrimaryDecomposition.comap_localized₀_eq_ite {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommMonoid M] [Module R M] {N : Submodule R M} (s₀ : Finset ↑N.associatedPrimes) (hs₀ : IsLowerSet ↑s₀) (q : Submodule R M) (hqp : q.IsPrimary) (p : ↑N.associatedPrimes) (hq : (q.colon Set.univ).radical = ↑p) : comap (LocalizedModule.mkLinearMap (⨅ q ∈ s₀, (↑q).primeCompl) M) (localized₀ (⨅ q ∈ s₀, (↑q).primeCompl) (LocalizedModule.mkLinearMap (⨅ q ∈ s₀, (↑q).primeCompl) M) q) = if p ∈ s₀ then q else ⊤

theorem Submodule.IsMinimalPrimaryDecomposition.comap_localized₀_eq_iInf {R : Type u_3} {M : Type u_4} [CommRing R] [AddCommMonoid M] [Module R M] {N : Submodule R M} {t : Finset (Submodule R M)} (ht : N.IsMinimalPrimaryDecomposition t) (s₀ : Finset ↑N.associatedPrimes) (hs₀ : IsLowerSet ↑s₀) (s : Finset (Submodule R M)) (hs : s ⊆ t) (hs' : Finset.image (fun (q : Submodule R M) => (q.colon Set.univ).radical) s = Finset.image Subtype.val s₀) : comap (LocalizedModule.mkLinearMap (⨅ q ∈ s₀, (↑q).primeCompl) M) (localized₀ (⨅ q ∈ s₀, (↑q).primeCompl) (LocalizedModule.mkLinearMap (⨅ q ∈ s₀, (↑q).primeCompl) M) N) = ⨅ q ∈ s, q

The second uniqueness theorem for primary decomposition, Theorem 4.10 in Atiyah-Macdonald.

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

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.