isMaximal_comap_of_isIntegral_of_isMaximal

English

If I is prime and comap f I is maximal, then I is maximal.

Русский

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

LaTeX

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

Lean4

theorem isMaximal_comap_of_isIntegral_of_isMaximal [Algebra.IsIntegral R S] (I : Ideal S) [hI : I.IsMaximal] :
    IsMaximal (I.comap (algebraMap R S)) :=
  by
  refine Ideal.Quotient.maximal_of_isField _ ?_
  haveI : IsPrime (I.comap (algebraMap R S)) := comap_isPrime _ _
  exact
    isField_of_isIntegral_of_isField algebraMap_quotient_injective
      (by rwa [← Quotient.maximal_ideal_iff_isField_quotient])

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