feat(RingTheory): compute the height of the ideal spanning a (sub)set of variables in a polynomial ring

Author: vlad902

Mathlib.lean

@@ -6787,6 +6787,7 @@ public import Mathlib.RingTheory.MvPolynomial.EulerIdentity
 public import Mathlib.RingTheory.MvPolynomial.Expand
 public import Mathlib.RingTheory.MvPolynomial.FreeCommRing
 public import Mathlib.RingTheory.MvPolynomial.Groebner
+public import Mathlib.RingTheory.MvPolynomial.Height
 public import Mathlib.RingTheory.MvPolynomial.Homogeneous
 public import Mathlib.RingTheory.MvPolynomial.Ideal
 public import Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic

Mathlib/RingTheory/Ideal/Height.lean

@@ -353,6 +353,18 @@ lemma RingEquiv.height_comap {S : Type*} [CommRing S] (e : R ≃+* S) (I : Ideal
     simp only [EquivLike.coe_coe, RingEquiv.idealComapOrderIso_apply,
       ← Ideal.height_eq_primeHeight, RingEquiv.height_comap_of_isPrime]
 
+theorem RingHom.height_le_height_comap_of_surjective {S : Type*} [CommRing S] {f : R →+* S}
+    (hf : Function.Surjective f) (J : Ideal S) :
+    J.height ≤ (Ideal.comap f J).height := by
+  iterate 2 rw [height_eq_inf_minimalPrimes]
+  refine le_iInf₂_iff.mpr fun I hI ↦ ?_
+  obtain ⟨K, hK₁, hK₂⟩ := exists_minimalPrimes_comap_eq f I hI
+  have := f.strictMono_comap_of_surjective hf
+  have := Order.height_le_height_apply_of_strictMono _ this ⟨K, hK₁.1.1⟩
+  simp only [← PrimeSpectrum.height_eq_orderHeight, PrimeSpectrum.comap_asIdeal] at this
+  grw [← hK₂, ← this]
+  exact iInf₂_le K hK₁
+
 @[simp]
 lemma RingEquiv.height_map {S : Type*} [CommRing S] (e : R ≃+* S) (I : Ideal R) :
     (I.map e).height = I.height := by

Mathlib/RingTheory/MvPolynomial/Height.lean

@@ -0,0 +1,63 @@
+/-
+Copyright (c) 2026 Vlad Tsyrklevich. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Vlad Tsyrklevich
+-/
+module
+
+public import Mathlib.RingTheory.Ideal.KrullsHeightTheorem
+public import Mathlib.RingTheory.MvPolynomial.Ideal
+
+/-!
+# Height of polynomial ideals
+
+This file computes the height of the ideal generated by an arbitrary set of variables `(Xₛ, ...)`
+in the polynomial ring `R[X₁, ..., Xₙ]`.
+-/
+
+public section
+
+namespace MvPolynomial
+
+variable {σ R : Type*} [CommRing R]
+
+private theorem le_height_span_X_image_of_isDomain [IsDomain R] (s : Set σ) :
+    s.encard ≤ (Ideal.span (X (R := R) '' s)).height := by
+  refine ENat.forall_natCast_le_iff_le.mp fun n hn ↦ ?_
+  induction n generalizing s with
+  | zero => simp
+  | succ n ih =>
+    by_cases! he : IsEmpty s
+    · simp_all
+    obtain ⟨x, hx⟩ := he
+    have := ih (s \ {x}) (by grw [← Set.encard_tsub_one_le_encard_sdiff_singleton, ← hn]; norm_cast)
+    push_cast
+    grw [this]
+    have := span_X_image_isPrime (R := R) (σ := σ)
+    refine Ideal.height_add_one_le_of_lt_of_isPrime <| lt_iff_le_and_ne'.mpr ⟨?_, ?_⟩
+    · exact Ideal.span_mono (by grind)
+    · exact ne_of_mem_of_not_mem' (a := X x) (by simp [hx]) (by simp)
+
+theorem le_height_span_X_image (s : Set σ) :
+    s.encard ≤ (Ideal.span (X (R := R) '' s)).height := by
+  rw [Ideal.height_eq_inf_minimalPrimes]
+  refine le_iInf₂ fun I hI ↦ ?_
+  let π := MvPolynomial.map (σ := σ) (Ideal.Quotient.mk (Ideal.comap C I))
+  have h₁ : (Ideal.map π I).height ≤ I.height := by
+    have : Function.Surjective π := MvPolynomial.map_surjective _ Ideal.Quotient.mk_surjective
+    grw [RingHom.height_le_height_comap_of_surjective this, Ideal.comap_map_of_surjective _ this]
+    simp [π, ← RingHom.ker_eq_comap_bot, ker_map, Ideal.map_comap_le]
+  have h₂ : Ideal.span (X '' s) ≤ Ideal.map π I := by
+    grw [← Ideal.map_mono hI.1.2, Ideal.map_span, Ideal.span_mono]
+    rintro x ⟨y, hy₁, hy₂⟩
+    simpa using ⟨y, hy₁, hy₂ ▸ map_X _ y⟩
+  have := hI.1.1
+  grw [← h₁, ← Ideal.height_mono h₂, ← le_height_span_X_image_of_isDomain]
+
+theorem height_span_X_image_eq [Nontrivial R] [IsNoetherianRing R] [Finite σ] (s : Set σ) :
+    (Ideal.span (X (R := R) '' s)).height = s.encard := by
+  refine le_antisymm ?_ (le_height_span_X_image ..)
+  grw [Ideal.height_span_le_encard_of_span_ne_top, Set.encard_image_le]
+  exact (Ideal.ne_top_iff_one _).mpr (by simp [mem_ideal_span_X_image])
+
+end MvPolynomial

Mathlib/RingTheory/MvPolynomial/Ideal.lean

@@ -59,6 +59,13 @@ theorem mem_ideal_span_X_image {x : MvPolynomial σ R} {s : Set σ} :
   refine this.trans ?_
   simp [Nat.one_le_iff_ne_zero]
 
+@[simp]
+theorem X_mem_ideal_span_X_image_iff [Nontrivial R] {x : σ} {s : Set σ} :
+    X x ∈ Ideal.span (X '' s : Set (MvPolynomial σ R)) ↔ x ∈ s := by
+  refine ⟨fun h ↦ ?_, fun _ ↦ Submodule.mem_span_of_mem (by grind)⟩
+  have := mem_ideal_span_X_image.mp h (Finsupp.single x 1)
+  grind [coeff_X_same, one_ne_zero, Finsupp.single_apply_eq_zero]
+
 section idealOfVars
 
 open Finset Finsupp