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.
• AlgebraicGeometry.Scheme.IdealSheafData.subscheme: The subscheme associated to an ideal sheaf.
• AlgebraicGeometry.Scheme.IdealSheafData.subschemeι: The inclusion from the subscheme.

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 refactored 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)
3. a subset of X equal to the support.

Also see Scheme.IdealSheafData.mkOfMemSupportIff for a constructor with the condition on the support being (usually) easier to prove.

• 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

• supportSet : Set ↑↑X.toPresheafedSpace

  The support of an ideal sheaf. Use IdealSheafData.support instead for most occasions.

• supportSet_eq_iInter_zeroLocus : self.supportSet = ⋂ (U : ↑X.affineOpens), X.zeroLocus ↑(self.ideal U)

theorem AlgebraicGeometry.Scheme.IdealSheafData.ext {X : Scheme} {I J : X.IdealSheafData} (h : I.ideal = J.ideal) : I = J

theorem AlgebraicGeometry.Scheme.IdealSheafData.ext_iff {X : Scheme} {I J : X.IdealSheafData} : I = J ↔ I.ideal = J.ideal

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

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

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.instOrderTop {X : Scheme} : OrderTop X.IdealSheafData

Equations

• AlgebraicGeometry.Scheme.IdealSheafData.instOrderTop = { top := { ideal := ⊤, map_ideal_basicOpen := ⋯, supportSet := ⊥, supportSet_eq_iInter_zeroLocus := ⋯ }, le_top := ⋯ }

instance AlgebraicGeometry.Scheme.IdealSheafData.instOrderBot {X : Scheme} : OrderBot X.IdealSheafData

Equations

• AlgebraicGeometry.Scheme.IdealSheafData.instOrderBot = { bot := { ideal := ⊥, map_ideal_basicOpen := ⋯, supportSet := ⊤, supportSet_eq_iInter_zeroLocus := ⋯ }, bot_le := ⋯ }

instance AlgebraicGeometry.Scheme.IdealSheafData.instSemilatticeInf {X : Scheme} : SemilatticeInf X.IdealSheafData

Equations

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

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

Equations

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

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

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

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

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

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

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

theorem AlgebraicGeometry.Scheme.IdealSheafData.isClosed_supportSet {X : Scheme} (I : X.IdealSheafData) : IsClosed I.supportSet

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

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

Equations

• I.support = { carrier := I.supportSet, isClosed' := ⋯ }

theorem AlgebraicGeometry.Scheme.IdealSheafData.coe_support_eq_eq_iInter_zeroLocus {X : Scheme} (I : X.IdealSheafData) : ↑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.mem_support_iff_of_mem {X : Scheme} {I : X.IdealSheafData} {x : ↑↑X.toPresheafedSpace} {U : ↑X.affineOpens} (h : x ∈ ↑U) : x ∈ I.support ↔ x ∈ X.zeroLocus ↑(I.ideal U)

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

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

Custom simps projection for IdealSheafData.

Equations

• AlgebraicGeometry.Scheme.IdealSheafData.Simps.coe_support I = ↑I.support

def AlgebraicGeometry.Scheme.IdealSheafData.mkOfMemSupportIff {X : Scheme} (ideal : (U : ↑X.affineOpens) → Ideal ↑(X.presheaf.obj (Opposite.op ↑U))) (map_ideal_basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑(X.presheaf.obj (Opposite.op ↑U))), Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (CategoryTheory.homOfLE ⋯).op)) (ideal U) = ideal (X.affineBasicOpen f)) (supportSet : Set ↑↑X.toPresheafedSpace) (supportSet_inter : ∀ (U : ↑X.affineOpens), ∀ x ∈ ↑U, x ∈ supportSet ↔ x ∈ X.zeroLocus ↑(ideal U)) : X.IdealSheafData

