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

  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

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

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.

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.

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

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

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

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

@[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.le_of_iSup_eq_top {X : Scheme} {I J : X.IdealSheafData} {ι : Type u_1} (U : ι → ↑X.affineOpens) (hU : ⨆ (i : ι), ↑(U i) = ⊤) (H : ∀ (i : ι), I.ideal (U i) ≤ J.ideal (U i)) : I ≤ J

theorem AlgebraicGeometry.Scheme.IdealSheafData.ext_of_iSup_eq_top {X : Scheme} {I J : X.IdealSheafData} {ι : Type u_1} (U : ι → ↑X.affineOpens) (hU : ⨆ (i : ι), ↑(U i) = ⊤) (H : ∀ (i : ι), I.ideal (U i) = J.ideal (U i)) : I = J

theorem AlgebraicGeometry.Scheme.IdealSheafData.mem_supportSet_iff {X : Scheme} {I : X.IdealSheafData} {x : ↥X} : 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} {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

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

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)

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.mem_supportSet_iff_mem_support {X : Scheme} {I : X.IdealSheafData} {x : ↥X} : x ∈ I.supportSet ↔ x ∈ I.support

theorem AlgebraicGeometry.Scheme.IdealSheafData.mem_support_iff {X : Scheme} {I : X.IdealSheafData} {x : ↥X} : 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} {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

Custom simps projection for IdealSheafData.

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

@[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) (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.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) (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.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 = ⊤

instance AlgebraicGeometry.Scheme.IdealSheafData.instZero {X : Scheme} : Zero X.IdealSheafData

instance AlgebraicGeometry.Scheme.IdealSheafData.instOne {X : Scheme} : One X.IdealSheafData

instance AlgebraicGeometry.Scheme.IdealSheafData.instAdd {X : Scheme} : Add X.IdealSheafData

instance AlgebraicGeometry.Scheme.IdealSheafData.instMul {X : Scheme} : Mul X.IdealSheafData

instance AlgebraicGeometry.Scheme.IdealSheafData.instPowNat {X : Scheme} : Pow X.IdealSheafData ℕ

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_mul {X : Scheme} (I J : X.IdealSheafData) : (I * J).ideal = I.ideal * J.ideal

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.support_mul {X : Scheme} (I J : X.IdealSheafData) : (I * J).support = I.support ⊔ J.support

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_pow {X : Scheme} (I : X.IdealSheafData) (n : ℕ) : (I ^ n).ideal = I.ideal ^ n

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.support_pow_succ {X : Scheme} (I : X.IdealSheafData) (n : ℕ) : (I ^ (n + 1)).support = I.support

theorem AlgebraicGeometry.Scheme.IdealSheafData.support_pow {X : Scheme} (I : X.IdealSheafData) (n : ℕ) (hn : n ≠ 0) : (I ^ n).support = I.support

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.top_mul {X : Scheme} (I : X.IdealSheafData) : ⊤ * I = I

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.mul_top {X : Scheme} (I : X.IdealSheafData) : I * ⊤ = I

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.bot_mul {X : Scheme} (I : X.IdealSheafData) : ⊥ * I = ⊥

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.mul_bot {X : Scheme} (I : X.IdealSheafData) : I * ⊥ = ⊥

theorem AlgebraicGeometry.Scheme.IdealSheafData.mul_inf {X : Scheme} (I J K : X.IdealSheafData) : I * (J ⊔ K) = I * J ⊔ I * K

theorem AlgebraicGeometry.Scheme.IdealSheafData.inf_mul {X : Scheme} (I J K : X.IdealSheafData) : (I ⊔ J) * K = I * K ⊔ J * K

instance AlgebraicGeometry.Scheme.IdealSheafData.instIdemCommSemiring {X : Scheme} : IdemCommSemiring X.IdealSheafData

instance AlgebraicGeometry.Scheme.IdealSheafData.instIsOrderedRing {X : Scheme} : IsOrderedRing X.IdealSheafData

We follow Ideal and set the simp normal form to be ⊥ and ⊤ and ⊔.

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.zero_eq_bot {X : Scheme} : 0 = ⊥

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.one_eq_top {X : Scheme} : 1 = ⊤

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.add_eq_sup {X : Scheme} (I J : X.IdealSheafData) : I + J = I ⊔ J

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.

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

@[simp]

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

@[simp]

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

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

The radical of an ideal sheaf.

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

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

@[simp]

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

def AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal {X : Scheme} (Z : TopologicalSpace.Closeds ↥X) : 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.

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_ideal {X : Scheme} (Z : TopologicalSpace.Closeds ↥X) (U : ↑X.affineOpens) : (vanishingIdeal Z).ideal U = PrimeSpectrum.vanishingIdeal (⇑(IsAffineOpen.fromSpec ⋯) ⁻¹' ↑Z)

@[simp]

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

theorem AlgebraicGeometry.Scheme.IdealSheafData.le_support_iff_le_vanishingIdeal {X : Scheme} {I : X.IdealSheafData} {Z : TopologicalSpace.Closeds ↥X} : 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)ᵒᵈ) => 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} (h : S ≤ T) : vanishingIdeal T ≤ vanishingIdeal S

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

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_bot {X : Scheme} : vanishingIdeal ⊥ = ⊤

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_top {X : Scheme} : vanishingIdeal ⊤ = X.nilradical

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_iSup {X : Scheme} {ι : Sort u_1} (Z : ι → TopologicalSpace.Closeds ↥X) : vanishingIdeal (iSup Z) = ⨅ (i : ι), vanishingIdeal (Z i)

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_sSup {X : Scheme} (Z : Set (TopologicalSpace.Closeds ↥X)) : vanishingIdeal (sSup Z) = ⨅ z ∈ Z, vanishingIdeal z

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal_sup {X : Scheme} (Z Z' : TopologicalSpace.Closeds ↥X) : vanishingIdeal (Z ⊔ Z') = vanishingIdeal Z ⊓ vanishingIdeal Z'

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.support_sup {X : Scheme} (I J : X.IdealSheafData) : (I ⊔ J).support = I.support ⊓ J.support

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.support_iSup {X : Scheme} {ι : Sort u_1} (I : ι → X.IdealSheafData) : (iSup I).support = ⨅ (i : ι), (I i).support

