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

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

Equations

• I.glueDataObj U = AlgebraicGeometry.Spec (CommRingCat.of (↑(X.presheaf.obj (Opposite.op ↑U)) ⧸ I.ideal U))

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.

Equations

• I.glueDataObjι U = CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk (I.ideal U)))) (AlgebraicGeometry.IsAffineOpen.isoSpec ⋯).inv

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 ⇑(I.glueDataObjι U) = ⇑(IsAffineOpen.isoSpec ⋯).inv '' PrimeSpectrum.zeroLocus ↑(I.ideal U)

theorem AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι_ι {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) : Set.range ⇑(CategoryTheory.CategoryStruct.comp (I.glueDataObjι U) (↑U).ι) = 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.

Equations

• I.glueDataObjCarrierIso U = TopCat.isoOfHomeo (⋯.toHomeomorph.trans (Homeomorph.setCongr ⋯))

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.

Equations

• I.glueDataObjMap h = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Ideal.quotientMap (I.ideal U) (CommRingCat.Hom.hom (X.presheaf.map (CategoryTheory.homOfLE h).op)) ⋯))

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))))

@[reducible, inline]

noncomputable abbrev AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjPullback {X : Scheme} (I : X.IdealSheafData) (U V : ↑X.affineOpens) : Scheme

(Implementation) The intersections Spec Γ(𝒪ₓ/I, U) ∩ V useful for gluing.

Equations

• I.glueDataObjPullback U V = CategoryTheory.Limits.pullback (I.glueDataObjι U) (X.homOfLE ⋯)

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.glueDataT {X : Scheme} (I : X.IdealSheafData) (U V : ↑X.affineOpens) : I.glueDataObjPullback U V ⟶ I.glueDataObjPullback V U

(Implementation) Transition maps in the glue data for 𝒪ₓ/I.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.glueDataT'Aux {X : Scheme} (I : X.IdealSheafData) (U V W U₀ : ↑X.affineOpens) (hU₀ : ↑U ⊓ ↑W ≤ ↑U₀) : CategoryTheory.Limits.pullback (CategoryTheory.Limits.pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) (CategoryTheory.Limits.pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) ⟶ I.glueDataObjPullback V U₀

(Implementation) t' in the glue data for 𝒪ₓ/I.

Equations

• One or more equations did not get rendered due to their size.

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

(Implementation) The glue data for 𝒪ₓ/I.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.glueData_t {X : Scheme} (I : X.IdealSheafData) (i j : ↑X.affineOpens) : I.glueData.t i j = I.glueDataT i j

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.glueData_U {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) : I.glueData.U U = I.glueDataObj U

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.glueData_J {X : Scheme} (I : X.IdealSheafData) : I.glueData.J = ↑X.affineOpens

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.glueData_f {X : Scheme} (I : X.IdealSheafData) (i j : ↑X.affineOpens) : I.glueData.f i j = CategoryTheory.Limits.pullback.fst (I.glueDataObjι (i, j).1) (X.homOfLE ⋯)

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.glueData_t' {X : Scheme} (I : X.IdealSheafData) (i j k : ↑X.affineOpens) : I.glueData.t' i j k = CategoryTheory.Limits.pullback.lift (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, k).2 ⋯) (I.glueDataT'Aux (i, j).1 (i, j).2 (i, k).2 (j, i).2 ⋯) ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.glueData_V {X : Scheme} (I : X.IdealSheafData) (ij : ↑X.affineOpens × ↑X.affineOpens) : I.glueData.V ij = I.glueDataObjPullback ij.1 ij.2

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.gluedTo {X : Scheme} (I : X.IdealSheafData) : I.glueData.glued ⟶ X

(Implementation) The map from Spec(𝒪ₓ/I) to X. See IdealSheafData.subschemeι instead.

Equations

• One or more equations did not get rendered due to their size.

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

theorem AlgebraicGeometry.Scheme.IdealSheafData.range_gluedTo {X : Scheme} (I : X.IdealSheafData) : Set.range ⇑I.gluedTo = ↑I.support

instance AlgebraicGeometry.Scheme.IdealSheafData.instIsPreimmersionGluedTo {X : Scheme} (I : X.IdealSheafData) : IsPreimmersion I.gluedTo

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.gluedHomeo {X : Scheme} (I : X.IdealSheafData) : ↥I.glueData.glued ≃ₜ ↥I.support

(Implementation) The underlying space of Spec(𝒪ₓ/I) is homeomorphic to the support of I.

Equations

• I.gluedHomeo = ⋯.toHomeomorph.trans (Homeomorph.setCongr ⋯)

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

The subscheme associated to an ideal sheaf.

Equations

• I.subscheme = I.glueData.glued.restrict ⋯

noncomputable def AlgebraicGeometry.Scheme.IdealSheafData.subschemeIso {X : Scheme} (I : X.IdealSheafData) : I.subscheme ≅ I.glueData.glued

(Implementation) The isomorphism between the subscheme and the glued scheme.

Equations

• I.subschemeIso = CategoryTheory.asIso (I.glueData.glued.ofRestrict ⋯)

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

The inclusion from the subscheme associated to an ideal sheaf.

Equations

• I.subschemeι = AlgebraicGeometry.Scheme.Hom.copyBase (CategoryTheory.CategoryStruct.comp I.subschemeIso.hom I.gluedTo) Subtype.val ⋯

theorem AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_apply {X : Scheme} (I : X.IdealSheafData) (x : ↥I.subscheme) : I.subschemeι 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 ⇑I.subschemeι = ↑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)).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.opensRange_subschemeCover_map {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) : Hom.opensRange (I.subschemeCover.f 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.f 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).

