Subscheme associated to an ideal sheaf

We construct the subscheme associated to an ideal sheaf.

Main definition

• AlgebraicGeometry.Scheme.IdealSheafData.subscheme: The subscheme associated to an ideal sheaf.
• AlgebraicGeometry.Scheme.IdealSheafData.subschemeι: The inclusion from the subscheme.
• AlgebraicGeometry.Scheme.Hom.image: The scheme theoretical image of a morphism.
• AlgebraicGeometry.Scheme.kerAdjunction: The adjunction between taking kernels and taking the associated subscheme.

Note

Some instances are in Mathlib/AlgebraicGeometry/Morphisms/ClosedImmersion and Mathlib/AlgebraicGeometry/Morphisms/Separated because they need more API to prove.

def AlgebraicGeometry.Scheme.IdealSheafData.glueDataObj {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) : Scheme

Spec (𝒪ₓ(U)/I(U)), the object to be glued into the closed subscheme.

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjι {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) : I.glueDataObj U ⟶ ↑↑U

Spec (𝒪ₓ(U)/I(U)) ⟶ Spec (𝒪ₓ(U)) = U, the closed immersion into U.

instance AlgebraicGeometry.Scheme.IdealSheafData.instIsPreimmersionGlueDataObjι {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) : IsPreimmersion (I.glueDataObjι U)

theorem AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjι_ι {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) : CategoryTheory.CategoryStruct.comp (I.glueDataObjι U) (↑U).ι = CategoryTheory.CategoryStruct.comp (Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)))) (IsAffineOpen.fromSpec ⋯)

theorem AlgebraicGeometry.Scheme.IdealSheafData.ker_glueDataObjι_appTop {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) : RingHom.ker (CommRingCat.Hom.hom (Hom.appTop (I.glueDataObjι U))) = Ideal.comap (CommRingCat.Hom.hom (↑U).topIso.hom) (I.ideal U)

theorem AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) : Set.range ⇑(CategoryTheory.ConcreteCategory.hom (I.glueDataObjι U).base) = ⇑(CategoryTheory.ConcreteCategory.hom (IsAffineOpen.isoSpec ⋯).inv.base) '' PrimeSpectrum.zeroLocus ↑(I.ideal U)

theorem AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι_ι {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) : Set.range ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp (I.glueDataObjι U) (↑U).ι).base) = X.zeroLocus ↑(I.ideal U) ∩ ↑↑U

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjCarrierIso {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) : ↑(I.glueDataObj U).toPresheafedSpace ≅ TopCat.of ↑(X.zeroLocus ↑(I.ideal U) ∩ ↑↑U)

The underlying space of Spec (𝒪ₓ(U)/I(U)) is homeomorphic to its image in X.

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjMap {X : Scheme} (I : X.IdealSheafData) {U V : ↑X.affineOpens} (h : U ≤ V) : I.glueDataObj U ⟶ I.glueDataObj V

The open immersion Spec Γ(𝒪ₓ/I, U) ⟶ Spec Γ(𝒪ₓ/I, V) if U ≤ V.

theorem AlgebraicGeometry.Scheme.IdealSheafData.isLocalization_away {X : Scheme} (I : X.IdealSheafData) {U V : ↑X.affineOpens} (h : U ≤ V) (f : ↑(X.presheaf.obj (Opposite.op ↑V))) (hU : U = X.affineBasicOpen f) : IsLocalization.Away ((Ideal.Quotient.mk (I.ideal V)) f) (↑(X.presheaf.obj (Opposite.op ↑U)) ⧸ I.ideal U)

instance AlgebraicGeometry.Scheme.IdealSheafData.isOpenImmersion_glueDataObjMap {X : Scheme} (I : X.IdealSheafData) {V : ↑X.affineOpens} (f : ↑(X.presheaf.obj (Opposite.op ↑V))) : IsOpenImmersion (I.glueDataObjMap ⋯)

theorem AlgebraicGeometry.Scheme.IdealSheafData.opensRange_glueDataObjMap {X : Scheme} (I : X.IdealSheafData) {V : ↑X.affineOpens} (f : ↑(X.presheaf.obj (Opposite.op ↑V))) : Hom.opensRange (I.glueDataObjMap ⋯) = (TopologicalSpace.Opens.map (I.glueDataObjι V).base).obj ((TopologicalSpace.Opens.map (↑V).ι.base).obj (X.basicOpen f))

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjMap_glueDataObjι {X : Scheme} (I : X.IdealSheafData) {U V : ↑X.affineOpens} (h : U ≤ V) : CategoryTheory.CategoryStruct.comp (I.glueDataObjMap h) (I.glueDataObjι V) = CategoryTheory.CategoryStruct.comp (I.glueDataObjι U) (X.homOfLE h)

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjMap_glueDataObjι_assoc {X : Scheme} (I : X.IdealSheafData) {U V : ↑X.affineOpens} (h : U ≤ V) {Z : Scheme} (h✝ : ↑↑V ⟶ Z) : CategoryTheory.CategoryStruct.comp (I.glueDataObjMap h) (CategoryTheory.CategoryStruct.comp (I.glueDataObjι V) h✝) = CategoryTheory.CategoryStruct.comp (I.glueDataObjι U) (CategoryTheory.CategoryStruct.comp (X.homOfLE h) h✝)

theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_le_ker_glueDataObjι {X : Scheme} (I : X.IdealSheafData) (U V : ↑X.affineOpens) : I.ideal V ≤ RingHom.ker (CommRingCat.Hom.hom (CategoryTheory.CategoryStruct.comp (Hom.app (↑U).ι ↑V) (Hom.app (I.glueDataObjι U) ((TopologicalSpace.Opens.map (↑U).ι.base).obj ↑V))))

theorem AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι_ι_eq_support_inter {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) : Set.range ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp (I.glueDataObjι U) (↑U).ι).base) = ↑I.support ∩ ↑↑U

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.subscheme {X : Scheme} (I : X.IdealSheafData) : Scheme

The subscheme associated to an ideal sheaf.

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.subschemeι {X : Scheme} (I : X.IdealSheafData) : I.subscheme ⟶ X

The inclusion from the subscheme associated to an ideal sheaf.

theorem AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_apply {X : Scheme} (I : X.IdealSheafData) (x : ↥I.subscheme) : (CategoryTheory.ConcreteCategory.hom I.subschemeι.base) x = ↑x

instance AlgebraicGeometry.Scheme.IdealSheafData.instIsPreimmersionSubschemeι {X : Scheme} (I : X.IdealSheafData) : IsPreimmersion I.subschemeι

See AlgebraicGeometry.Morphisms.ClosedImmersion for the closed immersion version.

instance AlgebraicGeometry.Scheme.IdealSheafData.instQuasiCompactSubschemeι {X : Scheme} (I : X.IdealSheafData) : QuasiCompact I.subschemeι

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.range_subschemeι {X : Scheme} (I : X.IdealSheafData) : Set.range ⇑(CategoryTheory.ConcreteCategory.hom I.subschemeι.base) = ↑I.support

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.subschemeCover {X : Scheme} (I : X.IdealSheafData) : I.subscheme.AffineOpenCover

The subscheme associated to an ideal sheaf I is covered by Spec(Γ(X, U)/I(U)).

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.opensRange_subschemeCover_map {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) : Hom.opensRange (I.subschemeCover.map U) = (TopologicalSpace.Opens.map I.subschemeι.base).obj ↑U

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.subschemeCover_map_subschemeι {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) : CategoryTheory.CategoryStruct.comp (I.subschemeCover.map U) I.subschemeι = CategoryTheory.CategoryStruct.comp (I.glueDataObjι U) (↑U).ι

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.subschemeObjIso {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) : I.subscheme.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map I.subschemeι.base).obj ↑U)) ≅ CommRingCat.of (↑(X.presheaf.obj (Opposite.op ↑U)) ⧸ I.ideal U)

Γ(𝒪ₓ/I, U) ≅ 𝒪ₓ(U)/I(U).

theorem AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_app {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) : Hom.app I.subschemeι ↑U = CategoryTheory.CategoryStruct.comp (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U))) (I.subschemeObjIso U).inv

theorem AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_app_surjective {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) : Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (Hom.app I.subschemeι ↑U))

theorem AlgebraicGeometry.Scheme.IdealSheafData.ker_subschemeι_app {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) : RingHom.ker (CommRingCat.Hom.hom (Hom.app I.subschemeι ↑U)) = I.ideal U

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.ker_subschemeι {X : Scheme} (I : X.IdealSheafData) : Hom.ker I.subschemeι = I

instance AlgebraicGeometry.Scheme.IdealSheafData.instIsEmptyCarrierCarrierCommRingCatSubschemeTop {X : Scheme} : IsEmpty ↥⊤.subscheme

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom {X : Scheme} {I J : X.IdealSheafData} (h : I ≤ J) (U : ↑X.affineOpens) : J.glueDataObj U ⟶ I.glueDataObj U

