English
If a morphism of schemes f: X → Z is surjective, then the base-changed projection from the pullback to X is surjective as well.
Русский
Если отображение f: X → Z сюръективно, то после базового изменения проекция из pullback к X остаётся сюръективной.
LaTeX
$$$\forall f,g,\; \, \text{Surjective } f \Rightarrow \text{Surjective} (pullback.fst f g)$$$
Lean4
/-- The comparison map for pullbacks under the forgetful functor `Scheme ⥤ Type u` is surjective. -/
theorem pullbackComparison_forget_surjective {X Y S : Scheme.{u}} (f : X ⟶ S) (g : Y ⟶ S) :
Function.Surjective (pullbackComparison forget f g) :=
by
refine .of_comp_left (fun x ↦ ?_) <| injective_of_mono (Types.pullbackIsoPullback (forget.map f) (forget.map g)).hom
obtain ⟨z, h1, h2⟩ := Pullback.exists_preimage_pullback (f := f) (g := g) x.1.1 x.1.2 x.2
use z
ext
· simp only [Function.comp_apply, Types.pullbackIsoPullback_hom_fst]
rwa [← types_comp_apply (g := pullback.fst _ _), pullbackComparison_comp_fst]
· simp only [Function.comp_apply, Types.pullbackIsoPullback_hom_snd]
rwa [← types_comp_apply (g := pullback.snd _ _), pullbackComparison_comp_snd]
