Commit 2026-01-22 07:06 29beeca0

View on Github →

feat(RingTheory/KrullDimension): generalize some results about local rings (#27557) We generalize ringKrullDim_le_ringKrullDim_add_card to non-local rings by assuming s ⊆ Ring.jacobson R instead of s ⊆ maximalIdeal R. For this we show that if R is a Noetherian ring and I is an ideal contained in a prime ideal p, then the height of p is bounded by the sum of the height of the image of p in R / I and the span rank of I.

Estimated changes

Modified Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean

added theorem Ideal.height_le_height_add_encard_of_subset

added theorem Ideal.height_le_height_add_one_of_mem

added theorem Ideal.height_le_height_add_spanFinrank_of_le

added theorem Ideal.height_le_ringKrullDim_quotient_add_encard

added theorem Ideal.height_le_ringKrullDim_quotient_add_one

added theorem height_le_ringKrullDim_quotient_add_spanFinrank

added theorem ringKrullDim_le_ringKrullDim_quotient_add_card

added theorem ringKrullDim_le_ringKrullDim_quotient_add_encard

added theorem ringKrullDim_le_ringKrullDim_quotient_add_spanFinrank

Modified Mathlib/RingTheory/Ideal/MinimalPrime/Basic.lean

added theorem Ideal.mem_minimalPrimes_sup

Modified Mathlib/RingTheory/Jacobson/Radical.lean

added theorem Ring.jacobson_le_of_isMaximal

Modified Mathlib/RingTheory/KrullDimension/Regular.lean

added theorem Module.ringKrullDim_quotient_add_one_of_mem_nonZeroDivisors

modified theorem ringKrullDim_le_ringKrullDim_add_spanFinrank