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 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 Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) :
    AlgebraicGeometry.IsSeparated f ↔ autoParam (AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Limits.pullback.diagonal f)) _auto✝
    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 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 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 Y 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
    instance AlgebraicGeometry.IsSeparated.isStableUnderBaseChange :
    CategoryTheory.MorphismProperty.IsStableUnderBaseChange @AlgebraicGeometry.IsSeparated
    Equations
    source
    instance AlgebraicGeometry.IsSeparated.instIsLocalAtTarget :
    AlgebraicGeometry.IsLocalAtTarget @AlgebraicGeometry.IsSeparated
    Equations
    source
    instance AlgebraicGeometry.IsSeparated.instMap (R S : CommRingCat) (f : R ⟶ S) :
    AlgebraicGeometry.IsSeparated (AlgebraicGeometry.Spec.map f)
    Equations
    • ⋯ = ⋯
    source
    theorem AlgebraicGeometry.IsSeparated.of_isAffineHom {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [h : AlgebraicGeometry.IsAffineHom f] :
    AlgebraicGeometry.IsSeparated f
    source
    instance AlgebraicGeometry.IsSeparated.instIsClosedImmersionMapDescScheme {X Y S 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 Y 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.Scheme.Pullback.diagonalCoverDiagonalRange_eq_top_of_injective {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover) (𝒱 : (i : 𝒰.J) → (CategoryTheory.Limits.pullback f (𝒰.map i)).OpenCover) (hf : Function.Injective ⇑f.base) :
    AlgebraicGeometry.Scheme.Pullback.diagonalCoverDiagonalRange f 𝒰 𝒱 = ⊤
    source
    theorem AlgebraicGeometry.Scheme.Pullback.range_diagonal_subset_diagonalCoverDiagonalRange {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover) (𝒱 : (i : 𝒰.J) → (CategoryTheory.Limits.pullback f (𝒰.map i)).OpenCover) :
    Set.range ⇑(CategoryTheory.Limits.pullback.diagonal f).base ⊆ ↑(AlgebraicGeometry.Scheme.Pullback.diagonalCoverDiagonalRange f 𝒰 𝒱)
    source
    theorem AlgebraicGeometry.isClosedImmersion_diagonal_restrict_diagonalCoverDiagonalRange {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover) (𝒱 : (i : 𝒰.J) → (CategoryTheory.Limits.pullback f (𝒰.map i)).OpenCover) [∀ (i : 𝒰.J), AlgebraicGeometry.IsAffine (𝒰.obj i)] [∀ (i : 𝒰.J) (j : (𝒱 i).J), AlgebraicGeometry.IsAffine ((𝒱 i).obj j)] :
    AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Limits.pullback.diagonal f ∣_ AlgebraicGeometry.Scheme.Pullback.diagonalCoverDiagonalRange f 𝒰 𝒱)
    source
    theorem AlgebraicGeometry.isSeparated_of_injective {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (hf : Function.Injective ⇑f.base) :
    AlgebraicGeometry.IsSeparated f

    Stacks Tag 0DVA

    source
    theorem AlgebraicGeometry.IsClosedImmersion.of_comp {X Y 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 Y 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 Y 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 Y : CategoryTheory.Over S} [AlgebraicGeometry.IsSeparated Y.hom] (f g : X ⟶ Y) :
    AlgebraicGeometry.IsClosedImmersion (CategoryTheory.Limits.equalizer.ι f g).left

    Stacks Tag 01KM

    Equations
    • ⋯ = ⋯
    source
    theorem AlgebraicGeometry.ext_of_isDominant_of_isSeparated {W X Y Z : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsReduced X] {f 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_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 Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [X.IsSeparated] :
      AlgebraicGeometry.IsSeparated f
      Equations
      • ⋯ = ⋯
      source
      instance AlgebraicGeometry.Scheme.instIsClosedImmersionιOfIsSeparated {X Y : AlgebraicGeometry.Scheme} (f 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 X Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsReduced X] {f 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.