English
If f is a bijective ring homomorphism between R and S, then there is a natural order isomorphism between Ideals(S) and Ideals(R) given by comap f and map f, with inverse map given by map f and comap f swapped.
Русский
Если f — биективный кольцевой гомоморфизм между R и S, существует естественное упорядоченное биективное соответствие между Ideals(S) и Ideals(R), заданное comap f и map f с обратной связью.
LaTeX
$$Ideal.S ≃o Ideal.R via toFun := comap f, invFun := map f, left_inv := map_comap_of_surjective _, right_inv := …$$
Lean4
/-- Special case of the correspondence theorem for isomorphic rings -/
def relIsoOfBijective : Ideal S ≃o Ideal R where
toFun := comap f
invFun := map f
left_inv := map_comap_of_surjective _ hf.2
right_inv
J :=
le_antisymm
(fun _ h ↦
have ⟨y, hy, eq⟩ := (mem_map_iff_of_surjective _ hf.2).mp h;
hf.1 eq ▸ hy)
le_comap_map
map_rel_iff'
{_ _} := by
refine ⟨fun h ↦ ?_, comap_mono⟩
have := map_mono (f := f) h
simpa only [Equiv.coe_fn_mk, map_comap_of_surjective f hf.2] using this
