Skip to content

[Merged by Bors] - feat(RingTheory): Ideal.span corollaries of Krull's height theorem #41401

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Closed
vlad902 wants to merge 2 commits into from
+26 −1
Closed

[Merged by Bors] - feat(RingTheory): Ideal.span corollaries of Krull's height theorem #41401

Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
4ee7bec
feat(RingTheory): `Ideal.span` corollaries of Krull's height theorem
vlad902 Jul 6, 2026
a53dcb7
minor golf
vlad902 Jul 7, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
27 changes: 26 additions & 1 deletion Mathlib/RingTheory/Ideal/KrullsHeightTheorem.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -242,12 +242,37 @@ lemma Ideal.height_le_card_of_mem_minimalPrimes_span_finset {p : Ideal R} {s : F
· exact Ideal.height_le_spanRank_toENat_of_mem_minimalPrimes _ _ hI
· simpa using Submodule.spanRank_span_le_card (s : Set R)

lemma Ideal.height_le_card_of_mem_minimalPrimes_span {p : Ideal R} {s : Set R}
lemma Ideal.height_span_le_card_of_span_ne_top {s : Finset R} (ht : Ideal.span (s : Set R) ≠ ⊤) :
(Ideal.span (s : Set R)).height ≤ s.card := by
obtain ⟨p, hp⟩ := Ideal.nonempty_minimalPrimes ht
grw [height_mono hp.1.2, height_le_card_of_mem_minimalPrimes_span_finset hp]

lemma Ideal.height_le_ncard_of_mem_minimalPrimes_span {p : Ideal R} {s : Set R}
(hs : s.Finite) (hI : p ∈ (Ideal.span s).minimalPrimes) :
p.height ≤ s.ncard := by
rw [s.ncard_eq_toFinset_card hs]
exact Ideal.height_le_card_of_mem_minimalPrimes_span_finset (by simpa)

@[deprecated (since := "2026-06-29")]
alias Ideal.height_le_card_of_mem_minimalPrimes_span :=
Ideal.height_le_ncard_of_mem_minimalPrimes_span

lemma Ideal.height_span_le_ncard_of_span_ne_top {s : Set R} (hs : s.Finite)
Comment thread
robin-carlier marked this conversation as resolved.
(ht : Ideal.span s ≠ ⊤) : (Ideal.span s).height ≤ s.ncard := by
obtain ⟨p, hp⟩ := Ideal.nonempty_minimalPrimes ht
grw [height_mono hp.1.2, height_le_ncard_of_mem_minimalPrimes_span hs hp]

lemma Ideal.height_le_encard_of_mem_minimalPrimes_span {p : Ideal R} {s : Set R}
(hI : p ∈ (Ideal.span s).minimalPrimes) : p.height ≤ s.encard := by
by_cases! hs : s.Finite
· exact hs.cast_ncard_eq ▸ Ideal.height_le_ncard_of_mem_minimalPrimes_span hs hI
· simp [hs]

lemma Ideal.height_span_le_encard_of_span_ne_top {s : Set R} (ht : Ideal.span s ≠ ⊤) :
(Ideal.span s).height ≤ s.encard := by
obtain ⟨p, hp⟩ := Ideal.nonempty_minimalPrimes ht
grw [height_mono hp.1.2, height_le_encard_of_mem_minimalPrimes_span hp]

/-- In a commutative Noetherian ring `R`, the height of a (finitely-generated) ideal is smaller
than or equal to the minimum number of generators for this ideal. -/
lemma Ideal.height_le_spanRank_toENat (I : Ideal R) (hI : I ≠ ⊤) :
Expand Down
Loading