Primary ideals

A proper ideal I is primary iff xy ∈ I implies x ∈ I or y ∈ radical I.

Main definitions

• Ideal.IsPrimary

Implementation details

Uses a specialized phrasing of Submodule.IsPrimary to have better API-piercing usage.

@[reducible, inline]

abbrev Ideal.IsPrimary {R : Type u_1} [CommSemiring R] (I : Ideal R) : Prop

A proper ideal I is primary as a submodule.

Equations

• I.IsPrimary = Submodule.IsPrimary I

theorem Ideal.isPrimary_iff {R : Type u_1} [CommSemiring R] {I : Ideal R} : I.IsPrimary ↔ I ≠ ⊤ ∧ ∀ {x y : R}, x * y ∈ I → x ∈ I ∨ y ∈ I.radical

A proper ideal I is primary iff xy ∈ I implies x ∈ I or y ∈ radical I.

theorem Ideal.IsPrime.isPrimary {R : Type u_1} [CommSemiring R] {I : Ideal R} (hi : I.IsPrime) : I.IsPrimary

theorem Ideal.isPrime_radical {R : Type u_1} [CommSemiring R] {I : Ideal R} (hi : I.IsPrimary) : I.radical.IsPrime

theorem Ideal.isPrimary_of_isMaximal_radical {R : Type u_1} [CommSemiring R] {I : Ideal R} (hi : I.radical.IsMaximal) : I.IsPrimary

theorem Ideal.IsPrimary.inf {R : Type u_1} [CommSemiring R] {I J : Ideal R} (hi : I.IsPrimary) (hj : J.IsPrimary) (hij : I.radical = J.radical) : (I ⊓ J).IsPrimary

@[deprecated Ideal.IsPrimary.inf (since := "2025-01-19")]

theorem Ideal.isPrimary_inf {R : Type u_1} [CommSemiring R] {I J : Ideal R} (hi : I.IsPrimary) (hj : J.IsPrimary) (hij : I.radical = J.radical) : (I ⊓ J).IsPrimary

Alias of Ideal.IsPrimary.inf.

theorem Ideal.isPrimary_finsetInf {R : Type u_1} [CommSemiring R] {ι : Type u_3} {s : Finset ι} {f : ι → Ideal R} {i : ι} (hi : i ∈ s) (hs : ∀ ⦃y : ι⦄, y ∈ s → (f y).IsPrimary) (hs' : ∀ ⦃y : ι⦄, y ∈ s → (f y).radical = (f i).radical) : (s.inf f).IsPrimary

@[deprecated Ideal.isPrimary_finsetInf (since := "2026-01-19")]

theorem Ideal.isPrimary_finset_inf {R : Type u_1} [CommSemiring R] {ι : Type u_3} {s : Finset ι} {f : ι → Ideal R} {i : ι} (hi : i ∈ s) (hs : ∀ ⦃y : ι⦄, y ∈ s → (f y).IsPrimary) (hs' : ∀ ⦃y : ι⦄, y ∈ s → (f y).radical = (f i).radical) : (s.inf f).IsPrimary

Alias of Ideal.isPrimary_finsetInf.

theorem Ideal.IsPrimary.comap {R : Type u_1} {S : Type u_2} [CommSemiring R] [CommSemiring S] {I : Ideal S} (hI : I.IsPrimary) (φ : R →+* S) : (Ideal.comap φ I).IsPrimary