KrullsHeightTheorem.lean

/-
Copyright (c) 2025 Andrew Yang. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Wanyi He, Jiedong Jiang, Christian Merten, Jingting Wang, Andrew Yang, Shouxin Zhang
-/
module

public import Mathlib.RingTheory.HopkinsLevitzki
public import Mathlib.RingTheory.Ideal.GoingDown
public import Mathlib.RingTheory.Ideal.Height
public import Mathlib.RingTheory.Localization.Submodule
public import Mathlib.RingTheory.Nakayama
public import Mathlib.RingTheory.Ideal.Quotient.Noetherian

/-!
# Krull's Height Theorem

In this file, we prove **Krull's principal ideal theorem** (also known as
**Krullscher Hauptidealsatz**), and **Krull's height theorem** (also known as
**Krullscher Höhensatz**).

## Main Results

* `Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes` : This theorem is the
  **Krull's principal ideal theorem** (also known as **Krullscher Hauptidealsatz**), which states
  that: In a commutative Noetherian ring `R`, any prime ideal that is minimal over a principal ideal
  has height at most 1.

* `Ideal.height_le_spanRank_toENat_of_mem_minimal_primes` : This theorem is the
  **Krull's height theorem** (also known as **Krullscher Höhensatz**), which states that:
  In a commutative Noetherian ring `R`, any prime ideal that is minimal over an ideal generated by
  `n` elements has height at most `n`.

* `Ideal.height_le_spanRank_toENat` : This theorem is a corollary of the **Krull's height theorem**
  (also known as **Krullscher Höhensatz**). 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.

* `Ideal.height_le_iff_exists_minimal_primes` : In a commutative Noetherian ring `R`, a prime ideal
  `p` has height no greater than `n` if and only if it is a minimal ideal over some ideal generated
  by no more than `n` elements.
-/

@[expose] public section

variable {R : Type*} [CommRing R] [IsNoetherianRing R]

lemma IsLocalRing.quotient_artinian_of_mem_minimalPrimes_of_isLocalRing
    [IsLocalRing R] (I : Ideal R) (hp : IsLocalRing.maximalIdeal R ∈ I.minimalPrimes) :
    IsArtinianRing (R ⧸ I) :=
  have : Ring.KrullDimLE 0 (R ⧸ I) := Ring.krullDimLE_zero_iff.mpr fun J prime ↦
    Ideal.isMaximal_of_isIntegral_of_isMaximal_comap _ <| by
      convert IsLocalRing.maximalIdeal.isMaximal R
      rw [Ideal.minimalPrimes, Set.mem_setOf] at hp
      have := prime.comap (Ideal.Quotient.mk I)
      exact hp.eq_of_le ⟨this, .trans (by simp) (Ideal.ker_le_comap _)⟩ (le_maximalIdeal this.1)
  IsNoetherianRing.isArtinianRing_of_krullDimLE_zero

