English
If f is an open embedding and the codomain is quasi-sober, then the domain is quasi-sober as well.
Русский
Если отображение является открытым вложением и кодоменм пространство квазисобро, то домен тоже квазисоберный.
LaTeX
$$$\\text{QuasiSober}(\\alpha)$, given $f: \\alpha \\to \\beta$ open embedding and $\\text{QuasiSober}(\\beta)$.$$
Lean4
theorem quasiSober {f : α → β} (hf : IsOpenEmbedding f) [QuasiSober β] : QuasiSober α where
sober hS
hS' := by
have hS'' := hS.image f hf.continuous.continuousOn
obtain ⟨x, hx⟩ := QuasiSober.sober hS''.closure isClosed_closure
obtain ⟨T, hT, rfl⟩ := hf.isInducing.isClosed_iff.mp hS'
rw [image_preimage_eq_inter_range] at hx hS''
have hxT : x ∈ T := by
rw [← hT.closure_eq]
exact closure_mono inter_subset_left hx.mem
obtain ⟨y, rfl⟩ : x ∈ range f := by
rw [hx.mem_open_set_iff hf.isOpen_range]
refine Nonempty.mono ?_ hS''.1
simpa using subset_closure
use y
change _ = _
rw [hf.isEmbedding.closure_eq_preimage_closure_image, image_singleton, show _ = _ from hx]
apply image_injective.mpr hf.injective
ext z
simp only [image_preimage_eq_inter_range, mem_inter_iff, and_congr_left_iff]
exact fun hy => ⟨fun h => hT.closure_eq ▸ closure_mono inter_subset_left h, fun h => subset_closure ⟨h, hy⟩⟩
