English
For surjective f, there exists an order isomorphism between Ideals(S) and a subobject of Ideals(R) describing the correspondence of primes via comap/map.
Русский
При сюръективности f существует упорядоченное изоморфное соответствие между Ideals(S) и подмножеством Ideals(R), описывающее соответствие простых через comap/map.
LaTeX
$$Ideal.relIsoOfSurjective f : Ideal S ≃o { p : Ideal R // comap f ⊥ ≤ p }$$
Lean4
protected theorem map_mul {R} [Semiring R] [FunLike F R S] [RingHomClass F R S] (f : F) (I J : Ideal R) :
map f (I * J) = map f I * map f J :=
le_antisymm
(map_le_iff_le_comap.2 <|
mul_le.2 fun r hri s hsj =>
show (f (r * s)) ∈ map f I * map f J by rw [map_mul];
exact mul_mem_mul (mem_map_of_mem f hri) (mem_map_of_mem f hsj))
(span_mul_span (↑f '' ↑I) (↑f '' ↑J) ▸
(span_le.2 <|
Set.iUnion₂_subset fun _ ⟨r, hri, hfri⟩ =>
Set.iUnion₂_subset fun _ ⟨s, hsj, hfsj⟩ =>
Set.singleton_subset_iff.2 <|
hfri ▸ hfsj ▸ by rw [← map_mul]; exact mem_map_of_mem f (mul_mem_mul hri hsj)))
