map_comap_eq_self_of_equiv — Mathlib

English

For a maximal ideal I in the i-th factor R_i, the pulled back along the i-th projection to the full product is a maximal ideal of the product.

Русский

Для максимального идеала I в R_i его предобраз через i-колонку к произведению становится максимальным идеалом в произведении.

LaTeX

$$$\forall i, \ I_i \ IsMaximal \Rightarrow (I_i.\comap (\Pi^{\mathrm{eval}}_{R,i}) ).IsMaximal$$$

Lean4

theorem map_comap_eq_self_of_equiv {E : Type*} [EquivLike E R S] [RingEquivClass E R S] (e : E) (I : Ideal S) :
    map e (comap e I) = I :=
  I.map_comap_of_surjective e (EquivLike.surjective e)

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