English
In a localization setting, for any ideal J of S, the map sending the comap of J back to S via the localization algebra equals J itself; i.e., pulling J back to R then pushing forward again recovers J.
Русский
В локализационной системе для любого идеала J кольца S отображение, возвращающее образ через локализационную алгебраическую карту, даёт то же самое идеал J.
LaTeX
$$$\\operatorname{Ideal.map}(\\mathrm{algebraMap}\\;R\\;S)(\\operatorname{Ideal.comap}(\\mathrm{algebraMap}\\;R\\;S)\\,J)=J$$$
Lean4
theorem map_comap (J : Ideal S) : Ideal.map (algebraMap R S) (Ideal.comap (algebraMap R S) J) = J :=
le_antisymm (Ideal.map_le_iff_le_comap.2 le_rfl) fun x hJ =>
by
obtain ⟨r, s, hx⟩ := mk'_surjective M x
rw [← hx] at hJ ⊢
exact
Ideal.mul_mem_right _ _
(Ideal.mem_map_of_mem _
(show (algebraMap R S) r ∈ J from mk'_spec S r s ▸ J.mul_mem_right ((algebraMap R S) s) hJ))
