Documentation

Mathlib.AlgebraicGeometry.Morphisms.Separated

Separated morphisms #

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

Main definitions #

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

Instances
    source
    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✝
    source
    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.

    source
    theorem AlgebraicGeometry.IsSeparated.isSeparated_eq_diagonal_isClosedImmersion :
    @AlgebraicGeometry.IsSeparated = CategoryTheory.MorphismProperty.diagonal @AlgebraicGeometry.IsClosedImmersion
    source
    @[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
    • ⋯ = ⋯
    source
    instance AlgebraicGeometry.IsSeparated.instRespectsIsoScheme :
    CategoryTheory.MorphismProperty.RespectsIso @AlgebraicGeometry.IsSeparated
    Equations
    source
    @[instance 900]
    instance AlgebraicGeometry.IsSeparated.instQuasiSeparated {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsSeparated f] :
    AlgebraicGeometry.QuasiSeparated f
    Equations
    • ⋯ = ⋯
    source
    instance AlgebraicGeometry.IsSeparated.stableUnderComposition :
    CategoryTheory.MorphismProperty.IsStableUnderComposition @AlgebraicGeometry.IsSeparated
    Equations
    source
    instance AlgebraicGeometry.IsSeparated.instCompScheme {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.IsSeparated f] [AlgebraicGeometry.IsSeparated g] :
    AlgebraicGeometry.IsSeparated (CategoryTheory.CategoryStruct.comp f g)
    Equations
    • ⋯ = ⋯
    source
    instance AlgebraicGeometry.IsSeparated.instIsMultiplicativeScheme :
    CategoryTheory.MorphismProperty.IsMultiplicative @AlgebraicGeometry.IsSeparated
    Equations
    source
    theorem AlgebraicGeometry.IsSeparated.stableUnderBaseChange :
    CategoryTheory.MorphismProperty.StableUnderBaseChange @AlgebraicGeometry.IsSeparated
    source
    instance AlgebraicGeometry.IsSeparated.instIsLocalAtTarget :
    AlgebraicGeometry.IsLocalAtTarget @AlgebraicGeometry.IsSeparated
    Equations
    source
    instance AlgebraicGeometry.IsSeparated.instMap (R : CommRingCat) (S : CommRingCat) (f : R ⟶ S) :
    AlgebraicGeometry.IsSeparated (AlgebraicGeometry.Spec.map f)
    Equations
    • ⋯ = ⋯
    source
    theorem AlgebraicGeometry.IsSeparated.of_isAffineHom {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [h : AlgebraicGeometry.IsAffineHom f] :
    AlgebraicGeometry.IsSeparated f
    source
    instance AlgebraicGeometry.IsSeparated.instIsClosedImmersionMapDescScheme {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {S : AlgebraicGeometry.Scheme} {T : AlgebraicGeometry.Scheme} (f : X ⟶ S) (g : Y ⟶ S) (i : S ⟶ T) [AlgebraicGeometry.IsSeparated i] :
    AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Limits.pullback.mapDesc f g i)
    Equations
    • ⋯ = ⋯
    source
    instance AlgebraicGeometry.IsSeparated.instIsClosedImmersionLiftSchemeId {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.IsSeparated g] :
    AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Limits.pullback.lift (CategoryTheory.CategoryStruct.id X) f ⋯)

    Given f : X ⟶ Y and g : Y ⟶ Z such that g is separated, the induced map X ⟶ X ×[Z] Y is a closed immersion.

    Equations
    • ⋯ = ⋯
    source
    theorem AlgebraicGeometry.IsClosedImmersion.of_comp {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.IsClosedImmersion (CategoryTheory.CategoryStruct.comp f g)] [AlgebraicGeometry.IsSeparated g] :
    AlgebraicGeometry.IsClosedImmersion f
    source
    theorem AlgebraicGeometry.IsSeparated.of_comp {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.IsSeparated (CategoryTheory.CategoryStruct.comp f g)] :
    AlgebraicGeometry.IsSeparated f
    source
    theorem AlgebraicGeometry.IsSeparated.comp_iff {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [AlgebraicGeometry.IsSeparated g] :
    AlgebraicGeometry.IsSeparated (CategoryTheory.CategoryStruct.comp f g) ↔ AlgebraicGeometry.IsSeparated f
    source
    instance AlgebraicGeometry.isClosedImmersion_equalizer_ι_left {S : AlgebraicGeometry.Scheme} {X : CategoryTheory.Over S} {Y : CategoryTheory.Over S} [AlgebraicGeometry.IsSeparated Y.hom] (f : X ⟶ Y) (g : X ⟶ Y) :
    AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Limits.equalizer.ι f g).left
    Equations
    • ⋯ = ⋯
    source
    theorem AlgebraicGeometry.ext_of_isDominant_of_isSeparated {W : AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} {Z : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsReduced X] {f : X ⟶ Y} {g : X ⟶ Y} (s : Y ⟶ Z) [AlgebraicGeometry.IsSeparated s] (h : CategoryTheory.CategoryStruct.comp f s = CategoryTheory.CategoryStruct.comp g s) (ι : W ⟶ X) [AlgebraicGeometry.IsDominant ι] (hU : CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g) :
    f = g

    Suppose X is a reduced scheme and that f g : X ⟶ Y agree over some separated Y ⟶ Z. Then f = g if ι ≫ f = ι ≫ g for some dominant ι.

    source
    class AlgebraicGeometry.Scheme.IsSeparated (X : AlgebraicGeometry.Scheme) :
    Prop

    A scheme X is separated if it is separated over ⊤_ Scheme.

    Instances
      source
      theorem AlgebraicGeometry.Scheme.isSeparated_iff (X : AlgebraicGeometry.Scheme) :
      X.IsSeparated ↔ AlgebraicGeometry.IsSeparated (CategoryTheory.Limits.terminal.from X)
      source
      theorem AlgebraicGeometry.Scheme.IsSeparated.isSeparated_terminal_from {X : AlgebraicGeometry.Scheme} [self : X.IsSeparated] :
      AlgebraicGeometry.IsSeparated (CategoryTheory.Limits.terminal.from X)
      source
      theorem AlgebraicGeometry.Scheme.isSeparated_iff_isClosedImmersion_prod_lift {X : AlgebraicGeometry.Scheme} :
      X.IsSeparated ↔ AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X))
      source
      instance AlgebraicGeometry.Scheme.instIsClosedImmersionLiftIdOfIsSeparated {X : AlgebraicGeometry.Scheme} [X.IsSeparated] :
      AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X))
      Equations
      • ⋯ = ⋯
      source
      @[instance 900]
      instance AlgebraicGeometry.Scheme.instIsSeparatedOfIsAffine {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X] :
      X.IsSeparated
      Equations
      • ⋯ = ⋯
      source
      @[instance 900]
      instance AlgebraicGeometry.Scheme.instIsSeparatedOfIsSeparated {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [X.IsSeparated] :
      AlgebraicGeometry.IsSeparated f
      Equations
      • ⋯ = ⋯
      source
      instance AlgebraicGeometry.Scheme.instIsClosedImmersionιOfIsSeparated {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : X ⟶ Y) [Y.IsSeparated] :
      AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Limits.equalizer.ι f g)
      Equations
      • ⋯ = ⋯
      source
      instance AlgebraicGeometry.IsSeparated.hasAffineProperty :
      AlgebraicGeometry.HasAffineProperty @AlgebraicGeometry.IsSeparated fun (X x : AlgebraicGeometry.Scheme) (x_1 : X ⟶ x) (x : AlgebraicGeometry.IsAffine x) => X.IsSeparated
      Equations
      source
      theorem AlgebraicGeometry.ext_of_isDominant {W : AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme} {Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsReduced X] {f : X ⟶ Y} {g : X ⟶ Y} [Y.IsSeparated] (ι : W ⟶ X) [AlgebraicGeometry.IsDominant ι] (hU : CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g) :
      f = g

      Suppose f g : X ⟶ Y where X is a reduced scheme and Y is a separated scheme. Then f = g if ι ≫ f = ι ≫ g for some dominant ι.

      Also see ext_of_isDominant_of_isSeparated for the general version over arbitrary bases.