English
The comap of the image equals the join of the original subring with the kernel closure; i.e., (s.map f).comap f = s ⊔ closure (f^{-1}({0})).
Русский
Обратное отображения образа равняется объединению исходного подкольца и замыкания ядра: (s.map f).comap f = s ⊔ closure (f^{-1}({0})).
LaTeX
$$(s.map f).comap f = s \u222a closure (f^{-1} {0})$$
Lean4
theorem comap_map_eq (f : R →+* S) (s : Subring R) : (s.map f).comap f = s ⊔ closure (f ⁻¹' {0}) :=
by
apply le_antisymm
· intro x hx
rw [mem_comap, mem_map] at hx
obtain ⟨y, hy, hxy⟩ := hx
replace hxy : x - y ∈ f ⁻¹' {0} := by simp [hxy]
rw [← closure_eq s, ← closure_union, ← add_sub_cancel y x]
exact Subring.add_mem _ (subset_closure <| Or.inl hy) (subset_closure <| Or.inr hxy)
· rw [← map_le_iff_le_comap, map_sup, f.map_closure]
apply le_of_eq
rw [sup_eq_left, closure_le]
exact (Set.image_preimage_subset f {0}).trans (Set.singleton_subset_iff.2 (s.map f).zero_mem)
