Theorems · Theorem · commutative algebra

Submodule.exists_minimal_isPrimary_decomposition_of_isPrimary_decomposition

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

Defined in

Mathlib.RingTheory.Lasker

Cited by

2 results in Mathlib

Foundations

Depth 85 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringAddCommMonoidModule