Properties of schemes and of morphisms of schemes

Properties, absent from Mathlib, of the schemes and structure morphisms over which the algebraic main theorems quantify.

• A morphism of schemes is of finite type if it is locally of finite type and quasi-compact [TSPA, Tag 01T0]. The class AlgebraicGeometry.FiniteType bundles Mathlib's LocallyOfFiniteType and QuasiCompact, as Mathlib's IsProper bundles its parts, and its parents are instances.
• HasDisjointIntegralComponents X: X is reduced and its irreducible components are pairwise disjoint — for a scheme of finite type over a field, a finite disjoint union of integral schemes, the schemes on which Kollár constructs the resolution functor before gluing [Kol07, Proposition 37 and the proof of Theorem 36].

class AlgebraicGeometry.FiniteType {X Y : Scheme} (f : X ⟶ Y) extends AlgebraicGeometry.LocallyOfFiniteType f, AlgebraicGeometry.QuasiCompact f : Prop

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

• finiteType_appLE {U : Y.Opens} : IsAffineOpen U → ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U), (CommRingCat.Hom.hom (Scheme.Hom.appLE f U V e)).FiniteType
• isCompact_preimage (U : Set ↥Y) : IsOpen U → IsCompact U → IsCompact (⇑f ⁻¹' U)