Pure ideals

An ideal I of a ring R is called pure if R ⧸ I is flat over R (see Stacks 04PR). In this file we show some properties of such ideals.

Main results and definitions

• Ideal.Pure: An ideal I of R is pure if R ⧸ I is R-flat.
• Ideal.inf_eq_mul_of_pure: If I is pure, I ⊓ J = I * J for every ideal J.
• Ideal.Pure.of_inf_eq_mul: If for any f.g. ideal J, the equality I ⊓ J = I * J holds, then I is pure.
• Ideal.zeroLocus_inj_of_pure: If I and J are pure ideals such that V(I) = V(J), then I = J.

@[reducible, inline]

abbrev Ideal.Pure {R : Type u_1} [CommRing R] (I : Ideal R) : Prop

An ideal I of R is pure if R ⧸ I is a flat R-module.

Equations

• I.Pure = Module.Flat R (R ⧸ I)

theorem injective_lTensor_quotient_iff_inf_eq_mul {R : Type u_1} [CommRing R] (I J : Ideal R) : Function.Injective ⇑(LinearMap.lTensor (R ⧸ I) (Submodule.subtype J)) ↔ I ⊓ J = I * J

theorem Ideal.inf_eq_mul_of_pure {R : Type u_1} [CommRing R] (I J : Ideal R) [I.Pure] : I ⊓ J = I * J

Stacks Tag 04PS ((1) => (2))

theorem Ideal.isIdempotentElem_of_pure {R : Type u_1} [CommRing R] (I : Ideal R) [I.Pure] : IsIdempotentElem I

If I is pure, I ^ 2 = I. The converse holds if I is finitely generated, see Ideal.Pure.of_isIdempotentElem.

theorem Ideal.Pure.of_isIdempotentElem {R : Type u_1} [CommRing R] {I : Ideal R} (h : I.FG) (h' : IsIdempotentElem I) : I.Pure

theorem Ideal.Pure.of_inf_eq_mul {R : Type u_1} [CommRing R] (I : Ideal R) (H : ∀ ⦃J : Ideal R⦄, J.FG → I ⊓ J = I * J) : I.Pure

Stacks Tag 04PS ((3) => (1))

theorem Ideal.exists_eq_mul_of_pure {R : Type u_1} [CommRing R] {I : Ideal R} [I.Pure] {x : R} (hx : x ∈ I) : ∃ y ∈ I, x = x * y

Stacks Tag 04PS ((1) => (5))

theorem Ideal.le_ker_atPrime_of_forall_exists_eq_mul {R : Type u_1} [CommRing R] {I : Ideal R} (h : ∀ x ∈ I, ∃ y ∈ I, x = x * y) {p : Ideal R} [p.IsPrime] (hle : I ≤ p) : I ≤ RingHom.ker (algebraMap R (Localization.AtPrime p))

Stacks Tag 04PS ((5) => (7))

theorem Ideal.ker_piRingHom_atPrime_eq_of_pure {R : Type u_1} [CommRing R] (I : Ideal R) [I.Pure] : RingHom.ker (RingHom.pi fun (p : ↑(PrimeSpectrum.zeroLocus ↑I)) => algebraMap R (Localization.AtPrime (↑p).asIdeal)) = I

theorem Ideal.zeroLocus_inj_of_pure {R : Type u_1} [CommRing R] {I J : Ideal R} [I.Pure] [J.Pure] : PrimeSpectrum.zeroLocus ↑I = PrimeSpectrum.zeroLocus ↑J ↔ I = J

Stacks Tag 04PT