instIsStableUnderBaseChangeScheme

English

In the setting of schemes, the stability of surjectivity under base change holds: surjectivity of g over S implies surjectivity of fst in the pullback X ×_S Y → X.

Русский

В контексте схем сохранение сюръективности при базовом изменении: сюръективность g над S влечёт сюръективность fst в произведении на шаре X ×_S Y → X.

LaTeX

$$$S.\mathrm{Surjective} g \Rightarrow S.\mathrm{Surjective} (pullback.fst f g)$$$

Lean4

instance : MorphismProperty.IsStableUnderBaseChange @Surjective :=
  by
  refine .mk' ?_
  introv hg
  simp only [surjective_iff, ← Set.range_eq_univ, Scheme.Pullback.range_fst] at hg ⊢
  rw [hg, Set.preimage_univ]

Похожие утверждения