Equations

• One or more equations did not get rendered due to their size.

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

Equations

• AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom h U = AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Ideal.Quotient.factor ⋯))

@[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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.subSchemeCover_map_inclusion_assoc {X : Scheme} {I J : X.IdealSheafData} (h : I ≤ J) (U : J.subschemeCover.I₀) {Z : Scheme} (h✝ : I.subscheme ⟶ Z) : CategoryTheory.CategoryStruct.comp (J.subschemeCover.f U) (CategoryTheory.CategoryStruct.comp (inclusion h) h✝) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (glueDataObjHom h U) (I.subschemeCover.f 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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

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

@[simp]

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

@[reducible, inline]

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

The scheme-theoretic image of a morphism.

Equations

• AlgebraicGeometry.Scheme.Hom.image f = (AlgebraicGeometry.Scheme.Hom.ker f).subscheme

@[reducible, inline]

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

The embedding from the scheme-theoretic image to the codomain.

Equations

• AlgebraicGeometry.Scheme.Hom.imageι f = (AlgebraicGeometry.Scheme.Hom.ker f).subschemeι

theorem AlgebraicGeometry.Scheme.ideal_ker_le_ker_ΓSpecIso_inv_comp {X Y : Scheme} (f : X ⟶ Y) (U : ↑Y.affineOpens) : (Hom.ker f).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.toImageAux {X Y : Scheme} (f : X ⟶ Y) : X ⟶ image f

(Implementation): Use Hom.toImage instead which has better def-eqs.

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.Scheme.Hom.toImageAux_spec {X Y : Scheme} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (toImageAux f) (imageι f) = f

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

The morphism from the domain to the scheme-theoretic image.

Equations

• AlgebraicGeometry.Scheme.Hom.toImage f = AlgebraicGeometry.Scheme.Hom.copyBase (AlgebraicGeometry.Scheme.Hom.toImageAux f) (fun (x : ↥X) => ⟨f x, ⋯⟩) ⋯

@[simp]

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

@[simp]

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

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

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

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

theorem AlgebraicGeometry.Scheme.isIso_subschemeι_iff_eq_bot {X : Scheme} (I : X.IdealSheafData) : CategoryTheory.IsIso I.subschemeι ↔ I = ⊥

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

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

theorem AlgebraicGeometry.Scheme.Hom.stalkFunctor_toImage_injective {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] (x : ↥(image f)) : Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom ((TopCat.Presheaf.stalkFunctor CommRingCat x).map (toImage f).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.

Equations

• One or more equations did not get rendered due to their size.

@[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