Separated morphisms

A morphism of schemes is separated if its diagonal morphism is a closed immmersion.

TODO

• Show separated is stable under composition and base change (this is immediate if we show that closed immersions are stable under base change).
• Show separated is local at the target.
• Show affine morphisms are separated.

theorem AlgebraicGeometry.isSeparated_iff {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : AlgebraicGeometry.IsSeparated f ↔ autoParam (AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Limits.pullback.diagonal f)) _auto✝

class AlgebraicGeometry.IsSeparated {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : Prop

A morphism is separated if the diagonal map is a closed immersion.

• diagonal_isClosedImmersion : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Limits.pullback.diagonal f)

  A morphism is separated if the diagonal map is a closed immersion.

theorem AlgebraicGeometry.IsSeparated.diagonal_isClosedImmersion {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [self : AlgebraicGeometry.IsSeparated f] : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Limits.pullback.diagonal f)

A morphism is separated if the diagonal map is a closed immersion.

theorem AlgebraicGeometry.IsSeparated.isSeparated_eq_diagonal_isClosedImmersion : @AlgebraicGeometry.IsSeparated = CategoryTheory.MorphismProperty.diagonal @AlgebraicGeometry.IsClosedImmersion

@[instance 900]

instance AlgebraicGeometry.IsSeparated.isSeparated_of_mono {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [CategoryTheory.Mono f] : AlgebraicGeometry.IsSeparated f

Monomorphisms are separated.

Equations

• ⋯ = ⋯

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

Equations

• AlgebraicGeometry.IsSeparated.instRespectsIsoScheme = ⋯

@[instance 900]

instance AlgebraicGeometry.IsSeparated.instQuasiSeparated {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsSeparated f] : AlgebraicGeometry.QuasiSeparated f

Equations

• ⋯ = ⋯