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 (TODO).

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

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

    Instances
      source
      theorem AlgebraicGeometry.isProper_iff {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) :
      AlgebraicGeometry.IsProper f ↔ AlgebraicGeometry.IsSeparated f ∧ AlgebraicGeometry.UniversallyClosed f ∧ AlgebraicGeometry.LocallyOfFiniteType f
      source
      theorem AlgebraicGeometry.isProper_eq :
      @AlgebraicGeometry.IsProper = @AlgebraicGeometry.IsSeparated ⊓ @AlgebraicGeometry.UniversallyClosed ⊓ @AlgebraicGeometry.LocallyOfFiniteType
      source
      instance AlgebraicGeometry.IsProper.instRespectsIsoScheme :
      CategoryTheory.MorphismProperty.RespectsIso @AlgebraicGeometry.IsProper
      Equations
      source
      instance AlgebraicGeometry.IsProper.stableUnderComposition :
      CategoryTheory.MorphismProperty.IsStableUnderComposition @AlgebraicGeometry.IsProper
      Equations
      source
      instance AlgebraicGeometry.IsProper.instIsMultiplicativeScheme :
      CategoryTheory.MorphismProperty.IsMultiplicative @AlgebraicGeometry.IsProper
      Equations
      source
      @[instance 900]
      instance AlgebraicGeometry.IsProper.instOfIsClosedImmersion {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsClosedImmersion f] :
      AlgebraicGeometry.IsProper f
      Equations
      • ⋯ = ⋯
      source
      theorem AlgebraicGeometry.IsProper.stableUnderBaseChange :
      CategoryTheory.MorphismProperty.StableUnderBaseChange @AlgebraicGeometry.IsProper
      source
      instance AlgebraicGeometry.IsProper.instIsLocalAtTarget :
      AlgebraicGeometry.IsLocalAtTarget @AlgebraicGeometry.IsProper
      Equations