A useful constructor of IdealSheafData with the condition on supportSet being easier to check.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.coe_support_mkOfMemSupportIff {X : Scheme} (ideal : (U : ↑X.affineOpens) → Ideal ↑(X.presheaf.obj (Opposite.op ↑U))) (map_ideal_basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑(X.presheaf.obj (Opposite.op ↑U))), Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (CategoryTheory.homOfLE ⋯).op)) (ideal U) = ideal (X.affineBasicOpen f)) (supportSet : Set ↑↑X.toPresheafedSpace) (supportSet_inter : ∀ (U : ↑X.affineOpens), ∀ x ∈ ↑U, x ∈ supportSet ↔ x ∈ X.zeroLocus ↑(ideal U)) : ↑(mkOfMemSupportIff ideal map_ideal_basicOpen supportSet supportSet_inter).support = supportSet

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.mkOfMemSupportIff_ideal {X : Scheme} (ideal : (U : ↑X.affineOpens) → Ideal ↑(X.presheaf.obj (Opposite.op ↑U))) (map_ideal_basicOpen : ∀ (U : ↑X.affineOpens) (f : ↑(X.presheaf.obj (Opposite.op ↑U))), Ideal.map (CommRingCat.Hom.hom (X.presheaf.map (CategoryTheory.homOfLE ⋯).op)) (ideal U) = ideal (X.affineBasicOpen f)) (supportSet : Set ↑↑X.toPresheafedSpace) (supportSet_inter : ∀ (U : ↑X.affineOpens), ∀ x ∈ ↑U, x ∈ supportSet ↔ x ∈ X.zeroLocus ↑(ideal U)) (U : ↑X.affineOpens) : (mkOfMemSupportIff ideal map_ideal_basicOpen supportSet supportSet_inter).ideal U = ideal U

@[simp]

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

@[simp]

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

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

@[simp]

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

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.coe_support_ofIdealTop {X : Scheme} (I : Ideal ↑(X.presheaf.obj (Opposite.op ⊤))) : ↑(ofIdealTop I).support = X.zeroLocus ↑I

@[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 ≃o 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 ⊤))) : (RelIso.symm equivOfIsAffine) I = ofIdealTop I

@[simp]

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

theorem AlgebraicGeometry.Scheme.IdealSheafData.Scheme.zeroLocus_radical {X : Scheme} {U : X.Opens} (I : Ideal ↑(X.presheaf.obj (Opposite.op U))) : X.zeroLocus ↑I.radical = X.zeroLocus ↑I

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

The radical of a ideal sheaf.

Equations

• I.radical = AlgebraicGeometry.Scheme.IdealSheafData.mkOfMemSupportIff (fun (U : ↑X.affineOpens) => (I.ideal U).radical) ⋯ I.supportSet ⋯

@[simp]

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

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.support_radical {X : Scheme} (I : X.IdealSheafData) : I.radical.support = I.support

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

The nilradical of a scheme.

Equations

• X.nilradical = ⊥.radical

@[simp]

theorem AlgebraicGeometry.Scheme.support_nilradical (X : Scheme) : X.nilradical.support = ⊤

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 : TopologicalSpace.Closeds ↑↑X.toPresheafedSpace) : X.IdealSheafData

The vanishing ideal sheaf of a closed set, which is the largest ideal sheaf whose support is equal to it. The reduced induced scheme structure on the closed set 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 : TopologicalSpace.Closeds ↑↑X.toPresheafedSpace) (U : ↑X.affineOpens) : (vanishingIdeal Z).ideal U = PrimeSpectrum.vanishingIdeal (⇑(CategoryTheory.ConcreteCategory.hom (IsAffineOpen.fromSpec ⋯).base) ⁻¹' ↑Z)

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.coe_support_vanishingIdeal {X : Scheme} (Z : TopologicalSpace.Closeds ↑↑X.toPresheafedSpace) : ↑(vanishingIdeal Z).support = ↑Z

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

theorem AlgebraicGeometry.Scheme.IdealSheafData.gc {X : Scheme} : GaloisConnection (fun (x : X.IdealSheafData) => x.support) fun (x : (TopologicalSpace.Closeds ↑↑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 : TopologicalSpace.Closeds ↑↑X.toPresheafedSpace} (h : S ≤ T) : vanishingIdeal T ≤ vanishingIdeal S

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.kerFunctor (Y : Scheme) : CategoryTheory.Functor (CategoryTheory.Over Y)ᵒᵖ Y.IdealSheafData

The functor taking a morphism into Y to its kernel as an ideal sheaf on Y.

Equations

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

@[simp]

theorem AlgebraicGeometry.Scheme.kerFunctor_map (Y : Scheme) {f g : (CategoryTheory.Over Y)ᵒᵖ} (hfg : f ⟶ g) : Y.kerFunctor.map hfg = CategoryTheory.homOfLE ⋯

@[simp]

theorem AlgebraicGeometry.Scheme.kerFunctor_obj (Y : Scheme) (f : (CategoryTheory.Over Y)ᵒᵖ) : Y.kerFunctor.obj f = Hom.ker (Opposite.unop f).hom

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

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.

Equations

• I.subscheme = (AlgebraicGeometry.Scheme.IdealSheafData.glueData✝ I).glued.restrict ⋯

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

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

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

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

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

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