@[simp]

theorem AlgebraicGeometry.Scheme.IdealSheafData.support_sSup {X : Scheme} (I : Set X.IdealSheafData) : (sSup I).support = ⨅ i ∈ I, i.support

theorem AlgebraicGeometry.Scheme.nilradical_eq_bot {X : Scheme} [IsReduced X] : X.nilradical = ⊥

theorem AlgebraicGeometry.Scheme.IdealSheafData.support_eq_top_iff {X : Scheme} [IsReduced X] {I : X.IdealSheafData} : I.support = ⊤ ↔ I = ⊥

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.

theorem AlgebraicGeometry.Scheme.Hom.ideal_ker_le {X Y : Scheme} (f : X.Hom Y) (U : ↑Y.affineOpens) : f.ker.ideal U ≤ 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] : f.ker = ⊤

@[simp]

theorem AlgebraicGeometry.Scheme.Hom.ker_eq_bot_of_isIso {X Y : Scheme} (f : X ⟶ Y) [CategoryTheory.IsIso f] : ker f = ⊥

theorem AlgebraicGeometry.Scheme.Hom.ker_comp_of_isIso {X Y Z : Scheme} (f : X ⟶ Y) (g : Y ⟶ Z) [CategoryTheory.IsIso f] : ker (CategoryTheory.CategoryStruct.comp f g) = ker g

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 ⟶ Y) : Set.range ⇑f ⊆ ↑(ker f).support

theorem AlgebraicGeometry.Scheme.Hom.ker_eq_top_iff_isEmpty {X Y : Scheme} (f : X.Hom Y) : f.ker = ⊤ ↔ IsEmpty ↥X

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 : 𝒰.I₀), (ker (CategoryTheory.CategoryStruct.comp (𝒰.f 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 : 𝒰.I₀), ker (CategoryTheory.CategoryStruct.comp (𝒰.f 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 𝒰.I₀] : ⋃ (i : 𝒰.I₀), ↑(ker (CategoryTheory.CategoryStruct.comp (𝒰.f 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 ⟶ Y) [QuasiCompact f] : ↑(ker f).support = closure (Set.range ⇑f)

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.

@[simp]

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

@[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.ker_toSpecΓ (X : Scheme) [CompactSpace ↥X] : Hom.ker X.toSpecΓ = ⊥