English
An isomorphism of rings induces an order isomorphism between the lattices of ideals.
Русский
Изоморфизм колец порождает упорядоченное изоморфизмой между решетками идеалов.
LaTeX
$$$$ \\text{For } e:R\\cong+^* S,\\; \\text{Ideal}(S) \\cong_o \\text{Ideal}(R). $$$$
Lean4
/-- Any ring isomorphism induces an order isomorphism of ideals. -/
@[simps apply]
def idealComapOrderIso {R S : Type*} [Semiring R] [Semiring S] (e : R ≃+* S) : Ideal S ≃o Ideal R
where
toFun I := I.comap e
invFun I := I.map e
left_inv I := I.map_comap_of_surjective _ e.surjective
right_inv I := I.comap_map_of_bijective _ e.bijective
map_rel_iff' := by simp [← Ideal.map_le_iff_le_comap, Ideal.map_comap_of_surjective _ e.surjective]
