comap_lt_comap — Mathlib

English

In an integral closure setting, comap of I is maximal whenever I is maximal (and domain towers satisfy hypotheses).

Русский

В рамках интегрального замыкания образ обратного образа сохраняет максимальность по цепям.

LaTeX

$$$$\text{Ideal.IsIntegralClosure.comap}(I)\text{ maximal} \Leftarrow \text{IsMaximal}(I).$$$$

Lean4

theorem comap_lt_comap {I J : Ideal (integralClosure R S)} [I.IsPrime] (I_lt_J : I < J) :
    I.comap (algebraMap R (integralClosure R S)) < J.comap (algebraMap R (integralClosure R S)) :=
  IsIntegralClosure.comap_lt_comap S I_lt_J

Похожие утверждения