English
There is a correspondence (an order isomorphism) between Ideals(S) and the set of primes in R under comap/map, parameterized by a surjective f.
Русский
Существует соответствие (упорядоченная изоморфия) между Ideals(S) и идеалами R через comap/map, заданное сюръективным отображением.
LaTeX
$$Ideal.relIsoOfSurjective : Ideal S ≃o { p : Ideal R // comap f ⊥ ≤ p }$$
Lean4
/-- Correspondence theorem -/
def relIsoOfSurjective (hf : Function.Surjective f) : Ideal S ≃o { p : Ideal R // comap f ⊥ ≤ p }
where
toFun J := ⟨comap f J, comap_mono bot_le⟩
invFun I := map f I.1
left_inv J := map_comap_of_surjective f hf J
right_inv
I :=
Subtype.eq <|
show comap f (map f I.1) = I.1 from
(comap_map_of_surjective f hf I).symm ▸ le_antisymm (sup_le le_rfl I.2) le_sup_left
map_rel_iff'
{I1 I2} :=
⟨fun H => map_comap_of_surjective f hf I1 ▸ map_comap_of_surjective f hf I2 ▸ map_mono H, comap_mono⟩
-- May not hold if `R` is a semiring: consider `ℕ →+* ZMod 2`.
