English
Let f: X → Z be an open immersion and g: Y → Z any morphism. Then the base map of the second projection in the pullback X ×_Z Y has as its image the preimage under g of the open range of f; i.e. the range of pullback.snd(f,g).base equals g^{-1}(f.opensRange).
Русский
Пусть f: X → Z является открытым вложением, и g: Y → Z произвольен. Тогда образ базовой части второго проекции в произведении по г: X ×_Z Y имеет вид преизображения под g открытого множества, порождаемого f; то есть образ pullback.snd(f,g).base совпадает с g^{-1}(f.opensRange).
LaTeX
$$$\\operatorname{range}((\\mathrm{pullback}.snd\\, f\\, g).\\text{base}) = (g^{-1}\\!\\_\\text{ᵁ} f.opensRange).1$$$
Lean4
theorem range_pullback_snd_of_left : Set.range (pullback.snd f g).base = (g ⁻¹ᵁ f.opensRange).1 :=
by
rw [← show _ = (pullback.snd f g).base from PreservesPullback.iso_hom_snd Scheme.forgetToTop f g, TopCat.coe_comp,
Set.range_comp, Set.range_eq_univ.mpr, ← @Set.preimage_univ _ _ (pullback.fst f.base g.base)]
-- Porting note (https://github.com/leanprover-community/mathlib4/issues/11224): was `rw`
· erw [TopCat.pullback_snd_image_fst_preimage]
rw [Set.image_univ]
rfl
rw [← TopCat.epi_iff_surjective]
infer_instance
