AlgebraicGeometry.locallyOfFiniteType_eq

theorem AlgebraicGeometry.locallyOfFiniteType_eq : @AlgebraicGeometry.LocallyOfFiniteType = AlgebraicGeometry.affineLocally @RingHom.FiniteType

The theorem `AlgebraicGeometry.locallyOfFiniteType_eq` states that a morphism in the category of schemes is locally of finite type if and only if for every pair of affine opens, one in the source and its preimage in the target, the induced ring homomorphism between their coordinate rings satisfies the property of being of finite type. Thus, it connects the geometric notion of being locally of finite type with the algebraic notion of ring homomorphisms being of finite type. This means, in essence, that the morphism has the property that the target is finitely generated as an algebra over the source, for every pair of affine open subsets, one in the source and its preimage in the target.

More concisely: A morphism of schemes is locally of finite type if and only if the induced homomorphism between the coordinate rings of every pair of affine open subsets is of finite type.