instIsAffinePullbackSchemeOfIsAffineHom_1

English

Same as above, in the general setting of schemes with IsAffineHom on f and IsAffine Y.

Русский

Аффинность обратно-произведения в общем случае схем.

LaTeX

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

Lean4

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

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