Ideal sheaves on schemes

We define ideal sheaves of schemes and provide various constructors for it.

Main definition

• AlgebraicGeometry.Scheme.IdealSheafData: A structure that contains the data to uniquely define an ideal sheaf, consisting of
  1. an ideal I(U) ≤ Γ(X, U) for every affine open U
  2. a proof that I(D(f)) = I(U)_f for every affine open U and every section f : Γ(X, U).
• AlgebraicGeometry.Scheme.IdealSheafData.ofIdeals: The largest ideal sheaf contained in a family of ideals.
• AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine: Over affine schemes, ideal sheaves are in bijection with ideals of the global sections.
• AlgebraicGeometry.Scheme.IdealSheafData.support: The support of an ideal sheaf.
• AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal: The vanishing ideal of a set.
• AlgebraicGeometry.Scheme.Hom.ker: The kernel of a morphism.

Main results

• AlgebraicGeometry.Scheme.IdealSheafData.gc: support and vanishingIdeal forms a galois connection.
• AlgebraicGeometry.Scheme.Hom.support_ker: The support of a kernel of a quasi-compact morphism is the closure of the range.

Implementation detail

Ideal sheaves are not yet defined in this file as actual subsheaves of 𝒪ₓ. Instead, for the ease of development and application, we define the structure IdealSheafData containing all necessary data to uniquely define an ideal sheaf. This should be refectored as a constructor for ideal sheaves once they are introduced into mathlib.

structure AlgebraicGeometry.Scheme.IdealSheafData (X : Scheme) : Type u

A structure that contains the data to uniquely define an ideal sheaf, consisting of

1. an ideal I(U) ≤ Γ(X, U) for every affine open U
2. a proof that I(D(f)) = I(U)_f for every affine open U and every section f : Γ(X, U).

• ideal (U : ↑X.affineOpens) : Ideal ↑(X.presheaf.obj (Opposite.op ↑U))

  The component of an ideal sheaf at an affine open.

• map_ideal_basicOpen (U : ↑X.affineOpens) (f : ↑(X.presheaf.obj (Opposite.op ↑U))) : Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (CategoryTheory.homOfLE ⋯).op)) (self.ideal U) = self.ideal (X.affineBasicOpen f)

  Also see AlgebraicGeometry.Scheme.IdealSheafData.map_ideal

theorem AlgebraicGeometry.Scheme.IdealSheafData.ext {X : Scheme} {x y : X.IdealSheafData} (ideal : x.ideal = y.ideal) : x = y

instance AlgebraicGeometry.Scheme.IdealSheafData.instPartialOrder {X : Scheme} : PartialOrder X.IdealSheafData

Equations

• AlgebraicGeometry.Scheme.IdealSheafData.instPartialOrder = PartialOrder.lift AlgebraicGeometry.Scheme.IdealSheafData.ideal ⋯

theorem AlgebraicGeometry.Scheme.IdealSheafData.le_def {X : Scheme} {I J : X.IdealSheafData} : I ≤ J ↔ ∀ (U : ↑X.affineOpens), I.ideal U ≤ J.ideal U

instance AlgebraicGeometry.Scheme.IdealSheafData.instCompleteSemilatticeSup {X : Scheme} : CompleteSemilatticeSup X.IdealSheafData

Equations

• AlgebraicGeometry.Scheme.IdealSheafData.instCompleteSemilatticeSup = CompleteSemilatticeSup.mk ⋯ ⋯

def AlgebraicGeometry.Scheme.IdealSheafData.ofIdeals {X : Scheme} (I : (U : ↑X.affineOpens) → Ideal ↑(X.presheaf.obj (Opposite.op ↑U))) : X.IdealSheafData

The largest ideal sheaf contained in a family of ideals.

Equations

• AlgebraicGeometry.Scheme.IdealSheafData.ofIdeals I = sSup {J : X.IdealSheafData | J.ideal ≤ I}

theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_ofIdeals_le {X : Scheme} (I : (U : ↑X.affineOpens) → Ideal ↑(X.presheaf.obj (Opposite.op ↑U))) : (ofIdeals I).ideal ≤ I

def AlgebraicGeometry.Scheme.IdealSheafData.gci {X : Scheme} : GaloisCoinsertion ideal ofIdeals

The galois coinsertion between ideal sheaves and arbitrary families of ideals.

Equations

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

theorem AlgebraicGeometry.Scheme.IdealSheafData.strictMono_ideal {X : Scheme} : StrictMono ideal

theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_mono {X : Scheme} : Monotone ideal

theorem AlgebraicGeometry.Scheme.IdealSheafData.ofIdeals_mono {X : Scheme} : Monotone ofIdeals

theorem AlgebraicGeometry.Scheme.IdealSheafData.ofIdeals_ideal {X : Scheme} (I : X.IdealSheafData) : ofIdeals I.ideal = I

theorem AlgebraicGeometry.Scheme.IdealSheafData.le_ofIdeals_iff {X : Scheme} {I : X.IdealSheafData} {J : (U : ↑X.affineOpens) → Ideal ↑(X.presheaf.obj (Opposite.op ↑U))} : I ≤ ofIdeals J ↔ I.ideal ≤ J

instance AlgebraicGeometry.Scheme.IdealSheafData.instCompleteLattice {X : Scheme} : CompleteLattice X.IdealSheafData

Equations

• AlgebraicGeometry.Scheme.IdealSheafData.instCompleteLattice = CompleteLattice.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_top {X : Scheme} : ⊤.ideal = ⊤

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_bot {X : Scheme} : ⊥.ideal = ⊥

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_sup {X : Scheme} {I J : X.IdealSheafData} : (I ⊔ J).ideal = I.ideal ⊔ J.ideal

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_sSup {X : Scheme} {I : Set X.IdealSheafData} : (sSup I).ideal = sSup (ideal '' I)

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_iSup {X : Scheme} {ι : Type u_1} {I : ι → X.IdealSheafData} : (iSup I).ideal = ⨆ (i : ι), (I i).ideal

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_inf {X : Scheme} {I J : X.IdealSheafData} : (I ⊓ J).ideal = I.ideal ⊓ J.ideal

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_biInf {X : Scheme} {ι : Type u_1} (I : ι → X.IdealSheafData) {s : Set ι} (hs : s.Finite) : (⨅ i ∈ s, I i).ideal = ⨅ i ∈ s, (I i).ideal

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_iInf {X : Scheme} {ι : Type u_1} (I : ι → X.IdealSheafData) [Finite ι] : (⨅ (i : ι), I i).ideal = ⨅ (i : ι), (I i).ideal

theorem AlgebraicGeometry.Scheme.IdealSheafData.map_ideal {X : Scheme} (I : X.IdealSheafData) {U V : ↑X.affineOpens} (h : U ≤ V) : Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (CategoryTheory.homOfLE h).op)) (I.ideal V) = I.ideal U

theorem AlgebraicGeometry.Scheme.IdealSheafData.map_ideal' {X : Scheme} (I : X.IdealSheafData) {U V : ↑X.affineOpens} (h : Opposite.op ↑V ⟶ Opposite.op ↑U) : Ideal.map (CommRingCat.Hom.hom (X.presheaf.map h)) (I.ideal V) = I.ideal U

A form of map_ideal that is easier to rewrite with.

theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_le_comap_ideal {X : Scheme} (I : X.IdealSheafData) {U V : ↑X.affineOpens} (h : U ≤ V) : I.ideal V ≤ Ideal.comap (CommRingCat.Hom.hom (X.presheaf.map (CategoryTheory.homOfLE h).op)) (I.ideal U)

def AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTop {X : Scheme} (I : Ideal ↑(X.presheaf.obj (Opposite.op ⊤))) : X.IdealSheafData

