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.

isClosedImmersion_diagonal : IsClosedImmersion (CategoryTheory.Limits.pullback.diagonal f)
universally_isClosedMap : (topologically @IsClosedMap).universally f
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

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.instIsZariskiLocalAtTarget :

IsZariskiLocalAtTarget @IsProper

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

IsProper (CategoryTheory.Limits.pullback.fst f g)

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

IsProper (CategoryTheory.Limits.pullback.snd f g)

instance AlgebraicGeometry.IsProper.instMorphismRestrict {X Y : Scheme} (f : X ⟶ Y) (V : Y.Opens) [IsProper f] :

IsProper (f ∣_ V)

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] :

instance AlgebraicGeometry.instHasOfPostcompPropertySchemeUniversallyClosedIsSeparated :

CategoryTheory.MorphismProperty.HasOfPostcompProperty @UniversallyClosed @IsSeparated

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))

instance AlgebraicGeometry.instHasOfPostcompPropertySchemeIsProperIsSeparated :

CategoryTheory.MorphismProperty.HasOfPostcompProperty @IsProper @IsSeparated

instance AlgebraicGeometry.instUniversallyClosedToImage {X Y : Scheme} (f : X ⟶ Y) [UniversallyClosed f] :

UniversallyClosed (Scheme.Hom.toImage f)

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

Stacks Tag 01W6 ((2))

theorem AlgebraicGeometry.IsProper.comp_iff {X Y Z : Scheme} {f : X ⟶ Y} {g : Y ⟶ Z} [IsProper g] :

IsProper (CategoryTheory.CategoryStruct.comp f g) ↔ IsProper f

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 ↧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 ↧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.