English
In a Noetherian ring, for any ideal I and r with r ≤ I.height, there exists J ≤ I with J.spanRank ≤ r and r ≤ J.height.
Русский
В кольце Нотереан для любого идеала I и r ≤ height(I) существует J ≤ I с J.spanRank ≤ r и r ≤ J.height.
LaTeX
$$$\forall I, r: \operatorname{Nat}, r \le I.height \Rightarrow \exists J \le I, J.spanRank \le r \land r \le J.height.$$$
Lean4
theorem exists_spanRank_le_and_le_height_of_le_height [IsNoetherianRing R] (I : Ideal R) (r : ℕ) (hr : r ≤ I.height) :
∃ J ≤ I, J.spanRank ≤ r ∧ r ≤ J.height := by
induction r with
| zero =>
refine ⟨⊥, bot_le, ?_, zero_le _⟩
rw [Submodule.spanRank_bot]
exact le_refl 0
| succ r ih =>
obtain ⟨J, h₁, h₂, h₃⟩ := ih ((WithTop.coe_le_coe.mpr r.le_succ).trans hr)
let S := {K | K ∈ J.minimalPrimes ∧ Ideal.height K = r}
have hS : Set.Finite S := Set.Finite.subset J.finite_minimalPrimes_of_isNoetherianRing (fun _ h => h.1)
have : ¬(I : Set R) ⊆ ⋃ K ∈ hS.toFinset, (K : Set R) :=
by
refine (Ideal.subset_union_prime ⊥ ⊥ ?_).not.mpr ?_
· rintro K hK - -
rw [Set.Finite.mem_toFinset] at hK
exact hK.1.1.1
· push_neg
intro K hK e
have := hr.trans (Ideal.height_mono e)
rw [Set.Finite.mem_toFinset] at hK
rw [hK.2, ← not_lt] at this
norm_cast at this
exact this r.lt_succ_self
simp_rw [Set.not_subset, Set.mem_iUnion, not_exists, Set.Finite.mem_toFinset] at this
obtain ⟨x, hx₁, hx₂⟩ := this
refine ⟨J ⊔ Ideal.span { x }, sup_le h₁ ?_, ?_, ?_⟩
· rwa [Ideal.span_le, Set.singleton_subset_iff]
· apply Submodule.spanRank_sup_le_sum_spanRank.trans
push_cast
exact add_le_add h₂ ((Submodule.spanRank_span_le_card _).trans (by simp))
· refine le_iInf₂ (fun p hp ↦ ?_)
have := hp.1.1
by_cases h : p.height = ⊤
· rw [← p.height_eq_primeHeight, h]
exact le_top
have : p.FiniteHeight := ⟨Or.inr h⟩
have := Ideal.height_mono (le_sup_left.trans hp.1.2)
suffices h : (r : ℕ∞) ≠ p.primeHeight by
push_cast
have := h₃.trans this
rw [Ideal.height_eq_primeHeight] at this
exact Order.add_one_le_of_lt (lt_of_le_of_ne this h)
intro e
apply hx₂ p
· have : J.height = p.primeHeight := by
apply le_antisymm
· rwa [← p.height_eq_primeHeight]
· rwa [← e]
refine ⟨mem_minimalPrimes_of_primeHeight_eq_height (le_sup_left.trans hp.1.2) this.symm, ?_⟩
rwa [p.height_eq_primeHeight, eq_comm]
· exact hp.1.2 <| Ideal.mem_sup_right <| Ideal.subset_span <| Set.mem_singleton x