The ideal sheaf induced by an ideal of the global sections.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.ofIdealTop_ideal {X : Scheme} (I : Ideal ↑(X.presheaf.obj (Opposite.op ⊤))) (U : ↑X.affineOpens) : (ofIdealTop I).ideal U = Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (CategoryTheory.homOfLE ⋯).op)) I

theorem AlgebraicGeometry.Scheme.IdealSheafData.le_of_isAffine {X : Scheme} [IsAffine X] {I J : X.IdealSheafData} (H : I.ideal ⟨⊤, ⋯⟩ ≤ J.ideal ⟨⊤, ⋯⟩) : I ≤ J

theorem AlgebraicGeometry.Scheme.IdealSheafData.ext_of_isAffine {X : Scheme} [IsAffine X] {I J : X.IdealSheafData} (H : I.ideal ⟨⊤, ⋯⟩ = J.ideal ⟨⊤, ⋯⟩) : I = J

def AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine {X : Scheme} [IsAffine X] : X.IdealSheafData ≃ Ideal ↑(X.presheaf.obj (Opposite.op ⊤))

Over affine schemes, ideal sheaves are in bijection with ideals of the global sections.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine_symm_apply {X : Scheme} [IsAffine X] (I : Ideal ↑(X.presheaf.obj (Opposite.op ⊤))) : equivOfIsAffine.symm I = ofIdealTop I

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine_apply {X : Scheme} [IsAffine X] (x✝ : X.IdealSheafData) : equivOfIsAffine x✝ = x✝.ideal ⟨⊤, ⋯⟩

def AlgebraicGeometry.Scheme.IdealSheafData.support {X : Scheme} (I : X.IdealSheafData) : Set ↑↑X.toPresheafedSpace

The support of an ideal sheaf. Also see IdealSheafData.mem_support_iff_of_mem.

Equations

• I.support = ⋂ (U : ↑X.affineOpens), X.zeroLocus ↑(I.ideal U)

theorem AlgebraicGeometry.Scheme.IdealSheafData.mem_support_iff {X : Scheme} {I : X.IdealSheafData} {x : ↑↑X.toPresheafedSpace} : x ∈ I.support ↔ ∀ (U : ↑X.affineOpens), x ∈ X.zeroLocus ↑(I.ideal U)

theorem AlgebraicGeometry.Scheme.IdealSheafData.support_subset_zeroLocus {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) : I.support ⊆ X.zeroLocus ↑(I.ideal U)

theorem AlgebraicGeometry.Scheme.IdealSheafData.zeroLocus_inter_subset_support {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) : X.zeroLocus ↑(I.ideal U) ∩ ↑↑U ⊆ I.support

theorem AlgebraicGeometry.Scheme.IdealSheafData.mem_support_iff_of_mem {X : Scheme} {I : X.IdealSheafData} {x : ↑↑X.toPresheafedSpace} {U : ↑X.affineOpens} (hxU : x ∈ ↑U) : x ∈ I.support ↔ x ∈ X.zeroLocus ↑(I.ideal U)

theorem AlgebraicGeometry.Scheme.IdealSheafData.support_inter {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) : I.support ∩ ↑↑U = X.zeroLocus ↑(I.ideal U) ∩ ↑↑U

theorem AlgebraicGeometry.Scheme.IdealSheafData.isClosed_support {X : Scheme} (I : X.IdealSheafData) : IsClosed I.support

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.support_top {X : Scheme} : ⊤.support = ∅

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.support_bot {X : Scheme} : ⊥.support = Set.univ

theorem AlgebraicGeometry.Scheme.IdealSheafData.support_antitone {X : Scheme} : Antitone support

theorem AlgebraicGeometry.Scheme.IdealSheafData.support_ofIdealTop {X : Scheme} (I : Ideal ↑(X.presheaf.obj (Opposite.op ⊤))) : (ofIdealTop I).support = X.zeroLocus ↑I

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.support_eq_empty_iff {X : Scheme} (I : X.IdealSheafData) : I.support = ∅ ↔ I = ⊤

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

