Module

StalkAwayComplement.lean

Nyll.SchemeTheory.Divisors.StalkAwayComplement

5 declarations indexed from sourceView source ↗

Module documentation

The principal complement of a stalk ideal

This is the one-localization counterpart of LocalComplement: the actual spectrum of the stalk localized away from a generator maps to the global support complement, and the canonical maps form a pullback square.

Imports2

Nyll.SchemeTheory.Divisors.LocalComplement
Mathlib.AlgebraicGeometry.OpenImmersion

Imported by2

theorem

fromSpecStalk_preimage_supportComplement_eq_basicOpen

L29 ↗

AlgebraicGeometry.Scheme.IdealSheafData.fromSpecStalk_preimage_supportComplement_eq_basicOpen

Documentation

A principal stalk ideal cuts out the corresponding basic open.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.Scheme.IdealSheafData
universe u
variable {X : Scheme.{u}}

Lean source · statement

theorem fromSpecStalk_preimage_supportComplement_eq_basicOpen
    (I : X.IdealSheafData) (x : X) (d : X.presheaf.stalk x)
    (hd : I.stalkIdeal x = Ideal.span {d}) :
    X.fromSpecStalk x ⁻¹ᵁ I.supportComplement = PrimeSpectrum.basicOpen d

def

stalkSupportComplementIsoSpecAway

L37 ↗

AlgebraicGeometry.Scheme.IdealSheafData.stalkSupportComplementIsoSpecAway

Documentation

The actual pullback complement is the spectrum of the principal localization.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.Scheme.IdealSheafData
universe u
variable {X : Scheme.{u}}

Lean source · statement

def stalkSupportComplementIsoSpecAway
    (I : X.IdealSheafData) (x : X) (d : X.presheaf.stalk x)
    (hd : I.stalkIdeal x = Ideal.span {d}) :
    (X.fromSpecStalk x ⁻¹ᵁ I.supportComplement).toScheme ≅
      Spec (.of (Localization.Away d))

def

stalkAwayToSupportComplement

L47 ↗

AlgebraicGeometry.Scheme.IdealSheafData.stalkAwayToSupportComplement

Documentation

The canonical map from the principal stalk complement to the global complement.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.Scheme.IdealSheafData
universe u
variable {X : Scheme.{u}}

Lean source · statement

def stalkAwayToSupportComplement
    (I : X.IdealSheafData) (x : X) (d : X.presheaf.stalk x)
    (hd : I.stalkIdeal x = Ideal.span {d}) :
    Spec (.of (Localization.Away d)) ⟶ I.supportComplement

theorem

stalkAwayToSupportComplement_comp_ι

L56 ↗

AlgebraicGeometry.Scheme.IdealSheafData.stalkAwayToSupportComplement_comp_ι

Documentation

The map from the principal localization lies over the original stalk map.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.Scheme.IdealSheafData
universe u
variable {X : Scheme.{u}}

Lean source · statement

theorem stalkAwayToSupportComplement_comp_ι
    (I : X.IdealSheafData) (x : X) (d : X.presheaf.stalk x)
    (hd : I.stalkIdeal x = Ideal.span {d}) :
    stalkAwayToSupportComplement I x d hd ≫ I.supportComplement.ι =
      Spec.map (CommRingCat.ofHom
        (algebraMap (X.presheaf.stalk x) (Localization.Away d))) ≫ X.fromSpecStalk x

theorem

isPullback_stalkAwayToSupportComplement

L85 ↗

AlgebraicGeometry.Scheme.IdealSheafData.isPullback_stalkAwayToSupportComplement

Documentation

The actual principal stalk complement is the pullback of the global complement.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace AlgebraicGeometry.Scheme.IdealSheafData
universe u
variable {X : Scheme.{u}}

Lean source · statement

theorem isPullback_stalkAwayToSupportComplement
    (I : X.IdealSheafData) (x : X) (d : X.presheaf.stalk x)
    (hd : I.stalkIdeal x = Ideal.span {d}) :
    IsPullback (stalkAwayToSupportComplement I x d hd)
      (Spec.map (CommRingCat.ofHom
        (algebraMap (X.presheaf.stalk x) (Localization.Away d))))
      I.supportComplement.ι (X.fromSpecStalk x)

Module documentation

The principal complement of a stalk ideal

Declarations

fromSpecStalk_preimage_supportComplement_eq_basicOpen

stalkSupportComplementIsoSpecAway

stalkAwayToSupportComplement

stalkAwayToSupportComplement_comp_ι

isPullback_stalkAwayToSupportComplement