Documentation

Mathlib.AlgebraicGeometry.Morphisms.Finite

Finite morphisms of schemes #

A morphism of schemes f : X ⟶ Y is finite if the preimage of an arbitrary affine open subset of Y is affine and the induced ring map is finite.

It is equivalent to ask only that Y is covered by affine opens whose preimage is affine and the induced ring map is finite.

Also see AlgebraicGeometry.IsFinite.finite_preimage_singleton in Mathlib/AlgebraicGeometry/Fiber.lean for the fact that finite morphisms have finite fibers.

A morphism of schemes X ⟶ Y is finite if the preimage of any affine open subset of Y is affine and the induced ring hom is finite.

Instances
    @[instance 900]

    If X is a jacobson scheme and k is a field, Spec(k) ⟶ X is finite iff it is (locally) of finite type. (The statement is more general to allow the empty scheme as well)