Given I ≤ J, this is the map Spec(Γ(X, U)/J(U)) ⟶ Spec(Γ(X, U)/I(U)).

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom_ι {X : Scheme} {I J : X.IdealSheafData} (h : I ≤ J) (U : ↑X.affineOpens) : CategoryTheory.CategoryStruct.comp (glueDataObjHom h U) (I.glueDataObjι U) = J.glueDataObjι U

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom_ι_assoc {X : Scheme} {I J : X.IdealSheafData} (h : I ≤ J) (U : ↑X.affineOpens) {Z : Scheme} (h✝ : ↑↑U ⟶ Z) : CategoryTheory.CategoryStruct.comp (glueDataObjHom h U) (CategoryTheory.CategoryStruct.comp (I.glueDataObjι U) h✝) = CategoryTheory.CategoryStruct.comp (J.glueDataObjι U) h✝

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom_id {X : Scheme} {I : X.IdealSheafData} (U : ↑X.affineOpens) : glueDataObjHom ⋯ U = CategoryTheory.CategoryStruct.id (I.glueDataObj U)

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom_comp {X : Scheme} {I J K : X.IdealSheafData} (hIJ : I ≤ J) (hJK : J ≤ K) (U : ↑X.affineOpens) : CategoryTheory.CategoryStruct.comp (glueDataObjHom hJK U) (glueDataObjHom hIJ U) = glueDataObjHom ⋯ U

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom_comp_assoc {X : Scheme} {I J K : X.IdealSheafData} (hIJ : I ≤ J) (hJK : J ≤ K) (U : ↑X.affineOpens) {Z : Scheme} (h : I.glueDataObj U ⟶ Z) : CategoryTheory.CategoryStruct.comp (glueDataObjHom hJK U) (CategoryTheory.CategoryStruct.comp (glueDataObjHom hIJ U) h) = CategoryTheory.CategoryStruct.comp (glueDataObjHom ⋯ U) h

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.inclusion {X : Scheme} {I J : X.IdealSheafData} (h : I ≤ J) : J.subscheme ⟶ I.subscheme

The inclusion of ideal sheaf induces an inclusion of subschemes

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.subSchemeCover_map_inclusion {X : Scheme} {I J : X.IdealSheafData} (h : I ≤ J) (U : J.subschemeCover.J) : CategoryTheory.CategoryStruct.comp (J.subschemeCover.map U) (inclusion h) = CategoryTheory.CategoryStruct.comp (glueDataObjHom h U) (I.subschemeCover.map U)

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.subSchemeCover_map_inclusion_assoc {X : Scheme} {I J : X.IdealSheafData} (h : I ≤ J) (U : J.subschemeCover.J) {Z : Scheme} (h✝ : I.subscheme ⟶ Z) : CategoryTheory.CategoryStruct.comp (J.subschemeCover.map U) (CategoryTheory.CategoryStruct.comp (inclusion h) h✝) = CategoryTheory.CategoryStruct.comp (glueDataObjHom h U) (CategoryTheory.CategoryStruct.comp (I.subschemeCover.map U) h✝)

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.inclusion_subschemeι {X : Scheme} {I J : X.IdealSheafData} (h : I ≤ J) : CategoryTheory.CategoryStruct.comp (inclusion h) I.subschemeι = J.subschemeι

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.inclusion_subschemeι_assoc {X : Scheme} {I J : X.IdealSheafData} (h : I ≤ J) {Z : Scheme} (h✝ : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (inclusion h) (CategoryTheory.CategoryStruct.comp I.subschemeι h✝) = CategoryTheory.CategoryStruct.comp J.subschemeι h✝

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.inclusion_id {X : Scheme} (I : X.IdealSheafData) : inclusion ⋯ = CategoryTheory.CategoryStruct.id I.subscheme

theorem AlgebraicGeometry.Scheme.IdealSheafData.inclusion_id_assoc {X : Scheme} (I : X.IdealSheafData) {Z : Scheme} (h : I.subscheme ⟶ Z) : CategoryTheory.CategoryStruct.comp (inclusion ⋯) h = h

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.inclusion_comp {X : Scheme} {I J K : X.IdealSheafData} (h₁ : I ≤ J) (h₂ : J ≤ K) : CategoryTheory.CategoryStruct.comp (inclusion h₂) (inclusion h₁) = inclusion ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.inclusion_comp_assoc {X : Scheme} {I J K : X.IdealSheafData} (h₁ : I ≤ J) (h₂ : J ≤ K) {Z : Scheme} (h : I.subscheme ⟶ Z) : CategoryTheory.CategoryStruct.comp (inclusion h₂) (CategoryTheory.CategoryStruct.comp (inclusion h₁) h) = CategoryTheory.CategoryStruct.comp (inclusion ⋯) h

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.subschemeFunctor (Y : Scheme) : CategoryTheory.Functor Y.IdealSheafDataᵒᵖ (CategoryTheory.Over Y)

The functor taking an ideal sheaf to its associated subscheme.

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.subschemeFunctor_obj (Y : Scheme) (I : Y.IdealSheafDataᵒᵖ) : (subschemeFunctor Y).obj I = CategoryTheory.Over.mk (Opposite.unop I).subschemeι

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.subschemeFunctor_map (Y : Scheme) {I J : Y.IdealSheafDataᵒᵖ} (h : I ⟶ J) : (subschemeFunctor Y).map h = CategoryTheory.Over.homMk (inclusion ⋯) ⋯

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.Hom.image {X Y : Scheme} (f : X.Hom Y) : Scheme

The scheme theoretic image of a morphism.

@[reducible, inline]

abbrev AlgebraicGeometry.Scheme.Hom.imageι {X Y : Scheme} (f : X.Hom Y) : f.image ⟶ Y

The embedding from the scheme theoretic image to the codomain.

theorem AlgebraicGeometry.Scheme.ideal_ker_le_ker_ΓSpecIso_inv_comp {X Y : Scheme} (f : X.Hom Y) (U : ↑Y.affineOpens) : f.ker.ideal U ≤ RingHom.ker (CommRingCat.Hom.hom (CategoryTheory.CategoryStruct.comp (ΓSpecIso (Y.presheaf.obj (Opposite.op ↑U))).inv (Hom.appTop (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f (↑U).ι) (↑U).toSpecΓ))))

