Varieties over a field

A variety over k is a scheme with a structure morphism to Spec k that is integral and locally of finite type. This file states that the way Mathlib states every property of a scheme over a base: the scheme is X : Scheme, the structure morphism is the X.Over (Spec k) instance with its notation X ↘ Spec k, and "variety" is the Prop-valued class IsVariety k X extending Mathlib's IsIntegral X and LocallyOfFiniteType (X ↘ Spec k), exactly as IsProper extends its constituents.

There is no bundled a variety over k type. A bundle is a second carrier for an object Mathlib already has, and every API written against it has to be unwrapped before Mathlib's own results about X apply. Consequently:

• an API about a variety takes (X : Scheme.{u}) [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] and writes X ↘ Spec (CommRingCat.of k) for the structure morphism;
• IsSmoothProperVariety k X is the conjunction with Smooth and IsProper of the structure morphism, for APIs stated on smooth proper varieties as such; a result that needs only smoothness or only properness takes [Smooth (X ↘ _)] or [IsProper (X ↘ _)] alone;
• the namespaces Variety and SmoothProperVariety name the concepts and hold their API, including SmoothProperVariety.CanonicalSheafData; they are not the names of types.

NumericalVarietyData n A N remains the intersection-theoretic quotient used by numerical arguments; the realization from a variety to it is separate data.

class AlgebraicGeometry.IsVariety (k : outParam (Type u)) [Field k] (X : Scheme) [X.Over (Spec (CommRingCat.of k))] extends AlgebraicGeometry.IsIntegral X, AlgebraicGeometry.LocallyOfFiniteType (X ↘ AlgebraicGeometry.Spec (CommRingCat.of k)) : Prop

X is a variety over k: integral, and locally of finite type over Spec k.

The base field is an outParam: a conclusion such as IsLocallyNoetherian X mentions no k, so instance search must be allowed to recover k from the IsVariety instance in scope rather than be given it. That is what the bundled a variety over k used to do through its type, and it is the only way an unbundled X : Scheme can carry the same instances.

• nonempty : Nonempty ↥X
• component_integral (U : X.Opens) [Nonempty ↥↑U] : IsDomain ↑(X.presheaf.obj (Opposite.op U))
• finiteType_appLE {U : (Spec (CommRingCat.of k)).Opens} : IsAffineOpen U → ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ (TopologicalSpace.Opens.map (X ↘ Spec (CommRingCat.of k)).base).obj U), (CommRingCat.Hom.hom (Scheme.Hom.appLE (X ↘ Spec (CommRingCat.of k)) U V e)).FiniteType

class AlgebraicGeometry.IsSmoothProperVariety (k : outParam (Type u)) [Field k] (X : Scheme) [X.Over (Spec (CommRingCat.of k))] extends AlgebraicGeometry.IsVariety k X, AlgebraicGeometry.Smooth (X ↘ AlgebraicGeometry.Spec (CommRingCat.of k)), AlgebraicGeometry.IsProper (X ↘ AlgebraicGeometry.Spec (CommRingCat.of k)) : Prop

X is a smooth proper variety over k: a variety whose structure morphism is smooth and proper. The conjunction is a class, as IsProper is, so that an API stated on smooth proper varieties carries one hypothesis; each constituent is recovered by instance search. The base is an outParam for the reason given at IsVariety.

• nonempty : Nonempty ↥X
• component_integral (U : X.Opens) [Nonempty ↥↑U] : IsDomain ↑(X.presheaf.obj (Opposite.op U))
• finiteType_appLE {U : (Spec (CommRingCat.of k)).Opens} : IsAffineOpen U → ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ (TopologicalSpace.Opens.map (X ↘ Spec (CommRingCat.of k)).base).obj U), (CommRingCat.Hom.hom (Scheme.Hom.appLE (X ↘ Spec (CommRingCat.of k)) U V e)).FiniteType
• smooth_appLE {U : (Spec (CommRingCat.of k)).Opens} : IsAffineOpen U → ∀ {V : X.Opens}, IsAffineOpen V → ∀ (e : V ≤ (TopologicalSpace.Opens.map (X ↘ Spec (CommRingCat.of k)).base).obj U), (CommRingCat.Hom.hom (Scheme.Hom.appLE (X ↘ Spec (CommRingCat.of k)) U V e)).Smooth
• isClosedImmersion_diagonal : IsClosedImmersion (CategoryTheory.Limits.pullback.diagonal (X ↘ Spec (CommRingCat.of k)))
• universally_isClosedMap : (topologically @IsClosedMap).universally (X ↘ Spec (CommRingCat.of k))

instance AlgebraicGeometry.Variety.isLocallyNoetherian {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] : IsLocallyNoetherian X

A variety over a field is locally noetherian: the base field is noetherian and the structure morphism is locally of finite type.

instance AlgebraicGeometry.Variety.isNoetherian_of_isProper {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] [IsProper (X ↘ Spec (CommRingCat.of k))] : IsNoetherian X

A proper variety over a field is Noetherian: finite type gives local Noetherianity and properness gives quasi-compactness over the compact point Spec k.

instance AlgebraicGeometry.Variety.isSeparated_of_isProper {k : Type u} [Field k] {X : Scheme} [X.Over (Spec (CommRingCat.of k))] [IsVariety k X] [IsProper (X ↘ Spec (CommRingCat.of k))] : X.IsSeparated

A proper variety over a field is separated as an absolute scheme.

The variety hypothesis contributes nothing to the proof, which uses only properness of the structure morphism. It is kept because its outParam base field is the only way instance search can recover k from the goal X.IsSeparated, which mentions no k; without it Lean reports no synthesization order for the instance.