English
Ideals in a finite direct product correspond to tuples of ideals in the factors, in an order-preserving way.
Русский
Идеалы в конечном прямом произведении соответствуют кортежам идеалов в фактор-колечах, сохраняющих порядок.
LaTeX
$$Definition: piOrderIso describes an order isomorphism between Ideals of Π_i R_i and Π_i Ideals(R_i) when ι is finite.$$
Lean4
/-- If `f : R ≃+* S` is a ring isomorphism and `I : Ideal R`,
then `comap f (comap f.symm I) = I`. -/
@[simp]
theorem comap_of_equiv {I : Ideal R} (f : R ≃+* S) : (I.comap (f.symm : S →+* R)).comap (f : R →+* S) = I := by
rw [← RingEquiv.toRingHom_eq_coe, ← RingEquiv.toRingHom_eq_coe, comap_comap, RingEquiv.toRingHom_eq_coe,
RingEquiv.toRingHom_eq_coe, RingEquiv.symm_comp, comap_id]