noncomputable def AlgebraicGeometry.Scheme.Hom.toImage {X Y : Scheme} (f : X.Hom Y) : X ⟶ f.image

The morphism from the domain to the scheme theoretic image.

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.toImage_imageι {X Y : Scheme} (f : X.Hom Y) : CategoryTheory.CategoryStruct.comp f.toImage f.imageι = f

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.toImage_imageι_assoc {X Y : Scheme} (f : X.Hom Y) {Z : Scheme} (h : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp f.toImage (CategoryTheory.CategoryStruct.comp f.imageι h) = CategoryTheory.CategoryStruct.comp f h

instance AlgebraicGeometry.Scheme.instIsDominantToImageOfQuasiCompact {X Y : Scheme} (f : X.Hom Y) [QuasiCompact f] : IsDominant f.toImage

instance AlgebraicGeometry.Scheme.instIsIsoSubschemeιBotIdealSheafData {X : Scheme} : CategoryTheory.IsIso ⊥.subschemeι

theorem AlgebraicGeometry.Scheme.Hom.toImage_app {X Y : Scheme} (f : X.Hom Y) (U : ↑Y.affineOpens) : app f.toImage ((TopologicalSpace.Opens.map f.imageι.base).obj ↑U) = CategoryTheory.CategoryStruct.comp (f.ker.subschemeObjIso U).hom (CommRingCat.ofHom (Ideal.Quotient.lift (f.ker.ideal U) (CommRingCat.Hom.hom (f.app ↑U)) ⋯))

theorem AlgebraicGeometry.Scheme.Hom.toImage_app_injective {X Y : Scheme} (f : X.Hom Y) (U : ↑Y.affineOpens) [QuasiCompact f] : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (app f.toImage ((TopologicalSpace.Opens.map f.imageι.base).obj ↑U)))

theorem AlgebraicGeometry.Scheme.Hom.stalkFunctor_toImage_injective {X Y : Scheme} (f : X.Hom Y) [QuasiCompact f] (x : ↥f.image) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom ((TopCat.Presheaf.stalkFunctor CommRingCat x).map f.toImage.c))

noncomputable def AlgebraicGeometry.Scheme.kerAdjunction (Y : Scheme) : (IdealSheafData.subschemeFunctor Y).rightOp ⊣ Y.kerFunctor

The adjunction between Y.IdealSheafData and (Over Y)ᵒᵖ given by taking kernels.

@[simp]

theorem AlgebraicGeometry.Scheme.kerAdjunction_unit_app (Y : Scheme) (I : Y.IdealSheafData) : Y.kerAdjunction.unit.app I = CategoryTheory.eqToHom ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.kerAdjunction_counit_app (Y : Scheme) (f : (CategoryTheory.Over Y)ᵒᵖ) : Y.kerAdjunction.counit.app f = (CategoryTheory.Over.homMk (Hom.toImage (Opposite.unop f).hom) ⋯).op

instance AlgebraicGeometry.Scheme.instFullOppositeIdealSheafDataOverSubschemeFunctor {Y : Scheme} : (IdealSheafData.subschemeFunctor Y).Full