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.

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 = ⊤