Module

SubschemeStalk.lean

Nyll.SchemeTheory.Divisors.SubschemeStalk

4 declarations indexed from sourceView source ↗

Module documentation

The local rings of a closed subscheme

The kernel of the stalk map of a closed immersion is the stalk ideal of its defining ideal sheaf. Thus the actual local ring of a closed subscheme is the quotient of the ambient local ring by its stalk ideal.

The comparison is obtained by localizing the surjective map on sections over an affine neighbourhood. In particular, the equivalence below is induced by the actual stalk map of the closed immersion.

Imports4

Nyll.SchemeTheory.Divisors.ArithmeticBoundaryEtale
Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Mathlib.RingTheory.Localization.Algebra
Mathlib.RingTheory.Ideal.Quotient.Operations

Imported by3

theorem

ker_stalkMap_eq_stalkIdeal

L33 ↗

AlgebraicGeometry.Scheme.Hom.ker_stalkMap_eq_stalkIdeal

Documentation

The ideal of a closed immersion localizes to the kernel of its stalk map.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
universe u
namespace AlgebraicGeometry.Scheme.Hom

Lean source · statement

theorem ker_stalkMap_eq_stalkIdeal {X Y : Scheme.{u}} (f : X ⟶ Y)
    [IsClosedImmersion f] (x : X) :
    RingHom.ker (f.stalkMap x).hom = f.ker.stalkIdeal (f x)

theorem

stalkIdeal_le_maximalIdeal_of_mem_support

L79 ↗

AlgebraicGeometry.Scheme.IdealSheafData.stalkIdeal_le_maximalIdeal_of_mem_support

Documentation

At a point on its support, a closed subscheme has a proper stalk ideal.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
universe u
namespace AlgebraicGeometry.Scheme.IdealSheafData

Lean source · statement

theorem stalkIdeal_le_maximalIdeal_of_mem_support {X : Scheme.{u}}
    (I : X.IdealSheafData) (x : X) (hx : x ∈ I.support) :
    I.stalkIdeal x ≤ IsLocalRing.maximalIdeal (X.presheaf.stalk x)

def

subschemeStalkQuotientEquiv

L93 ↗

AlgebraicGeometry.Scheme.IdealSheafData.subschemeStalkQuotientEquiv

Documentation

The actual closed subscheme stalk is the quotient by the ambient stalk ideal.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
universe u
namespace AlgebraicGeometry.Scheme.IdealSheafData

Lean source · statement

def subschemeStalkQuotientEquiv {X : Scheme.{u}} (I : X.IdealSheafData)
    (x : I.subscheme) :
    (X.presheaf.stalk (I.subschemeι x) ⧸ I.stalkIdeal (I.subschemeι x)) ≃+*
      I.subscheme.presheaf.stalk x

theorem

subschemeStalkQuotientEquiv_apply_mk

L103 ↗

AlgebraicGeometry.Scheme.IdealSheafData.subschemeStalkQuotientEquiv_apply_mk

Documentation

The quotient comparison is induced by the closed immersion's stalk map.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
universe u
namespace AlgebraicGeometry.Scheme.IdealSheafData

Lean source · statement

theorem subschemeStalkQuotientEquiv_apply_mk {X : Scheme.{u}}
    (I : X.IdealSheafData) (x : I.subscheme)
    (a : X.presheaf.stalk (I.subschemeι x)) :
    I.subschemeStalkQuotientEquiv x
        (Ideal.Quotient.mk (I.stalkIdeal (I.subschemeι x)) a) =
      I.subschemeι.stalkMap x a

Module documentation

The local rings of a closed subscheme

Declarations

ker_stalkMap_eq_stalkIdeal

stalkIdeal_le_maximalIdeal_of_mem_support

subschemeStalkQuotientEquiv

subschemeStalkQuotientEquiv_apply_mk