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

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