isMaximal_comap_of_isIntegral_of_isMaximal'

English

If f is integral, then comap f I is maximal whenever I is maximal.

Русский

Если f интегрально, то I максимален тогда и только тогда, когда comap f I максимален.

LaTeX

$$$$\text{IsIntegral}(R,S) \Rightarrow \bigl(\text{IsMaximal}(I) \Rightarrow \text{IsMaximal}(I^{\mathrm{comap} f})\bigr).$$$$

Lean4

theorem isMaximal_comap_of_isIntegral_of_isMaximal' {R S : Type*} [CommRing R] [CommRing S] (f : R →+* S)
    (hf : f.IsIntegral) (I : Ideal S) [I.IsMaximal] : IsMaximal (I.comap f) :=
  let _ : Algebra R S := f.toAlgebra
  have : Algebra.IsIntegral R S := ⟨hf⟩
  isMaximal_comap_of_isIntegral_of_isMaximal (R := R) (S := S) I

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