instIsAffinePullbackSchemeOfIsAffineHom

English

If f: X → S is affine and g: Y → S is any morphism with IsAffine Y, then the pullback X×_S Y → Y is affine.

Русский

Если f: X → S аффинен и g: Y → S аффинности, тогда произведение по основанию — аффинно.

LaTeX

$$$[IsAffineHom f] \\land [IsAffine Y] \\Rightarrow IsAffine (pullback f g)$$$

Lean4

instance {X Y S : Scheme} (f : X ⟶ S) (g : Y ⟶ S) [IsAffineHom f] [IsAffine Y] : IsAffine (pullback f g) :=
  letI : IsAffineHom (pullback.snd f g) := MorphismProperty.pullback_snd _ _ ‹_›
  isAffine_of_isAffineHom (pullback.snd f g)

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