instIsAffineFiberOfIsAffineHom — Mathlib

English

If f is an affine morphism, then every fiber over a point is an affine scheme.

Русский

Если f аффинный морфизм, то каждое волокно над точкой аффинно схематично.

LaTeX

$$IsAffine((f.fiber y))$$

Lean4

instance (f : X ⟶ Y) [IsAffineHom f] (y : Y) : IsAffine (f.fiber y) :=
  haveI : IsAffineHom (f.fiberToSpecResidueField y) := MorphismProperty.pullback_snd _ _ inferInstance
  isAffine_of_isAffineHom (f.fiberToSpecResidueField y)

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