NYLL
Module

LocalComplement.lean

Nyll.SchemeTheory.Divisors.LocalComplement
16 declarations indexed from sourceView source ↗

Module documentation

Local descriptions of support complements

This file identifies the complement of the support of an ideal sheaf near a scheme point. If the stalk ideal becomes principal after localizing at a prime, the resulting open subscheme is canonically the spectrum of the localization away from that principal generator.

Imports4
Imported by15

Declarations

def

idealComplement

L32 ↗
PrimeSpectrum.idealComplement
Documentation

The open complement of the closed set cut out by an ideal.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
open scoped BigOperators
namespace PrimeSpectrum
universe u
Lean source · statement
def idealComplement {R : Type u} [CommRing R] (J : Ideal R) :
    Opens (PrimeSpectrum R)
theorem

mem_idealComplement

L38 ↗
PrimeSpectrum.mem_idealComplement
Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
open scoped BigOperators
namespace PrimeSpectrum
universe u
Lean source · statement
theorem mem_idealComplement {R : Type u} [CommRing R] (J : Ideal R)
    (p : PrimeSpectrum R) :
    p ∈ idealComplement J ↔ ¬ J ≤ p.asIdeal
theorem

preimage_idealComplement

L45 ↗
PrimeSpectrum.preimage_idealComplement
Documentation

Pulling an ideal complement back along a spectrum map extends the defining ideal.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
open scoped BigOperators
namespace PrimeSpectrum
universe u
Lean source · statement
theorem preimage_idealComplement {A B : Type u} [CommRing A] [CommRing B]
    (f : A →+* B) (J : Ideal A) :
    Spec.map (CommRingCat.ofHom f) ⁻¹ᵁ idealComplement J =
      idealComplement (J.map f)
theorem

idealComplement_span_singleton

L57 ↗
PrimeSpectrum.idealComplement_span_singleton
Documentation

The complement of the vanishing set of a principal ideal is the corresponding basic open.

Source context 5 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
open scoped BigOperators
namespace PrimeSpectrum
universe u
Lean source · statement
theorem idealComplement_span_singleton {R : Type u} [CommRing R]
    (f : R) :
    idealComplement (Ideal.span {f}) = basicOpen f
def

localizationAtPrimeTo

L75 ↗
AlgebraicGeometry.Scheme.localizationAtPrimeTo
Documentation

The canonical map from the spectrum of a prime localization of the stalk at x back to X.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme
universe u
variable (X : Scheme.{u}) (x : X)
Lean source · statement
def localizationAtPrimeTo
    (P : Ideal (X.presheaf.stalk x)) [P.IsPrime] :
    Spec (.of (Localization.AtPrime P)) ⟶ X
lemma

support_finset_prod

L91 ↗
AlgebraicGeometry.Scheme.IdealSheafData.support_finset_prod
Documentation

The support of a finite product is the finite union of the supports.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme.IdealSheafData
universe u
variable {X Y : Scheme.{u}}
Lean source · full declaration
lemma support_finset_prod {ι : Type*} (s : Finset ι)
    (I : ι → X.IdealSheafData) :
    (∏ i ∈ s, I i).support = s.sup (fun i => (I i).support) := by
  classical
  induction s using Finset.induction_on with
  | empty =>
      rw [Finset.prod_empty, one_eq_top, support_top, Finset.sup_empty]
  | insert i s hi ih =>
      rw [Finset.prod_insert hi, support_mul, Finset.sup_insert, ih]
def

supportComplement

L102 ↗
AlgebraicGeometry.Scheme.IdealSheafData.supportComplement
Documentation

The canonical open complement of the support of an ideal sheaf.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme.IdealSheafData
universe u
variable {X Y : Scheme.{u}}
Lean source · statement
def supportComplement (I : X.IdealSheafData) : X.Opens
theorem

mem_supportComplement

L105 ↗
AlgebraicGeometry.Scheme.IdealSheafData.mem_supportComplement
Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme.IdealSheafData
universe u
variable {X Y : Scheme.{u}}
Lean source · statement
theorem mem_supportComplement (I : X.IdealSheafData) (y : X) :
    y ∈ I.supportComplement ↔ y ∉ I.support
theorem

supportComplement_comap

L112 ↗
AlgebraicGeometry.Scheme.IdealSheafData.supportComplement_comap
Documentation

Formation of the support complement commutes with pullback of an ideal sheaf.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme.IdealSheafData
universe u
variable {X Y : Scheme.{u}}
Lean source · statement
theorem supportComplement_comap
    (I : Y.IdealSheafData) (f : X ⟶ Y) :
    (I.comap f).supportComplement = f ⁻¹ᵁ I.supportComplement
theorem

mem_support_fromSpecStalk_iff_stalkIdeal_le

L123 ↗
AlgebraicGeometry.Scheme.IdealSheafData.mem_support_fromSpecStalk_iff_stalkIdeal_le
Documentation

A point of the spectrum of 𝒪_{X,x} lies over the support precisely when its prime contains the stalk ideal.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme.IdealSheafData
universe u
variable {X Y : Scheme.{u}}
Lean source · statement
theorem mem_support_fromSpecStalk_iff_stalkIdeal_le
    (I : X.IdealSheafData) (x : X)
    (p : Spec (X.presheaf.stalk x)) :
    X.fromSpecStalk x p ∈ I.support ↔ I.stalkIdeal x ≤ p.asIdeal
theorem

fromSpecStalk_preimage_supportComplement