lemma Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes_of_isLocalRing
    [IsLocalRing R] (I : Ideal R) [I.IsPrincipal]
    (hp : (IsLocalRing.maximalIdeal R) ∈ I.minimalPrimes) :
    (IsLocalRing.maximalIdeal R).height ≤ 1 := by
  refine Ideal.height_le_iff.mpr fun q h₁ h₂ ↦ ?_
  suffices q.height = 0 by rw [this]; exact zero_lt_one
  rw [← WithBot.coe_inj,
    ← IsLocalization.AtPrime.ringKrullDim_eq_height q (Localization.AtPrime q),
    WithBot.coe_zero, ← ringKrullDimZero_iff_ringKrullDim_eq_zero,
    ← isArtinianRing_iff_krullDimLE_zero, isArtinianRing_iff_isNilpotent_maximalIdeal,
    ← Localization.AtPrime.map_eq_maximalIdeal]
  have : IsArtinianRing (R ⧸ I) :=
    IsLocalRing.quotient_artinian_of_mem_minimalPrimes_of_isLocalRing I hp
  let f := algebraMap R (Localization.AtPrime q)
  let qs : ℕ →o (Ideal (R ⧸ I))ᵒᵈ :=
    { toFun n := ((q.map f ^ n).comap f).map (Ideal.Quotient.mk I)
      monotone' i j e := Ideal.map_mono (Ideal.comap_mono (Ideal.pow_le_pow_right e)) }
  obtain ⟨n, hn⟩ := IsArtinian.monotone_stabilizes qs
  refine ⟨n, ?_⟩
  apply Submodule.eq_bot_of_le_smul_of_le_jacobson_bot (q.map f) _ (IsNoetherian.noetherian _)
  rotate_left
  · rw [IsLocalRing.jacobson_eq_maximalIdeal, Localization.AtPrime.map_eq_maximalIdeal]
    exact bot_ne_top
  rw [smul_eq_mul, ← pow_succ',
    ← (IsLocalization.orderEmbedding q.primeCompl (Localization.AtPrime q)).map_rel_iff]
  refine Submodule.le_of_le_smul_of_le_jacobson_bot (I := I) (IsNoetherian.noetherian _) ?_ ?_
  · rw [IsLocalRing.jacobson_eq_maximalIdeal]
    exacts [Ideal.le_minimalPrimes hp, bot_ne_top]
  · replace hn := congr(Ideal.comap (Ideal.Quotient.mk I) $(hn _ n.le_succ))
    simp only [qs, OrderHom.coe_mk, ← RingHom.ker_eq_comap_bot, Ideal.mk_ker,
      Ideal.comap_map_of_surjective _ Ideal.Quotient.mk_surjective] at hn
    intro x hx
    obtain ⟨y, hy, z, hz, rfl⟩ := Submodule.mem_sup.mp (hn.le (Ideal.mem_sup_left hx))
    refine Submodule.add_mem_sup hy ?_
    obtain ⟨z, rfl⟩ := (Submodule.IsPrincipal.mem_iff_eq_smul_generator I).mp hz
    rw [smul_eq_mul, smul_eq_mul, mul_comm]
    refine Ideal.mul_mem_mul ?_ (Submodule.IsPrincipal.generator_mem _)
    dsimp [IsLocalization.orderEmbedding] at hx
    rwa [Ideal.mem_comap, f.map_add, f.map_mul, Ideal.add_mem_iff_right _
      (Ideal.pow_le_pow_right n.le_succ hy), mul_comm, Ideal.unit_mul_mem_iff_mem] at hx
    refine IsLocalization.map_units (M := q.primeCompl) _ ⟨_, ?_⟩
    change Submodule.IsPrincipal.generator I ∉ (↑q : Set R)
    rw [← Set.singleton_subset_iff, ← Ideal.span_le, Ideal.span_singleton_generator]
    exact fun e ↦ h₂.not_ge (hp.2 ⟨h₁, e⟩ h₂.le)

/-- **Krull's principal ideal theorem** (also known as **Krullscher Hauptidealsatz**) :
  In a commutative Noetherian ring `R`, any prime ideal that is minimal over a principal ideal
  has height at most 1. -/
lemma Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes
    (I : Ideal R) [I.IsPrincipal] (p : Ideal R) (hp : p ∈ I.minimalPrimes) : p.height ≤ 1 := by
  have := Ideal.minimalPrimes_isPrime hp
  let f := algebraMap R (Localization.AtPrime p)
  have := Ideal.height_le_one_of_isPrincipal_of_mem_minimalPrimes_of_isLocalRing (I.map f) ?_
  · rwa [← IsLocalization.height_comap p.primeCompl,
      Localization.AtPrime.comap_maximalIdeal] at this
  · rwa [IsLocalization.minimalPrimes_map p.primeCompl (Localization.AtPrime p) I,
      Set.mem_preimage, Localization.AtPrime.comap_maximalIdeal]

theorem Ideal.map_height_le_one_of_mem_minimalPrimes {I p : Ideal R} {x : R}
    (hp : p ∈ (I ⊔ span {x}).minimalPrimes) : (p.map (Ideal.Quotient.mk I)).height ≤ 1 :=
  let f := Ideal.Quotient.mk I
  have : p.IsPrime := Ideal.minimalPrimes_isPrime hp
  have hfp : RingHom.ker f ≤ p := I.mk_ker.trans_le (le_sup_left.trans (Ideal.le_minimalPrimes hp))
  height_le_one_of_isPrincipal_of_mem_minimalPrimes ((span {x}).map f) (p.map f)
    ⟨⟨map_isPrime_of_surjective Quotient.mk_surjective hfp,
      map_mono (le_sup_right.trans (Ideal.le_minimalPrimes hp))⟩,
        fun _ ⟨hr, hxr⟩ hrp ↦ map_le_iff_le_comap.mpr <| hp.2 ⟨hr.comap f, sup_le_iff.mpr
          ⟨I.mk_ker.symm.trans_le <| ker_le_comap (Ideal.Quotient.mk I), le_comap_of_map_le hxr⟩⟩ <|
            (comap_mono hrp).trans <| Eq.le <|
              (p.comap_map_of_surjective _ Quotient.mk_surjective).trans <| sup_eq_left.mpr hfp⟩

/-- If `q < p` are prime ideals such that `p` is minimal over `span (s ∪ {x})` and
`t` is a set contained in `q` such that `s ⊆ √span (t ∪ {x})`, then `q` is minimal over `span t`.
This is used in the induction step for the proof of Krull's height theorem. -/
theorem Ideal.mem_minimalPrimes_span_of_mem_minimalPrimes_span_insert {q p : Ideal R} [q.IsPrime]
    (hqp : q < p) (x : R) (s : Set R) (hp : p ∈ (span (insert x s)).minimalPrimes)
    (t : Set R) (htq : t ⊆ q) (hsp : s ⊆ (span (insert x t)).radical) :
    q ∈ (span t).minimalPrimes := by
  let f := Quotient.mk (span t)
  have hf : Function.Surjective f := Quotient.mk_surjective
  have hI'q : span t ≤ q := span_le.mpr htq
  have hI'p : span t ≤ p := hI'q.trans hqp.le
  have := minimalPrimes_isPrime hp
  have : (p.map f).IsPrime := map_isPrime_of_surjective hf (by rwa [mk_ker])
  suffices h : (p.map f).height ≤ 1 by
    have h_lt : q.map f < p.map f := (map_mono hqp.le).lt_of_not_ge fun e ↦ hqp.not_ge <| by
      simpa only [comap_map_of_surjective f hf, ← RingHom.ker_eq_comap_bot, f, mk_ker,
        sup_eq_left.mpr hI'q, sup_eq_left.mpr hI'p] using comap_mono (f := f) e
    have : (q.map f).IsPrime := map_isPrime_of_surjective hf (by rwa [mk_ker])
    have : (p.map f).FiniteHeight := ⟨Or.inr (h.trans_lt (WithTop.coe_lt_top 1)).ne⟩
    rw [height_eq_primeHeight] at h
    have := (primeHeight_strict_mono h_lt).trans_le h
    rw [ENat.lt_one_iff_eq_zero, primeHeight_eq_zero_iff] at this
    have := minimal_primes_comap_of_surjective hf this
    rwa [comap_map_of_surjective f hf, ← RingHom.ker_eq_comap_bot,
      mk_ker, sup_eq_left.mpr hI'q] at this
  refine height_le_one_of_isPrincipal_of_mem_minimalPrimes ((span {x}).map f) (p.map f) ⟨⟨this,
    map_mono <| span_le.mpr <| Set.singleton_subset_iff.mpr <| (Ideal.le_minimalPrimes hp) <|
      subset_span <| .inl rfl⟩,
    fun r ⟨hr, hxr⟩ hrp ↦ map_le_iff_le_comap.mpr (hp.2 ⟨hr.comap f, ?_⟩ ?_)⟩
  · rw [span_le, Set.insert_subset_iff]
    have := map_le_iff_le_comap.mp hxr (subset_span rfl)
    refine ⟨this, hsp.trans ((hr.comap f).isRadical.radical_le_iff.mpr ?_)⟩
    rw [span_le, Set.insert_subset_iff]
    exact ⟨this, span_le.mp (mk_ker.symm.trans_le (ker_le_comap _))⟩
  · conv_rhs => rw [← sup_eq_left.mpr hI'p, ← (span t).mk_ker, RingHom.ker_eq_comap_bot,
      ← comap_map_of_surjective f hf p]
    exact comap_mono hrp

open IsLocalRing in
/-- **Krull's height theorem** (also known as **Krullscher Höhensatz**) :
  In a commutative Noetherian ring `R`, any prime ideal that is minimal over an ideal generated
  by `n` elements has height at most `n`. -/
nonrec lemma Ideal.height_le_spanRank_toENat_of_mem_minimal_primes
    (I : Ideal R) (p : Ideal R) (hp : p ∈ I.minimalPrimes) :
    p.height ≤ I.spanRank.toENat := by
  classical
  rw [I.spanRank_toENat_eq_iInf_finset_card, le_iInf_iff]
  rintro ⟨s, (rfl : span s = I)⟩
  induction hn : s.card using Nat.strong_induction_on generalizing R with
  | h n H =>
    replace hn : s.card ≤ n := hn.le
    have := Ideal.minimalPrimes_isPrime hp
    cases n with
    | zero =>
      rw [ENat.coe_zero, nonpos_iff_eq_zero, height_eq_primeHeight p,
        primeHeight_eq_zero_iff, minimalPrimes]
      simp_all
    | succ n =>
      wlog hR : ∃ (_ : IsLocalRing R), p = maximalIdeal R
      · rw [← Localization.AtPrime.comap_maximalIdeal (I := p)] at hp ⊢
        rw [IsLocalization.height_comap p.primeCompl]
        rw [← Set.mem_preimage, ← IsLocalization.minimalPrimes_map p.primeCompl, map_span] at hp
        exact this _ (s.image (algebraMap R (Localization p.primeCompl))) (by simpa using hp)
          inferInstance _ H (Finset.card_image_le.trans hn) ⟨inferInstance, rfl⟩
      obtain ⟨_, rfl⟩ := hR
      simp_rw [height_le_iff_covBy, ENat.coe_add, ENat.coe_one, ENat.lt_coe_add_one_iff]
      intro q hq hpq hq'
      obtain ⟨x, s', hxs', rfl, hxq⟩ : ∃ x s', x ∉ s' ∧ s = insert x s' ∧ x ∉ q := by
        have : ¬(s : Set R) ⊆ q := by
          rw [← span_le]
          exact fun e ↦ lt_irrefl _ ((hp.2 ⟨hq, e⟩ hpq.le).trans_lt hpq)
        obtain ⟨x, hxt, hxq⟩ := Set.not_subset.mp this
        exact ⟨x, _, fun e ↦ (Finset.mem_erase.mp e).1 rfl, (Finset.insert_erase hxt).symm, hxq⟩
      have : maximalIdeal R ≤ (q ⊔ span {x}).radical := by
        rw [radical_eq_sInf, le_sInf_iff]
        exact fun J ⟨hJ, hJ'⟩ ↦ by_contra fun h ↦ hq' J hJ' ((SetLike.lt_iff_le_and_exists.mpr
          ⟨le_sup_left, x, mem_sup_right (mem_span_singleton_self _), hxq⟩).trans_le hJ)
          ((le_maximalIdeal hJ'.ne_top).lt_of_not_ge h)
      have h : (s' : Set R) ⊆ (q ⊔ span {x}).radical := by
        have := (Ideal.le_minimalPrimes hp).trans this
        rw [span_le, Finset.coe_insert, Set.insert_subset_iff] at this
        exact this.2
      obtain ⟨t, ht, hspan⟩ := exists_subset_radical_span_sup_of_subset_radical_sup _ _ _ h
      let t := Finset.univ.image t
      suffices hq : q ∈ (span t).minimalPrimes from
        have tcard : t.card ≤ n := Nat.le_of_lt_succ ((Finset.card_image_le.trans_lt <| by
          simpa using Finset.card_lt_card (Finset.ssubset_insert hxs')).trans_le hn)
        (H _ (tcard.trans_lt n.lt_succ_self) q t hq rfl).trans (by norm_cast)
      rw [Finset.coe_insert] at hp
      convert mem_minimalPrimes_span_of_mem_minimalPrimes_span_insert hpq _ _ hp _ ht ?_
      · simp [t]
      refine hspan.trans <| radical_mono ?_
      rw [← Set.union_singleton, span_union]

lemma Ideal.height_le_card_of_mem_minimalPrimes_span_finset {p : Ideal R} {s : Finset R}
    (hI : p ∈ (Ideal.span s).minimalPrimes) :
    p.height ≤ s.card := by
  trans (Cardinal.toENat (Submodule.spanRank (Ideal.span (s : Set R))))
  · exact Ideal.height_le_spanRank_toENat_of_mem_minimal_primes _ _ 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}
    (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)

/-- 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 ≠ ⊤) :
    I.height ≤ I.spanRank.toENat := by
  obtain ⟨J, hJ⟩ := nonempty_minimalPrimes hI
  refine (iInf₂_le J hJ).trans ?_
  convert (I.height_le_spanRank_toENat_of_mem_minimal_primes J hJ)
  exact (@height_eq_primeHeight _ _ J (Ideal.minimalPrimes_isPrime hJ)).symm

lemma Ideal.height_le_spanFinrank (I : Ideal R) (hI : I ≠ ⊤) :
    I.height ≤ I.spanFinrank := by
  have : I.spanFinrank = I.spanRank.toENat := by
    rw [Submodule.fg_iff_spanRank_eq_spanFinrank.mpr (IsNoetherian.noetherian I), map_natCast]
  exact this ▸ height_le_spanRank_toENat I hI

lemma Ideal.height_le_spanRank (I : Ideal R) (hI : I ≠ ⊤) :
    I.height ≤ I.spanRank := by
  trans ↑I.spanRank.toENat
  · exact_mod_cast I.height_le_spanRank_toENat hI
  · exact I.spanRank.ofENat_toENat_le

instance Ideal.finiteHeight_of_isNoetherianRing (I : Ideal R) :
    I.FiniteHeight := finiteHeight_iff_lt.mpr <| Or.elim (em (I = ⊤)) Or.inl
  fun h ↦ Or.inr <| (I.height_le_spanFinrank h).trans_lt (ENat.coe_lt_top _)

instance [IsNoetherianRing R] [IsLocalRing R] : FiniteRingKrullDim R := by
  apply finiteRingKrullDim_iff_ne_bot_and_top.mpr
  rw [← IsLocalRing.maximalIdeal_height_eq_ringKrullDim]
  constructor
  · exact WithBot.coe_ne_bot
  · rw [← WithBot.coe_top, ne_eq, WithBot.coe_inj]
    exact ((IsLocalRing.maximalIdeal R).finiteHeight_iff.mp
      (IsLocalRing.maximalIdeal R).finiteHeight_of_isNoetherianRing).resolve_left
        Ideal.IsPrime.ne_top'

lemma Ideal.exists_spanRank_eq_and_height_eq (I : Ideal R) (hI : I ≠ ⊤) :
    ∃ J ≤ I, J.spanRank = I.height ∧ J.height = I.height := by
  obtain ⟨J, hJ₁, hJ₂, hJ₃⟩ := exists_spanRank_le_and_le_height_of_le_height I _
    (ENat.coe_toNat_le_self I.height)
  rw [ENat.coe_toNat_eq_self.mpr (Ideal.height_ne_top hI)] at hJ₃
  refine ⟨J, hJ₁, le_antisymm ?_ (le_trans ?_ (J.height_le_spanRank ?_)),
    le_antisymm (Ideal.height_mono hJ₁) hJ₃⟩
  · convert hJ₂
    exact Cardinal.ofENat_eq_nat.mpr (ENat.coe_toNat (I.height_ne_top hI)).symm
  · exact Cardinal.ofENat_le_ofENat_of_le hJ₃
  · rintro rfl
    exact hI (top_le_iff.mp hJ₁)

/-- In a commutative Noetherian ring `R`, a prime ideal `p` has height no greater than `n` if and
only if it is a minimal ideal over some ideal generated by no more than `n` elements. -/
lemma Ideal.height_le_iff_exists_minimalPrimes (p : Ideal R) [p.IsPrime]
    (n : ℕ∞) : p.height ≤ n ↔ ∃ I : Ideal R, p ∈ I.minimalPrimes ∧ I.spanRank ≤ n := by
  constructor
  · intro h
    obtain ⟨I, hI, e₁, e₂⟩ := exists_spanRank_eq_and_height_eq p (IsPrime.ne_top ‹_›)
    refine ⟨I, Ideal.mem_minimalPrimes_of_height_eq hI e₂.ge, e₁.symm ▸ ?_⟩
    norm_cast
  · rintro ⟨I, hp, hI⟩
    exact le_trans
      (Ideal.height_le_spanRank_toENat_of_mem_minimal_primes I p hp)
      (by simpa using (Cardinal.toENat.monotone' hI))

/-- If `p` is a prime in a Noetherian ring `R`, there exists a `p`-primary ideal `I`
spanned by `p.height` elements. -/
lemma Ideal.exists_finset_card_eq_height_of_isNoetherianRing (p : Ideal R) [p.IsPrime] :
    ∃ s : Finset R, p ∈ (span s).minimalPrimes ∧ s.card = p.height := by
  obtain ⟨I, hI, hr⟩ := (p.height_le_iff_exists_minimalPrimes <| p.height).mp le_rfl
  have hs : I.generators.Finite := (IsNoetherian.noetherian I).finite_generators
  refine ⟨hs.toFinset, by rwa [hs.coe_toFinset, span, I.span_generators], ?_⟩
  rw [← Set.ncard_eq_toFinset_card (hs := hs), (IsNoetherian.noetherian I).generators_ncard]
  refine le_antisymm ?_ ?_
  · rw [Submodule.fg_iff_spanRank_eq_spanFinrank.mpr (IsNoetherian.noetherian I)] at hr
    exact Cardinal.nat_le_ofENat.mp hr
  · convert_to p.height ≤ I.spanRank.toENat
    · symm
      simpa [Submodule.fg_iff_spanRank_eq_spanFinrank] using (IsNoetherian.noetherian I)
    · exact I.height_le_spanRank_toENat_of_mem_minimal_primes _ hI

/-- If `I ≤ p` and `p` is prime, the height of `p` is bounded by the height of `p ⧸ I R` plus
the span rank of `I`. -/
lemma Ideal.height_le_height_add_spanFinrank_of_le {I p : Ideal R} [p.IsPrime] (hrp : I ≤ p) :
    p.height ≤ (p.map (Quotient.mk I)).height + I.spanFinrank := by
  classical
  let p' := p.map (algebraMap R (R ⧸ I))
  have : p'.IsPrime := isPrime_map_quotientMk_of_isPrime hrp
  obtain ⟨s, hps, hs⟩ := exists_finset_card_eq_height_of_isNoetherianRing p'
  have hsp' : (s : Set (R ⧸ I)) ⊆ (p' : Set _) :=
    fun _ hx ↦ (Ideal.le_minimalPrimes hps) (subset_span hx)
  have : Set.SurjOn (Ideal.Quotient.mk I) p s := by
    refine Set.SurjOn.mono subset_rfl hsp' fun x hx ↦ ?_
    obtain ⟨x, rfl⟩ := Ideal.Quotient.mk_surjective x
    exact ⟨x, by simpa [hrp, sup_of_le_left, p'] using hx⟩
  obtain ⟨o, hsubset, ho, himgo⟩ := s.exists_subset_injOn_image_eq_of_surjOn (p : Set R) this
  have hI : I.FG := IsNoetherian.noetherian I
  let t : Finset R := o ∪ (Submodule.FG.finite_generators hI).toFinset
  suffices h : p.height ≤ t.card by
    refine le_trans h (hs ▸ ?_)
    norm_cast
    have : (Submodule.FG.finite_generators hI).toFinset.card = I.spanFinrank := by
      rw [← Set.ncard_eq_toFinset_card (hs := Submodule.FG.finite_generators hI)]
      exact Submodule.FG.generators_ncard hI
    grind
  refine Ideal.height_le_card_of_mem_minimalPrimes_span_finset ?_
  rw [Finset.coe_union, Set.Finite.coe_toFinset, span_union, sup_comm, span,
    Submodule.span_generators]
  refine Ideal.mem_minimalPrimes_sup hrp ?_
  convert hps
  simp [Ideal.map_span, ← himgo]

lemma height_le_ringKrullDim_quotient_add_spanFinrank {p I : Ideal R} [p.IsPrime] (h : I ≤ p) :
    p.height ≤ ringKrullDim (R ⧸ I) + I.spanFinrank := by
  trans (p.map (Ideal.Quotient.mk I)).height + I.spanFinrank
  · norm_cast; exact Ideal.height_le_height_add_spanFinrank_of_le h
  · gcongr
    have : (Ideal.map (Ideal.Quotient.mk I) p).IsPrime :=
      Ideal.isPrime_map_quotientMk_of_isPrime h
    exact Ideal.height_le_ringKrullDim_of_ne_top Ideal.IsPrime.ne_top'

lemma ringKrullDim_le_ringKrullDim_quotient_add_spanFinrank (I : Ideal R)
    (h : I ≤ Ring.jacobson R) :
    ringKrullDim R ≤ ringKrullDim (R ⧸ I) + I.spanFinrank := by
  nontriviality R
  rw [ringKrullDim_le_iff_isMaximal_height_le]
  intro m hm
  exact height_le_ringKrullDim_quotient_add_spanFinrank <|
    le_trans h <| Ring.jacobson_le_of_isMaximal m

/-- If `p` is a prime ideal containing `s`, the height of `p` is bounded
by the sum of the height of the image of `p` in `R ⧸ (s)` and the cardinality of `s`. -/
lemma Ideal.height_le_height_add_encard_of_subset (s : Set R) {p : Ideal R} [p.IsPrime]
    (hrm : s ⊆ p) : p.height ≤ (p.map (Quotient.mk (span s))).height + s.encard := by
  apply le_trans (Ideal.height_le_height_add_spanFinrank_of_le (I := span s) (p := p) ?_) ?_
  · rwa [span_le]
  · gcongr
    exact Submodule.spanFinrank_span_le_encard _

lemma Ideal.height_le_ringKrullDim_quotient_add_encard {p : Ideal R} [p.IsPrime]
    (s : Set R) (hs : s ⊆ p) : p.height ≤ ringKrullDim (R ⧸ span s) + s.encard := by
  refine le_trans (height_le_ringKrullDim_quotient_add_spanFinrank (I := .span s) ?_) ?_
  · simpa [span_le]
  · gcongr; norm_cast; exact Submodule.spanFinrank_span_le_encard _

lemma Ideal.height_le_height_add_one_of_mem {r : R} {p : Ideal R} [p.IsPrime] (hrm : r ∈ p) :
    p.height ≤ (p.map (Quotient.mk (span {r}))).height + 1 := by
  convert height_le_height_add_encard_of_subset {r} (p := p) (by simpa)
  simp

lemma Ideal.height_le_ringKrullDim_quotient_add_one {r : R} {p : Ideal R} [p.IsPrime]
    (hrp : r ∈ p) : p.height ≤ ringKrullDim (R ⧸ span {r}) + 1 := by
  convert Ideal.height_le_ringKrullDim_quotient_add_encard {r} (by simpa)
  simp

lemma ringKrullDim_le_ringKrullDim_quotient_add_encard (s : Set R) (hs : s ⊆ Ring.jacobson R) :
    ringKrullDim R ≤ ringKrullDim (R ⧸ Ideal.span s) + s.encard := by
  refine le_trans (ringKrullDim_le_ringKrullDim_quotient_add_spanFinrank (Ideal.span s) ?_) ?_
  · simpa [Ideal.span_le]
  · gcongr; norm_cast; exact Submodule.spanFinrank_span_le_encard _

lemma ringKrullDim_le_ringKrullDim_quotient_add_card (s : Finset R)
    (hs : (s : Set R) ⊆ Ring.jacobson R) :
    ringKrullDim R ≤ ringKrullDim (R ⧸ Ideal.span (s : Set R)) + s.card := by
  convert ringKrullDim_le_ringKrullDim_quotient_add_encard s hs
  norm_cast

section Algebra

variable {S : Type*} [CommRing S] [Algebra R S]

/--
If `P` lies over `p`, the height of `P` is bounded by the height of `p` plus
the height of the image of `P` in `S ⧸ p S`.
Equality holds if `S` satisfies going-down as an `R`-algebra
(see `Ideal.height_eq_height_add_of_liesOver_of_hasGoingDown`).
-/
@[stacks 00OM]
lemma Ideal.height_le_height_add_of_liesOver [IsNoetherianRing S] (p : Ideal R) [p.IsPrime]
      (P : Ideal S) [P.IsPrime] [P.LiesOver p] :
    P.height ≤ p.height +
      (P.map (Ideal.Quotient.mk <| p.map (algebraMap R S))).height := by
  classical
  obtain ⟨s, hp, heq⟩ := p.exists_finset_card_eq_height_of_isNoetherianRing
  let P' := P.map (Ideal.Quotient.mk <| p.map (algebraMap R S))
  obtain ⟨s', hP', heq'⟩ := P'.exists_finset_card_eq_height_of_isNoetherianRing
  have hsP'sub : (s' : Set <| S ⧸ (Ideal.map (algebraMap R S) p)) ⊆ (P' : Set <| S ⧸ _) :=
    fun x hx ↦ (Ideal.le_minimalPrimes hP') (Ideal.subset_span hx)
  have : Set.SurjOn (Ideal.Quotient.mk (p.map (algebraMap R S))) P s' := by
    refine Set.SurjOn.mono subset_rfl hsP'sub fun x hx ↦ ?_
    obtain ⟨y, rfl⟩ := Ideal.Quotient.mk_surjective x
    rw [SetLike.mem_coe, Ideal.mem_quotient_iff_mem] at hx
    · use y, hx
    · rw [Ideal.map_le_iff_le_comap, Ideal.LiesOver.over (p := p) (P := P)]
  obtain ⟨o, ho, hinj, himgo⟩ := s'.exists_subset_injOn_image_eq_of_surjOn (P : Set S) this
  let t : Finset S := Finset.image (algebraMap R S) s ∪ o
  suffices h : P.height ≤ t.card by
    rw [← heq, ← heq']
    apply le_trans h
    norm_cast
    refine le_trans (Finset.card_union_le _ _) (add_le_add Finset.card_image_le ?_)
    rw [← himgo, Finset.card_image_of_injOn hinj]
  refine Ideal.height_le_card_of_mem_minimalPrimes_span_finset ?_
  have : Ideal.span t = Ideal.map (algebraMap R S) (.span s) ⊔ .span o := by
    simp [t, Ideal.span_union, Ideal.map_span]
  refine this ▸ map_sup_mem_minimalPrimes_of_map_quotientMk_mem_minimalPrimes hp (span_le.mpr ho) ?_
  convert hP'
  simp [Ideal.map_span, ← himgo]

/--
If `S` satisfies going-down as an `R`-algebra and `P` lies over `p`, the height of `P` is equal
to the height of `p` plus the height of the image of `P` in `S ⧸ p S`
(Matsumura 13.B Th. 19 (2)).
-/
@[stacks 00ON]
lemma Ideal.height_eq_height_add_of_liesOver_of_hasGoingDown [IsNoetherianRing S]
    [Algebra.HasGoingDown R S] (p : Ideal R) [p.IsPrime] (P : Ideal S) [P.IsPrime] [P.LiesOver p] :
    P.height = p.height +
      (P.map (Ideal.Quotient.mk <| p.map (algebraMap R S))).height := by
  refine le_antisymm (height_le_height_add_of_liesOver p P) ?_
  obtain ⟨lp, hlp, hlenp⟩ := p.exists_ltSeries_length_eq_height
  obtain ⟨lq, hlq, hlenq⟩ :=
    (P.map (Quotient.mk (p.map (algebraMap R S)))).exists_ltSeries_length_eq_height
  let l' : LTSeries (PrimeSpectrum S) :=
    lq.map (PrimeSpectrum.comap (Quotient.mk (p.map (algebraMap R S))))
      (RingHom.strictMono_comap_of_surjective Quotient.mk_surjective)
  have : l'.head.asIdeal.LiesOver lp.last.asIdeal := by
    simp only [LTSeries.head_map, hlp, l']
    refine ⟨?_⟩
    refine le_antisymm ?_ ?_
    · rw [← map_le_iff_le_comap, PrimeSpectrum.comap_asIdeal, ← map_le_iff_le_comap]
      simp
    · conv_rhs => rw [LiesOver.over (p := p) (P := P), under_def]
      refine comap_mono (le_trans (comap_mono (lq.head_le_last)) ?_)
      simp [hlq, map_le_iff_le_comap, LiesOver.over (p := p) (P := P)]
  obtain ⟨lp', hlp'len, hlp', _⟩ := exists_ltSeries_of_hasGoingDown lp l'.head.asIdeal
  have : (lp'.smash l' hlp').length = lp.length + lq.length := by simp [hlp'len, l']
  rw [← hlenp, ← hlenq, ← Nat.cast_add, ← this, height_eq_primeHeight]
  apply Order.length_le_height
  simp [hlq, l', ← PrimeSpectrum.asIdeal_le_asIdeal, map_le_iff_le_comap,
    LiesOver.over (p := p) (P := P)]

variable (R) in
lemma ringKrullDim_le_spanFinrank_maximalIdeal [IsLocalRing R] :
    ringKrullDim R ≤ (IsLocalRing.maximalIdeal R).spanFinrank :=
  le_of_eq_of_le IsLocalRing.maximalIdeal_height_eq_ringKrullDim.symm
    (WithBot.coe_le_coe.mpr (Ideal.height_le_spanFinrank (IsLocalRing.maximalIdeal R)
      Ideal.IsPrime.ne_top'))

end Algebra