The radical of a ideal sheaf.

Equations

• I.radical = { ideal := fun (U : ↑X.affineOpens) => (I.ideal U).radical, map_ideal_basicOpen := ⋯ }

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.radical_ideal {X : Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens) : I.radical.ideal U = (I.ideal U).radical

def AlgebraicGeometry.Scheme.nilradical (X : Scheme) : X.IdealSheafData

The nilradical of a scheme.

Equations

• X.nilradical = ⊥.radical

theorem AlgebraicGeometry.Scheme.IdealSheafData.le_radical {X : Scheme} (I : X.IdealSheafData) : I ≤ I.radical

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.radical_top {X : Scheme} : ⊤.radical = ⊤

theorem AlgebraicGeometry.Scheme.IdealSheafData.radical_bot {X : Scheme} : ⊥.radical = X.nilradical

theorem AlgebraicGeometry.Scheme.IdealSheafData.radical_sup {X : Scheme} {I J : X.IdealSheafData} : (I ⊔ J).radical = (I.radical ⊔ J.radical).radical

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.radical_inf {X : Scheme} {I J : X.IdealSheafData} : (I ⊓ J).radical = I.radical ⊓ J.radical

def AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal {X : Scheme} (Z : Set ↑↑X.toPresheafedSpace) : X.IdealSheafData

The vanishing ideal sheaf of a set, which is the largest ideal sheaf whose support contains a subset. When the set Z is closed, the reduced induced scheme structure is the quotient of this ideal.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_ideal {X : Scheme} (Z : Set ↑↑X.toPresheafedSpace) (U : ↑X.affineOpens) : (vanishingIdeal Z).ideal U = PrimeSpectrum.vanishingIdeal (⇑(CategoryTheory.ConcreteCategory.hom (IsAffineOpen.fromSpec ⋯).base) ⁻¹' Z)

theorem AlgebraicGeometry.Scheme.IdealSheafData.subset_support_iff_le_vanishingIdeal {X : Scheme} {I : X.IdealSheafData} {Z : Set ↑↑X.toPresheafedSpace} : Z ⊆ I.support ↔ I ≤ vanishingIdeal Z

theorem AlgebraicGeometry.Scheme.IdealSheafData.gc {X : Scheme} : GaloisConnection (fun (x : X.IdealSheafData) => x.support) fun (x : (Set ↑↑X.toPresheafedSpace)ᵒᵈ) => vanishingIdeal x

support and vanishingIdeal forms a galois connection. This is the global version of PrimeSpectrum.gc.

theorem AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_antimono {X : Scheme} {S T : Set ↑↑X.toPresheafedSpace} (h : S ⊆ T) : vanishingIdeal T ≤ vanishingIdeal S

theorem AlgebraicGeometry.Scheme.IdealSheafData.support_vanishingIdeal {X : Scheme} {Z : Set ↑↑X.toPresheafedSpace} : (vanishingIdeal Z).support = closure Z

theorem AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_support {X : Scheme} {I : X.IdealSheafData} : vanishingIdeal I.support = I.radical

def AlgebraicGeometry.Scheme.Hom.ker {X Y : Scheme} (f : X.Hom Y) : Y.IdealSheafData

The kernel of a morphism, defined as the largest (quasi-coherent) ideal sheaf contained in the component-wise kernel. This is usually only well-behaved when f is quasi-compact.

Equations

• f.ker = AlgebraicGeometry.Scheme.IdealSheafData.ofIdeals fun (U : ↑Y.affineOpens) => RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.ker_apply {X Y : Scheme} (f : X.Hom Y) [QuasiCompact f] (U : ↑Y.affineOpens) : f.ker.ideal U = RingHom.ker (CommRingCat.Hom.hom (f.app ↑U))

theorem AlgebraicGeometry.Scheme.Hom.le_ker_comp {X Y Z : Scheme} (f : X ⟶ Y) (g : Y.Hom Z) : g.ker ≤ ker (CategoryTheory.CategoryStruct.comp f g)

theorem AlgebraicGeometry.Scheme.ker_eq_top_of_isEmpty {X Y : Scheme} (f : X.Hom Y) [IsEmpty ↑↑X.toPresheafedSpace] : f.ker = ⊤

theorem AlgebraicGeometry.Scheme.ker_of_isAffine {X Y : Scheme} (f : X ⟶ Y) [IsAffine Y] : Hom.ker f = IdealSheafData.ofIdealTop (RingHom.ker (CommRingCat.Hom.hom (Hom.appTop f)))

theorem AlgebraicGeometry.Scheme.Hom.range_subset_ker_support {X Y : Scheme} (f : X.Hom Y) : Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base) ⊆ f.ker.support

