English
There is an order isomorphism between ideals of R × S and pairs of ideals (I, J) with I ⊆ R and J ⊆ S.
Русский
Существуют взаимно однозначно соответствия между идеалами в R × S и парами идеалов (I, J) в R и S.
LaTeX
$$$\\text{idealProdEquiv} : \\mathrm{Ideal}(R \\times S) \\cong_o \\mathrm{Ideal}(R) \\times \\mathrm{Ideal}(S)$$$
Lean4
/-- Ideals of `R × S` are in one-to-one correspondence with pairs of ideals of `R` and ideals of
`S`. -/
def idealProdEquiv : Ideal (R × S) ≃o Ideal R × Ideal S
where
toFun I := ⟨map (RingHom.fst R S) I, map (RingHom.snd R S) I⟩
invFun I := prod I.1 I.2
left_inv I := (ideal_prod_eq I).symm
right_inv := fun ⟨I, J⟩ => by simp
map_rel_iff'
{I J} := by
simp only [Equiv.coe_fn_mk, ge_iff_le, Prod.mk_le_mk]
refine ⟨fun h ↦ ?_, fun h ↦ ⟨map_mono h, map_mono h⟩⟩
rw [ideal_prod_eq I, ideal_prod_eq J]
exact inf_le_inf (comap_mono h.1) (comap_mono h.2)
