English
The principal-equivalence is a multiplicative equivalence between the associates of nonzero divisors and the principal-nonzero-divisors submonoid.
Русский
Главное эквивалентное отображение является мультипликативной эквивалентностью между ассоциатами не нулевых делителей и подмоноидом главных не нулевых делителей.
LaTeX
$$$\mathrm{associatesNonZeroDivisorsEquivIsPrincipal}\ \ R \;:\; \mathrm{Associates}(R)^{0} \; \to_*\; (\text{isPrincipalNonZeroDivisorsSubmonoid } R)$$$
Lean4
/-- 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 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 <| hp.1.2 <| 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
