Morphisms of finite type

A morphism of schemes is of finite type (AlgebraicGeometry.FiniteType) if it is locally of finite type and quasi-compact [TSPA, Tag 01T0]. The class is bundled like Mathlib's IsProper: its parents are instances, and conversely FiniteType f is inferred from the two parts (the instance FiniteType.of_locallyOfFiniteType_of_quasiCompact), so that statements may carry the bundled class while the lemmas feeding them keep the two unbundled ones. finiteType_iff unbundles it.

theorem AlgebraicGeometry.finiteType_iff {X Y : Scheme} (f : X ⟶ Y) : FiniteType f ↔ LocallyOfFiniteType f ∧ QuasiCompact f

instance AlgebraicGeometry.FiniteType.of_locallyOfFiniteType_of_quasiCompact {X Y : Scheme} (f : X ⟶ Y) [LocallyOfFiniteType f] [QuasiCompact f] : FiniteType f

A morphism that is locally of finite type and quasi-compact is of finite type.