Separated morphisms

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

Main definitions

• AlgebraicGeometry.IsSeparated: The class of separated morphisms.
• AlgebraicGeometry.Scheme.IsSeparated: The class of separated schemes.
• AlgebraicGeometry.IsSeparated.hasAffineProperty: A morphism is separated iff the preimage of affine opens are separated schemes.

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

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

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

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

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

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

@[instance 900]

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

Monomorphisms are separated.

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

@[instance 900]

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

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

instance AlgebraicGeometry.IsSeparated.instCompScheme {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsSeparated f] [IsSeparated g] : IsSeparated (CategoryTheory.CategoryStruct.comp f g)

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

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

instance AlgebraicGeometry.IsSeparated.instIsLocalAtTarget : IsLocalAtTarget @IsSeparated

instance AlgebraicGeometry.IsSeparated.instMap (R S : CommRingCat) (f : R ⟶ S) : IsSeparated (Spec.map f)

@[instance 100]

instance AlgebraicGeometry.IsSeparated.of_isAffineHom {X Y : Scheme} (f : X ⟶ Y) [h : IsAffineHom f] : IsSeparated f

instance AlgebraicGeometry.IsSeparated.instIsClosedImmersionMapDescScheme {X Y S T : Scheme} (f : X ⟶ S) (g : Y ⟶ S) (i : S ⟶ T) [IsSeparated i] : IsClosedImmersion (CategoryTheory.Limits.pullback.mapDesc f g i)

instance AlgebraicGeometry.IsSeparated.instIsClosedImmersionLiftSchemeId {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsSeparated g] : 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.

theorem AlgebraicGeometry.Scheme.Pullback.diagonalCoverDiagonalRange_eq_top_of_injective {X Y : Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover) (𝒱 : (i : 𝒰.J) → (CategoryTheory.Limits.pullback f (𝒰.map i)).OpenCover) (hf : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f.base)) : diagonalCoverDiagonalRange f 𝒰 𝒱 = ⊤

theorem AlgebraicGeometry.Scheme.Pullback.range_diagonal_subset_diagonalCoverDiagonalRange {X Y : Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover) (𝒱 : (i : 𝒰.J) → (CategoryTheory.Limits.pullback f (𝒰.map i)).OpenCover) : Set.range ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.diagonal f).base) ⊆ ↑(diagonalCoverDiagonalRange f 𝒰 𝒱)

theorem AlgebraicGeometry.isClosedImmersion_diagonal_restrict_diagonalCoverDiagonalRange {X Y : Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover) (𝒱 : (i : 𝒰.J) → (CategoryTheory.Limits.pullback f (𝒰.map i)).OpenCover) [∀ (i : 𝒰.J), IsAffine (𝒰.obj i)] [∀ (i : 𝒰.J) (j : (𝒱 i).J), IsAffine ((𝒱 i).obj j)] : IsClosedImmersion (CategoryTheory.Limits.pullback.diagonal f ∣_ Scheme.Pullback.diagonalCoverDiagonalRange f 𝒰 𝒱)

theorem AlgebraicGeometry.isSeparated_of_injective {X Y : Scheme} (f : X ⟶ Y) (hf : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f.base)) : IsSeparated f

Stacks Tag 0DVA

theorem AlgebraicGeometry.IsClosedImmersion.of_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsClosedImmersion (CategoryTheory.CategoryStruct.comp f g)] [IsSeparated g] : IsClosedImmersion f

instance AlgebraicGeometry.instIsClosedImmersionInclusion {X : Scheme} {I J : X.IdealSheafData} (h : I ≤ J) : IsClosedImmersion (Scheme.IdealSheafData.inclusion h)

theorem AlgebraicGeometry.IsSeparated.of_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsSeparated (CategoryTheory.CategoryStruct.comp f g)] : IsSeparated f

theorem AlgebraicGeometry.IsSeparated.comp_iff {X Y Z : Scheme} {f : X ⟶ Y} {g : Y ⟶ Z} [IsSeparated g] : IsSeparated (CategoryTheory.CategoryStruct.comp f g) ↔ IsSeparated f

theorem AlgebraicGeometry.IsAffineHom.of_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [IsAffineHom (CategoryTheory.CategoryStruct.comp f g)] [IsSeparated g] : IsAffineHom f

theorem AlgebraicGeometry.IsAffineHom.comp_iff {X Y Z : Scheme} {f : X ⟶ Y} {g : Y ⟶ Z} [IsAffineHom g] : IsAffineHom (CategoryTheory.CategoryStruct.comp f g) ↔ IsAffineHom f

instance AlgebraicGeometry.isClosedImmersion_equalizer_ι_left {S : Scheme} {X Y : CategoryTheory.Over S} [IsSeparated Y.hom] (f g : X ⟶ Y) : IsClosedImmersion (CategoryTheory.Limits.equalizer.ι f g).left

Stacks Tag 01KM

theorem AlgebraicGeometry.ext_of_isDominant_of_isSeparated {W X Y Z : Scheme} [IsReduced X] {f g : X ⟶ Y} (s : Y ⟶ Z) [IsSeparated s] (h : CategoryTheory.CategoryStruct.comp f s = CategoryTheory.CategoryStruct.comp g s) (ι : W ⟶ X) [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 ι.

theorem AlgebraicGeometry.ext_of_isDominant_of_isSeparated' {X Y : Scheme} (S : Scheme) [X.Over S] [Y.Over S] [IsReduced X] [IsSeparated (Y ↘ S)] {f g : X ⟶ Y} [Scheme.Hom.IsOver f S] [Scheme.Hom.IsOver g S] {W : Scheme} (ι : W ⟶ X) [IsDominant ι] (hU : CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g) : f = g

Suppose X is a reduced S-scheme and Y is a separated S-scheme. For any S-morphisms f g : X ⟶ Y, f = g if ι ≫ f = ι ≫ g for some dominant ι.

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

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

• isSeparated_terminal_from : IsSeparated (CategoryTheory.Limits.terminal.from X)

theorem AlgebraicGeometry.Scheme.isSeparated_iff (X : Scheme) : X.IsSeparated ↔ IsSeparated (CategoryTheory.Limits.terminal.from X)

theorem AlgebraicGeometry.Scheme.isSeparated_iff_isClosedImmersion_prod_lift {X : Scheme} : X.IsSeparated ↔ IsClosedImmersion (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X))

instance AlgebraicGeometry.Scheme.instIsClosedImmersionLiftIdOfIsSeparated {X : Scheme} [X.IsSeparated] : IsClosedImmersion (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X))

@[instance 900]

instance AlgebraicGeometry.Scheme.instIsSeparatedOfIsAffine {X : Scheme} [IsAffine X] : X.IsSeparated

@[instance 900]

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

instance AlgebraicGeometry.Scheme.instIsClosedImmersionιOfIsSeparated {X Y : Scheme} (f g : X ⟶ Y) [Y.IsSeparated] : IsClosedImmersion (CategoryTheory.Limits.equalizer.ι f g)

instance AlgebraicGeometry.IsSeparated.hasAffineProperty : HasAffineProperty @IsSeparated fun (X x : Scheme) (x_1 : X ⟶ x) (x : IsAffine x) => X.IsSeparated

theorem AlgebraicGeometry.ext_of_isDominant {W X Y : Scheme} [IsReduced X] {f g : X ⟶ Y} [Y.IsSeparated] (ι : W ⟶ X) [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.