L159 ↗
AlgebraicGeometry.Scheme.IdealSheafData.fromSpecStalk_preimage_supportComplement
Documentation

On the spectrum of the stalk, the support complement is the complement of the stalk ideal.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme.IdealSheafData
universe u
variable {X Y : Scheme.{u}}
Lean source · statement
theorem fromSpecStalk_preimage_supportComplement
    (I : X.IdealSheafData) (x : X) :
    X.fromSpecStalk x ⁻¹ᵁ I.supportComplement =
      PrimeSpectrum.idealComplement (I.stalkIdeal x)
theorem

localizationAtPrimeTo_preimage_supportComplement

L171 ↗
AlgebraicGeometry.Scheme.IdealSheafData.localizationAtPrimeTo_preimage_supportComplement
Documentation

After localizing the stalk at a prime, the support complement is defined by the extended stalk ideal.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme.IdealSheafData
universe u
variable {X Y : Scheme.{u}}
Lean source · statement
theorem localizationAtPrimeTo_preimage_supportComplement
    (I : X.IdealSheafData) (x : X)
    (P : Ideal (X.presheaf.stalk x)) [P.IsPrime] :
    Scheme.localizationAtPrimeTo X x P ⁻¹ᵁ I.supportComplement =
      PrimeSpectrum.idealComplement
        ((I.stalkIdeal x).map
          (algebraMap (X.presheaf.stalk x) (Localization.AtPrime P)))
theorem

localizationAtPrimeTo_preimage_supportComplement_eq_basicOpen

L184 ↗
AlgebraicGeometry.Scheme.IdealSheafData.localizationAtPrimeTo_preimage_supportComplement_eq_basicOpen
Documentation

If the localized stalk ideal is generated by f, the local support complement is the basic open D(f).

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme.IdealSheafData
universe u
variable {X Y : Scheme.{u}}
Lean source · statement
theorem localizationAtPrimeTo_preimage_supportComplement_eq_basicOpen
    (I : X.IdealSheafData) (x : X)
    (P : Ideal (X.presheaf.stalk x)) [P.IsPrime]
    (f : Localization.AtPrime P)
    (hboundary :
      (I.stalkIdeal x).map
          (algebraMap (X.presheaf.stalk x) (Localization.AtPrime P)) =
        Ideal.span {f}) :
    Scheme.localizationAtPrimeTo X x P ⁻¹ᵁ I.supportComplement =
      PrimeSpectrum.basicOpen f
def

localizationAtPrimeSupportComplementIsoSpecAway

L199 ↗
AlgebraicGeometry.Scheme.IdealSheafData.localizationAtPrimeSupportComplementIsoSpecAway
Documentation

The local support complement cut out by a principal stalk ideal is the spectrum of the localization away from its generator.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme.IdealSheafData
universe u
variable {X Y : Scheme.{u}}
Lean source · statement
def localizationAtPrimeSupportComplementIsoSpecAway
    (I : X.IdealSheafData) (x : X)
    (P : Ideal (X.presheaf.stalk x)) [P.IsPrime]
    (f : Localization.AtPrime P)
    (hboundary :
      (I.stalkIdeal x).map
          (algebraMap (X.presheaf.stalk x) (Localization.AtPrime P)) =
        Ideal.span {f}) :
    (Scheme.localizationAtPrimeTo X x P ⁻¹ᵁ
        I.supportComplement).toScheme ≅
      Spec (.of (Localization.Away f))
def

localizationAwayToSupportComplement

L217 ↗
AlgebraicGeometry.Scheme.IdealSheafData.localizationAwayToSupportComplement
Documentation

The canonical morphism from the localized principal complement into the global support complement.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme.IdealSheafData
universe u
variable {X Y : Scheme.{u}}
Lean source · statement
def localizationAwayToSupportComplement
    (I : X.IdealSheafData) (x : X)
    (P : Ideal (X.presheaf.stalk x)) [P.IsPrime]
    (f : Localization.AtPrime P)
    (hboundary :
      (I.stalkIdeal x).map
          (algebraMap (X.presheaf.stalk x) (Localization.AtPrime P)) =
        Ideal.span {f}) :
    Spec (.of (Localization.Away f)) ⟶ I.supportComplement
theorem

localizationAwayToSupportComplement_comp_ι

L233 ↗
AlgebraicGeometry.Scheme.IdealSheafData.localizationAwayToSupportComplement_comp_ι
Documentation

The map to the support complement is the factorization of the canonical map from the principal localization back to the ambient scheme.

Source context 6 commands

Surrounding namespaces, section variables, and local commands at this declaration.

noncomputable section
open AlgebraicGeometry CategoryTheory TopologicalSpace
open scoped BigOperators
namespace AlgebraicGeometry.Scheme.IdealSheafData
universe u
variable {X Y : Scheme.{u}}
Lean source · statement
theorem localizationAwayToSupportComplement_comp_ι
    (I : X.IdealSheafData) (x : X)
    (P : Ideal (X.presheaf.stalk x)) [P.IsPrime]
    (f : Localization.AtPrime P)
    (hboundary :
      (I.stalkIdeal x).map
          (algebraMap (X.presheaf.stalk x) (Localization.AtPrime P)) =
        Ideal.span {f}) :
    localizationAwayToSupportComplement I x P f hboundary ≫
        I.supportComplement.ι =
      Spec.map (CommRingCat.ofHom
          (algebraMap (Localization.AtPrime P) (Localization.Away f))) ≫
        Scheme.localizationAtPrimeTo X x P

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.