English
Let f: X → Y and g: U → Y with [IsOpenImmersion f]. Then the range of the first projection from the pullback is the image of the range of f under g, i.e. the opens on the right-hand side reflect the pushforward of f along g.
Русский
Пусть f: X → Y, g: U → Y и f открыто вложение. Тогда образ fst pullback равен образу диапазона f по g, то есть откр. множество справа отображается как образ f под g.
LaTeX
$$$\\operatorname{range}(\\mathrm{pullback}.fst\\ g\\ f).base = ((Opens.map g.base).obj ⟨\\operatorname{range} f.base, H.base_open.isOpen_range⟩).1$$$
Lean4
theorem range_pullback_fst_of_right :
Set.range (pullback.fst g f).base = ((Opens.map g.base).obj ⟨Set.range f.base, H.base_open.isOpen_range⟩).1 :=
by
rw [← show _ = (pullback.fst g f).base from PreservesPullback.iso_hom_fst Scheme.forgetToTop g f, TopCat.coe_comp,
Set.range_comp, Set.range_eq_univ.mpr, ← @Set.preimage_univ _ _ (pullback.snd g.base f.base)]
-- Porting note (https://github.com/leanprover-community/mathlib4/issues/11224): was `rw`
· erw [TopCat.pullback_fst_image_snd_preimage]
rw [Set.image_univ]
rfl
rw [← TopCat.epi_iff_surjective]
infer_instance
