Documentation

Mathlib.AlgebraicGeometry.Morphisms.Proper

Proper morphisms #

A morphism of schemes is proper if it is separated, universally closed and (locally) of finite type. Note that we don't require quasi-compact, since this is implied by universally closed.

Main results #

AlgebraicGeometry.isField_of_universallyClosed: If X is an integral scheme that is universally closed over Spec K, then Γ(X, ⊤) is a field.
AlgebraicGeometry.finite_appTop_of_universallyClosed: If X is an integral scheme that is universally closed and of finite type over Spec K, then Γ(X, ⊤) is finite dimensional over K.

class AlgebraicGeometry.IsProper {X Y : Scheme} (f : X ⟶ Y) extends AlgebraicGeometry.IsSeparated f, AlgebraicGeometry.UniversallyClosed f, AlgebraicGeometry.LocallyOfFiniteType f :

A morphism is proper if it is separated, universally closed and locally of finite type.

diagonal_isClosedImmersion : IsClosedImmersion (CategoryTheory.Limits.pullback.diagonal f)
out : (topologically @IsClosedMap).universally f
finiteType_of_affine_subset (U : ↑Y.affineOpens) (V : ↑X.affineOpens) (e : ↑V ≤ (TopologicalSpace.Opens.map f.base).obj ↑U) : (CommRingCat.Hom.hom (Scheme.Hom.appLE f (↑U) (↑V) e)).FiniteType

Instances

theorem AlgebraicGeometry.isProper_iff {X Y : Scheme} (f : X ⟶ Y) :

IsProper f ↔ IsSeparated f ∧ UniversallyClosed f ∧ LocallyOfFiniteType f

theorem AlgebraicGeometry.isProper_eq :

@IsProper = @IsSeparated ⊓ @UniversallyClosed ⊓ @LocallyOfFiniteType

instance AlgebraicGeometry.IsProper.instRespectsIsoScheme :

CategoryTheory.MorphismProperty.RespectsIso @IsProper

instance AlgebraicGeometry.IsProper.stableUnderComposition :

CategoryTheory.MorphismProperty.IsStableUnderComposition @IsProper

instance AlgebraicGeometry.IsProper.instIsMultiplicativeScheme :

CategoryTheory.MorphismProperty.IsMultiplicative @IsProper

instance AlgebraicGeometry.IsProper.instCompScheme {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsProper f] [IsProper g] :

IsProper (CategoryTheory.CategoryStruct.comp f g)

@[instance 900]

instance AlgebraicGeometry.IsProper.instOfIsFinite {X Y : Scheme} (f : X ⟶ Y) [IsFinite f] :

instance AlgebraicGeometry.IsProper.isStableUnderBaseChange :

CategoryTheory.MorphismProperty.IsStableUnderBaseChange @IsProper

instance AlgebraicGeometry.IsProper.instIsLocalAtTarget :

IsLocalAtTarget @IsProper

theorem AlgebraicGeometry.IsFinite.eq_isProper_inf_isAffineHom :

@IsFinite = @IsProper ⊓ @IsAffineHom

theorem AlgebraicGeometry.IsFinite.iff_isProper_and_isAffineHom {X Y : Scheme} {f : X ⟶ Y} :

IsFinite f ↔ IsProper f ∧ IsAffineHom f

@[instance 100]

instance AlgebraicGeometry.instIsProperOfIsFinite {X Y : Scheme} (f : X ⟶ Y) [IsFinite f] :

theorem AlgebraicGeometry.UniversallyClosed.of_comp_of_isSeparated {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [UniversallyClosed (CategoryTheory.CategoryStruct.comp f g)] [IsSeparated g] :

UniversallyClosed f

Stacks Tag 01W6 ((1))

theorem AlgebraicGeometry.IsProper.of_comp_of_isSeparated {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsProper (CategoryTheory.CategoryStruct.comp f g)] [IsSeparated g] :

Stacks Tag 01W6 ((2))

theorem AlgebraicGeometry.isIntegral_appTop_of_universallyClosed {X Y : Scheme} (f : X ⟶ Y) [UniversallyClosed f] [IsAffine Y] :

(CommRingCat.Hom.hom (Scheme.Hom.appTop f)).IsIntegral

If f : X ⟶ Y is universally closed and Y is affine, then the map on global sections is integral.

theorem AlgebraicGeometry.isField_of_universallyClosed {X : Scheme} (K : Type u) [Field K] (f : X ⟶ Spec (CommRingCat.of K)) [IsIntegral X] [UniversallyClosed f] :

IsField ↑(X.presheaf.obj (Opposite.op ⊤))

If X is an integral scheme that is universally closed over Spec K, then Γ(X, ⊤) is a field.

theorem AlgebraicGeometry.finite_appTop_of_universallyClosed {X : Scheme} (K : Type u) [Field K] (f : X ⟶ Spec (CommRingCat.of K)) [IsIntegral X] [UniversallyClosed f] [LocallyOfFiniteType f] :

(CommRingCat.Hom.hom (Scheme.Hom.appTop f)).Finite

If X is an integral scheme that is universally closed and of finite type over Spec K, then Γ(X, ⊤) is a finite field extension over K.