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

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

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

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

theorem AlgebraicGeometry.isProper_iff {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : AlgebraicGeometry.IsProper f ↔ AlgebraicGeometry.IsSeparated f ∧ AlgebraicGeometry.UniversallyClosed f ∧ AlgebraicGeometry.LocallyOfFiniteType f

theorem AlgebraicGeometry.isProper_eq : @AlgebraicGeometry.IsProper = @AlgebraicGeometry.IsSeparated ⊓ @AlgebraicGeometry.UniversallyClosed ⊓ @AlgebraicGeometry.LocallyOfFiniteType

instance AlgebraicGeometry.IsProper.instRespectsIsoScheme : CategoryTheory.MorphismProperty.RespectsIso @AlgebraicGeometry.IsProper

Equations

• AlgebraicGeometry.IsProper.instRespectsIsoScheme = ⋯

instance AlgebraicGeometry.IsProper.stableUnderComposition : CategoryTheory.MorphismProperty.IsStableUnderComposition @AlgebraicGeometry.IsProper

Equations

• AlgebraicGeometry.IsProper.stableUnderComposition = ⋯

instance AlgebraicGeometry.IsProper.instIsMultiplicativeScheme : CategoryTheory.MorphismProperty.IsMultiplicative @AlgebraicGeometry.IsProper

Equations

• AlgebraicGeometry.IsProper.instIsMultiplicativeScheme = ⋯

@[instance 900]

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

Equations

• ⋯ = ⋯

instance AlgebraicGeometry.IsProper.isStableUnderBaseChange : CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.IsProper

Equations

• AlgebraicGeometry.IsProper.isStableUnderBaseChange = ⋯

instance AlgebraicGeometry.IsProper.instIsLocalAtTarget : AlgebraicGeometry.IsLocalAtTarget @AlgebraicGeometry.IsProper

Equations

• AlgebraicGeometry.IsProper.instIsLocalAtTarget = ⋯