isMaximal_of_isIntegral_of_isMaximal_comap'

English

If f is integral and I is maximal, then the comap of I along f is maximal.

Русский

Если f интегрально и I максимален, то обратный образ I по f максимален.

LaTeX

$$$$\text{IsMaximal}(I) \Rightarrow \text{IsMaximal}(I^{\mathrm{comap} f}).$$$$

Lean4

theorem isMaximal_of_isIntegral_of_isMaximal_comap' (f : R →+* S) (hf : f.IsIntegral) (I : Ideal S) [I.IsPrime]
    (hI : IsMaximal (I.comap f)) : IsMaximal I :=
  let _ : Algebra R S := f.toAlgebra
  have : Algebra.IsIntegral R S := ⟨hf⟩
  isMaximal_of_isIntegral_of_isMaximal_comap (R := R) (S := S) I hI

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