mathlib3 documentation

algebraic_geometry.morphisms.finite_type

Morphisms of finite type #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

A morphism of schemes f : X ⟶ Y is locally of finite type if for each affine U ⊆ Y and V ⊆ f ⁻¹' U, The induced map Γ(Y, U) ⟶ Γ(X, V) is of finite type.

A morphism of schemes is of finite type if it is both locally of finite type and quasi-compact.

We show that these properties are local, and are stable under compositions.

@[class]

A morphism of schemes f : X ⟶ Y is locally of finite type if for each affine U ⊆ Y and V ⊆ f ⁻¹' U, The induced map Γ(Y, U) ⟶ Γ(X, V) is of finite type.

Instances of this typeclass