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.

structure AlgebraicGeometry.IsProper {X Y : Scheme} (f : Quiver.Hom 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.Elem) (V : X.affineOpens.Elem) (e : LE.le V.val ((TopologicalSpace.Opens.map f.base).obj U.val)) : (CommRingCat.Hom.hom (Scheme.Hom.appLE f U.val V.val e)).FiniteType

Instances For

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

Iff (IsProper f) (And (IsSeparated f) (And (UniversallyClosed f) (LocallyOfFiniteType f)))

theorem AlgebraicGeometry.isProper_eq :

Eq (@IsProper) (Min.min (Min.min @IsSeparated @UniversallyClosed) @LocallyOfFiniteType)

theorem AlgebraicGeometry.IsProper.instRespectsIsoScheme :

CategoryTheory.MorphismProperty.RespectsIso @IsProper

theorem AlgebraicGeometry.IsProper.stableUnderComposition :

CategoryTheory.MorphismProperty.IsStableUnderComposition @IsProper

theorem AlgebraicGeometry.IsProper.instIsMultiplicativeScheme :

CategoryTheory.MorphismProperty.IsMultiplicative @IsProper

theorem AlgebraicGeometry.IsProper.instCompScheme {X Y Z : Scheme} (f : Quiver.Hom X Y) (g : Quiver.Hom Y Z) [IsProper f] [IsProper g] :

IsProper (CategoryTheory.CategoryStruct.comp f g)

theorem AlgebraicGeometry.IsProper.instOfIsFinite {X Y : Scheme} (f : Quiver.Hom X Y) [IsFinite f] :

theorem AlgebraicGeometry.IsProper.isStableUnderBaseChange :

CategoryTheory.MorphismProperty.IsStableUnderBaseChange @IsProper

theorem AlgebraicGeometry.IsProper.instIsLocalAtTarget :

IsLocalAtTarget @IsProper

theorem AlgebraicGeometry.IsFinite.eq_isProper_inf_isAffineHom :

Eq (@IsFinite) (Min.min @IsProper @IsAffineHom)

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

Iff (IsFinite f) (And (IsProper f) (IsAffineHom f))

theorem AlgebraicGeometry.instIsProperOfIsFinite {X Y : Scheme} (f : Quiver.Hom X Y) [IsFinite f] :

theorem AlgebraicGeometry.UniversallyClosed.of_comp_of_isSeparated {X Y Z : Scheme} (f : Quiver.Hom X Y) (g : Quiver.Hom 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 : Quiver.Hom X Y) (g : Quiver.Hom Y Z) [IsProper (CategoryTheory.CategoryStruct.comp f g)] [IsSeparated g] :

Stacks Tag 01W6 ((2))

theorem AlgebraicGeometry.isIntegral_appTop_of_universallyClosed {X Y : Scheme} (f : Quiver.Hom 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 : Quiver.Hom X (Spec (CommRingCat.of K))) [IsIntegral X] [UniversallyClosed f] :

IsField (X.presheaf.obj { unop := Top.top }).carrier

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 : Quiver.Hom 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.