theorem AlgebraicGeometry.Scheme.Hom.iInf_ker_openCover_map_comp_apply {X Y : Scheme} (f : X.Hom Y) [QuasiCompact f] (𝒰 : X.OpenCover) (U : ↑Y.affineOpens) : ⨅ (i : 𝒰.J), (ker (CategoryTheory.CategoryStruct.comp (𝒰.map i) f)).ideal U = f.ker.ideal U

theorem AlgebraicGeometry.Scheme.Hom.iInf_ker_openCover_map_comp {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] (𝒰 : X.OpenCover) : ⨅ (i : 𝒰.J), ker (CategoryTheory.CategoryStruct.comp (𝒰.map i) f) = ker f

theorem AlgebraicGeometry.Scheme.Hom.iUnion_support_ker_openCover_map_comp {X Y : Scheme} (f : X.Hom Y) [QuasiCompact f] (𝒰 : X.OpenCover) [Finite 𝒰.J] : ⋃ (i : 𝒰.J), (ker (CategoryTheory.CategoryStruct.comp (𝒰.map i) f)).support = f.ker.support

theorem AlgebraicGeometry.Scheme.ker_morphismRestrict_ideal {X Y : Scheme} (f : X.Hom Y) [QuasiCompact f] (U : Y.Opens) (V : ↑(↑U).affineOpens) : (Hom.ker (f ∣_ U)).ideal V = f.ker.ideal ⟨(Hom.opensFunctor U.ι).obj ↑V, ⋯⟩

