English
The principal-equivalence sends 1 to the unit ideal 1.
Русский
Главное эквивалентное отображение отправляет 1 в единичный идеал.
LaTeX
$$$(associatesNonZeroDivisorsEquivIsPrincipal\ R\ 1 : \mathrm{Ideal} R) = 1$$$
Lean4
theorem 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 := hp.1.1
have hfp : RingHom.ker f ≤ p := I.mk_ker.trans_le (le_sup_left.trans hp.1.2)
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 hp.1.2)⟩, 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⟩
