English
If f is a closed embedding and the range complement is retrocompact, then the image of a constructible set is constructible.
Русский
Если f — замкнутое вложение и дополнение диапазона ретрокомпактно, то образ конструируемого множества конструируем.
LaTeX
$$$\\forall f:\\ X \\to Y, IsClosedEmbedding(f) \\Rightarrow IsRetrocompact((range f)^{c}) \\Rightarrow IsConstructible(s) \\Rightarrow IsConstructible(f''s).$$$
Lean4
@[stacks 09YG]
theorem image_of_isClosedEmbedding (hf : IsClosedEmbedding f) (hfcomp : IsRetrocompact (range f)ᶜ)
(hs : IsConstructible s) : IsConstructible (f '' s) := by
induction hs using IsConstructible.empty_union_induction with
| open_retrocompact U hUopen
hUcomp =>
have hfU : IsOpen (f '' U ∪ (range f)ᶜ) := by
simpa [← range_diff_image hf.injective, sdiff_eq, compl_inter, union_comm] using
(hf.isClosedMap _ hUopen.isClosed_compl).isOpen_compl
suffices h : IsRetrocompact (f '' U ∪ (range f)ᶜ) by
simpa [union_inter_distrib_right, inter_eq_left.2 (image_subset_range ..)] using
(h.isConstructible hfU).sdiff (hfcomp.isConstructible hf.isClosed_range.isOpen_compl)
rintro V hVcomp hVopen
rw [union_inter_distrib_right, ← image_inter_preimage]
exact
((hUcomp (hf.isCompact_preimage hVcomp) (hVopen.preimage hf.continuous)).image hf.continuous).union <|
hfcomp hVcomp hVopen
| union s hs t ht hs' ht' => rw [image_union]; exact hs'.union ht'
| compl s hs hs' =>
rw [← range_diff_image hf.injective]
exact (hfcomp.isConstructible hf.isClosed_range.isOpen_compl).of_compl.sdiff hs'
