English
The height of the comap of a prime ideal under an algebra map equals the height of the original prime ideal.
Русский
Высота комапа простого идеала через алгебраическое отображение равна высоте исходного простого идеала.
LaTeX
$$$\operatorname{height}(J \downarrow) = \operatorname{height}(J).$$$
Lean4
@[simp]
theorem height_comap {S : Type*} [CommRing S] (e : R ≃+* S) (I : Ideal S) : (I.comap e).height = I.height :=
by
refine (Equiv.iInf_congr e.idealComapOrderIso fun J ↦ (Equiv.iInf_congr ?_ fun h ↦ ?_).symm).symm
· refine .ofIff ?_
rw [← Ideal.comap_coe, Ideal.comap_minimalPrimes_eq_of_surjective (f := (↑e : R →+* S)) e.surjective]
exact e.idealComapOrderIso.injective.mem_set_image.symm
· have : J.IsPrime := h.1.1
simp only [EquivLike.coe_coe, RingEquiv.idealComapOrderIso_apply, ← Ideal.height_eq_primeHeight,
RingEquiv.height_comap_of_isPrime]
