Documentation

Mathlib.AlgebraicGeometry.Morphisms.Affine

Affine morphisms of schemes #

A morphism of schemes f : X ⟶ Y is affine if the preimage of an arbitrary affine open subset of Y is affine.

It is equivalent to ask only that Y is covered by affine opens whose preimage is affine.

Main results #

We also provide the instance HasAffineProperty @IsAffineHom fun X _ _ _ ↦ IsAffine X.

class AlgebraicGeometry.IsAffineHom {X Y : Scheme} (f : X Y) :

A morphism of schemes X ⟶ Y is affine if the preimage of any affine open subset of Y is affine.

Instances
    @[deprecated AlgebraicGeometry.IsAffineOpen.preimage (since := "2025-10-07")]

    Alias of AlgebraicGeometry.IsAffineOpen.preimage.

    If s is a spanning set of Γ(X, U), such that each X.basicOpen i is affine, then U is also affine.

    @[instance 100]

    If the underlying map of a morphism is inducing and has closed range, then it is affine.