instFstScheme — Mathlib

English

For any X,Y,Z and morphisms f,g, the projection fst of the pullback is itself a surjection under the appropriate base change assumptions in the scheme category.

Русский

Для любых схем X,Y,Z и отображений f,g проекция fst от произведения pullback является сюръективной при соответствующих условиях базового изменения.

LaTeX

$$$\forall f,g:\; Surjective (pullback.fst f g) $$$

Lean4

instance {X Y Z : Scheme.{u}} (f : X ⟶ Z) (g : Y ⟶ Z) [Surjective g] : Surjective (pullback.fst f g) :=
  MorphismProperty.pullback_fst _ _ inferInstance

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