theorem AlgebraicGeometry.Scheme.ker_ideal_of_isPullback_of_isOpenImmersion {X Y U V : Scheme} (f : X ⟶ Y) (f' : U ⟶ V) (iU : U ⟶ X) (iV : V ⟶ Y) [IsOpenImmersion iV] [QuasiCompact f] (H : CategoryTheory.IsPullback f' iU iV f) (W : ↑V.affineOpens) : (Hom.ker f').ideal W = Ideal.comap (CommRingCat.Hom.hom (Hom.appIso iV ↑W).inv) ((Hom.ker f).ideal ⟨(Hom.opensFunctor iV).obj ↑W, ⋯⟩)

theorem AlgebraicGeometry.Scheme.Hom.support_ker {X Y : Scheme} (f : X.Hom Y) [QuasiCompact f] : f.ker.support = closure (Set.range ⇑(CategoryTheory.ConcreteCategory.hom f.base))

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 ⇑(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.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

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.

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.glueDataT_snd {X : Scheme} (I : X.IdealSheafData) (U V : ↑X.affineOpens) : CategoryTheory.CategoryStruct.comp (I.glueDataT U V) (CategoryTheory.Limits.pullback.snd (I.glueDataObjι V) (X.homOfLE ⋯)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)) (X.homOfLE ⋯)

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.glueDataT_snd_assoc {X : Scheme} (I : X.IdealSheafData) (U V : ↑X.affineOpens) {Z : Scheme} (h : ↑(↑V ⊓ ↑U) ⟶ Z) : CategoryTheory.CategoryStruct.comp (I.glueDataT U V) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (I.glueDataObjι V) (X.homOfLE ⋯)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)) (CategoryTheory.CategoryStruct.comp (X.homOfLE ⋯) h)

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.glueDataT_fst {X : Scheme} (I : X.IdealSheafData) (U V : ↑X.affineOpens) : CategoryTheory.CategoryStruct.comp (I.glueDataT U V) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯)) (I.glueDataObjι V)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)) (X.homOfLE ⋯)

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.glueDataT_fst_assoc {X : Scheme} (I : X.IdealSheafData) (U V : ↑X.affineOpens) {Z : Scheme} (h : ↑↑V ⟶ Z) : CategoryTheory.CategoryStruct.comp (I.glueDataT U V) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯)) (CategoryTheory.CategoryStruct.comp (I.glueDataObjι V) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (I.glueDataObjι U) (X.homOfLE ⋯)) (CategoryTheory.CategoryStruct.comp (X.homOfLE ⋯) h)

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.

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.glueDataT'Aux_fst {X : Scheme} (I : X.IdealSheafData) (U V W U₀ : ↑X.affineOpens) (hU₀ : ↑U ⊓ ↑W ≤ ↑U₀) : CategoryTheory.CategoryStruct.comp (I.glueDataT'Aux U V W U₀ hU₀) (CategoryTheory.Limits.pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) (CategoryTheory.Limits.pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯))) (CategoryTheory.CategoryStruct.comp (I.glueDataT U V) (CategoryTheory.Limits.pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯)))

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.glueDataT'Aux_fst_assoc {X : Scheme} (I : X.IdealSheafData) (U V W U₀ : ↑X.affineOpens) (hU₀ : ↑U ⊓ ↑W ≤ ↑U₀) {Z : Scheme} (h : I.glueDataObj V ⟶ Z) : CategoryTheory.CategoryStruct.comp (I.glueDataT'Aux U V W U₀ hU₀) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) (CategoryTheory.Limits.pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯))) (CategoryTheory.CategoryStruct.comp (I.glueDataT U V) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (I.glueDataObjι V) (X.homOfLE ⋯)) h))

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.glueDataT'Aux_snd_ι {X : Scheme} (I : X.IdealSheafData) (U V W U₀ : ↑X.affineOpens) (hU₀ : ↑U ⊓ ↑W ≤ ↑U₀) : CategoryTheory.CategoryStruct.comp (I.glueDataT'Aux U V W U₀ hU₀) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (I.glueDataObjι V) (X.homOfLE ⋯)) (↑V ⊓ ↑U₀).ι) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) (CategoryTheory.Limits.pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) (CategoryTheory.CategoryStruct.comp (I.glueDataObjι U) (↑U).ι))

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.glueDataT'Aux_snd_ι_assoc {X : Scheme} (I : X.IdealSheafData) (U V W U₀ : ↑X.affineOpens) (hU₀ : ↑U ⊓ ↑W ≤ ↑U₀) {Z : Scheme} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (I.glueDataT'Aux U V W U₀ hU₀) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (I.glueDataObjι V) (X.homOfLE ⋯)) (CategoryTheory.CategoryStruct.comp (↑V ⊓ ↑U₀).ι h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) (CategoryTheory.Limits.pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (I.glueDataObjι U) (X.homOfLE ⋯)) (CategoryTheory.CategoryStruct.comp (I.glueDataObjι U) (CategoryTheory.CategoryStruct.comp (↑U).ι h)))

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_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_V {X : Scheme} (I : X.IdealSheafData) (ij : ↑X.affineOpens × ↑X.affineOpens) : I.glueData.V ij = I.glueDataObjPullback ij.1 ij.2

@[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_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 : ↑X.affineOpens) : I.glueData.t i j = I.glueDataT i j