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.
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.
Instances
@[instance 900]
instance
AlgebraicGeometry.IsSeparated.isSeparated_of_mono
{X Y : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
[CategoryTheory.Mono f]
:
Monomorphisms are separated.
@[instance 900]
instance
AlgebraicGeometry.IsSeparated.instQuasiSeparated
{X Y : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
[AlgebraicGeometry.IsSeparated f]
:
instance
AlgebraicGeometry.IsSeparated.instCompScheme
{X Y Z : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[AlgebraicGeometry.IsSeparated f]
[AlgebraicGeometry.IsSeparated g]
:
@[instance 100]
instance
AlgebraicGeometry.IsSeparated.of_isAffineHom
{X Y : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
[h : AlgebraicGeometry.IsAffineHom f]
:
instance
AlgebraicGeometry.IsSeparated.instIsClosedImmersionMapDescScheme
{X Y S T : AlgebraicGeometry.Scheme}
(f : X ⟶ S)
(g : Y ⟶ S)
(i : S ⟶ T)
[AlgebraicGeometry.IsSeparated i]
:
instance
AlgebraicGeometry.IsSeparated.instIsClosedImmersionLiftSchemeId
{X Y Z : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[AlgebraicGeometry.IsSeparated g]
:
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 : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
(𝒰 : Y.OpenCover)
(𝒱 : (i : 𝒰.J) → (CategoryTheory.Limits.pullback f (𝒰.map i)).OpenCover)
(hf : Function.Injective ⇑f.base)
:
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)
:
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)]
:
theorem
AlgebraicGeometry.isSeparated_of_injective
{X Y : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
(hf : Function.Injective ⇑f.base)
:
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]
:
theorem
AlgebraicGeometry.IsSeparated.of_comp
{X Y Z : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[AlgebraicGeometry.IsSeparated (CategoryTheory.CategoryStruct.comp f g)]
:
theorem
AlgebraicGeometry.IsSeparated.comp_iff
{X Y Z : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
(g : Y ⟶ Z)
[AlgebraicGeometry.IsSeparated g]
:
instance
AlgebraicGeometry.isClosedImmersion_equalizer_ι_left
{S : AlgebraicGeometry.Scheme}
{X Y : CategoryTheory.Over S}
[AlgebraicGeometry.IsSeparated Y.hom]
(f g : X ⟶ Y)
:
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 ι.
theorem
AlgebraicGeometry.ext_of_isDominant_of_isSeparated'
{X Y : AlgebraicGeometry.Scheme}
(S : AlgebraicGeometry.Scheme)
[X.Over S]
[Y.Over S]
[AlgebraicGeometry.IsReduced X]
[AlgebraicGeometry.IsSeparated (Y ↘ S)]
{f g : X ⟶ Y}
[AlgebraicGeometry.Scheme.Hom.IsOver f S]
[AlgebraicGeometry.Scheme.Hom.IsOver g S]
{W : AlgebraicGeometry.Scheme}
(ι : W ⟶ X)
[AlgebraicGeometry.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 ι.
A scheme X is separated if it is separated over ⊤_ Scheme.
- isSeparated_terminal_from : AlgebraicGeometry.IsSeparated (CategoryTheory.Limits.terminal.from X)
Instances
theorem
AlgebraicGeometry.Scheme.isSeparated_iff
(X : AlgebraicGeometry.Scheme)
:
X.IsSeparated ↔ AlgebraicGeometry.IsSeparated (CategoryTheory.Limits.terminal.from X)
@[instance 900]
instance
AlgebraicGeometry.Scheme.instIsSeparatedOfIsAffine
{X : AlgebraicGeometry.Scheme}
[AlgebraicGeometry.IsAffine X]
:
X.IsSeparated
@[instance 900]
instance
AlgebraicGeometry.Scheme.instIsSeparatedOfIsSeparated
{X Y : AlgebraicGeometry.Scheme}
(f : X ⟶ Y)
[X.IsSeparated]
:
instance
AlgebraicGeometry.Scheme.instIsClosedImmersionιOfIsSeparated
{X Y : AlgebraicGeometry.Scheme}
(f g : X ⟶ Y)
[Y.IsSeparated]
:
instance
AlgebraicGeometry.IsSeparated.hasAffineProperty :
AlgebraicGeometry.HasAffineProperty @AlgebraicGeometry.IsSeparated
fun (X x : AlgebraicGeometry.Scheme) (x_1 : X ⟶ x) (x : AlgebraicGeometry.IsAffine x) => X.IsSeparated
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.