Module

ComponentStalkBranch.lean

Nyll.SchemeTheory.Divisors.ComponentStalkBranch

15 declarations indexed from sourceView source ↗

Module documentation

Component branches in a specialized stalk

The generic point of an irreducible boundary component specializes to each point on that component. Pulling the closed prime of the generic stalk back along the corresponding generization map gives the canonical branch prime in the stalk at the specialized point.

Imports4

Imported by5

def

specializationPrime

L35 ↗

AlgebraicGeometry.Scheme.specializationPrime

Documentation

The prime of O_{X,y} represented by a generalization x of y. It is the inverse image of the maximal ideal of O_{X,x} under the generization map.

Source context 5 commands

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

noncomputable section
open CategoryTheory TopologicalSpace IsLocalRing
namespace AlgebraicGeometry.Scheme
universe u
variable {X : Scheme.{u}} {x y : X}

Lean source · statement

def specializationPrime (hxy : x ⤳ y) :
    Spec (X.presheaf.stalk y)

theorem

fromSpecStalk_specializationPrime

L42 ↗

AlgebraicGeometry.Scheme.fromSpecStalk_specializationPrime

Documentation

The specialization prime maps back to its defining generalization.

Source context 5 commands

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

noncomputable section
open CategoryTheory TopologicalSpace IsLocalRing
namespace AlgebraicGeometry.Scheme
universe u
variable {X : Scheme.{u}} {x y : X}

Lean source · statement

theorem fromSpecStalk_specializationPrime (hxy : x ⤳ y) :
    X.fromSpecStalk y (specializationPrime hxy) = x

theorem

specializationPrime_height

L52 ↗

AlgebraicGeometry.Scheme.specializationPrime_height

Documentation

The height of the specialization prime is the codimension of its defining generalization.

Source context 5 commands

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

noncomputable section
open CategoryTheory TopologicalSpace IsLocalRing
namespace AlgebraicGeometry.Scheme
universe u
variable {X : Scheme.{u}} {x y : X}

Lean source · statement

theorem specializationPrime_height (hxy : x ⤳ y) :
    (specializationPrime hxy).asIdeal.height = Order.coheight x

theorem

specializationPrime_asIdeal_eq_ker_residue

L69 ↗

AlgebraicGeometry.Scheme.specializationPrime_asIdeal_eq_ker_residue

Documentation

The specialization prime is the kernel of evaluation in the residue field of its defining generalization.

Source context 5 commands

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

noncomputable section
open CategoryTheory TopologicalSpace IsLocalRing
namespace AlgebraicGeometry.Scheme
universe u
variable {X : Scheme.{u}} {x y : X}

Lean source · statement

theorem specializationPrime_asIdeal_eq_ker_residue (hxy : x ⤳ y) :
    (specializationPrime hxy).asIdeal =
      RingHom.ker
        ((X.residue x).hom.comp
          (X.presheaf.stalkSpecializes hxy).hom)

theorem

specializationPrime_quotient_charZero

L84 ↗

AlgebraicGeometry.Scheme.specializationPrime_quotient_charZero

Documentation

Characteristic zero descends from the generic residue field to the quotient by the corresponding specialization prime.

Source context 5 commands

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

noncomputable section
open CategoryTheory TopologicalSpace IsLocalRing
namespace AlgebraicGeometry.Scheme
universe u
variable {X : Scheme.{u}} {x y : X}

Lean source · statement

theorem specializationPrime_quotient_charZero
    (hxy : x ⤳ y) [CharZero (X.residueField x)] :
    CharZero
      (X.presheaf.stalk y ⧸ (specializationPrime hxy).asIdeal)

theorem

specializationPrime_le_maximalIdeal

L96 ↗

AlgebraicGeometry.Scheme.specializationPrime_le_maximalIdeal

Documentation

Every specialization prime is contained in the closed prime of the specialized local ring.

Source context 5 commands

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

noncomputable section
open CategoryTheory TopologicalSpace IsLocalRing
namespace AlgebraicGeometry.Scheme
universe u
variable {X : Scheme.{u}} {x y : X}

Lean source · statement

theorem specializationPrime_le_maximalIdeal (hxy : x ⤳ y) :
    (specializationPrime hxy).asIdeal ≤
      IsLocalRing.maximalIdeal (X.presheaf.stalk y)

def

specializationPrimeQuotientToResidueField

L104 ↗

AlgebraicGeometry.Scheme.specializationPrimeQuotientToResidueField

Documentation

The residue field at the specialized point is a residue-characteristic target for the component branch quotient.

Source context 5 commands

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

noncomputable section
open CategoryTheory TopologicalSpace IsLocalRing
namespace AlgebraicGeometry.Scheme
universe u
variable {X : Scheme.{u}} {x y : X}

Lean source · statement

def specializationPrimeQuotientToResidueField
    (hxy : x ⤳ y) :
    (X.presheaf.stalk y ⧸ (specializationPrime hxy).asIdeal) →+*
      X.residueField y

theorem

stalkIdeal_le_specializationPrime_of_mem_support

L118 ↗

AlgebraicGeometry.Scheme.IdealSheafData.stalkIdeal_le_specializationPrime_of_mem_support

Documentation

If the generalization lies on an ideal-sheaf support, then the corresponding specialization prime contains the stalk ideal.

Source context 5 commands

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

noncomputable section
open CategoryTheory TopologicalSpace IsLocalRing
namespace AlgebraicGeometry.Scheme
universe u
variable {X : Scheme.{u}} {x y : X}

Lean source · statement

theorem IdealSheafData.stalkIdeal_le_specializationPrime_of_mem_support
    (I : X.IdealSheafData) (hxy : x ⤳ y) (hxI : x ∈ I.support) :
    I.stalkIdeal y ≤ (specializationPrime hxy).asIdeal

theorem

componentGenericPoint_specializes_subschemeι

L152 ↗

AlgebraicGeometry.Scheme.IdealSheafData.componentGenericPoint_specializes_subschemeι

Documentation

The generic point of a component specializes to every point of that component.

Source context 7 commands

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

noncomputable section
open CategoryTheory TopologicalSpace IsLocalRing
namespace AlgebraicGeometry.Scheme
universe u
variable {X : Scheme.{u}} {x y : X}
namespace IdealSheafData
variable {I : X.IdealSheafData}

Lean source · statement

theorem componentGenericPoint_specializes_subschemeι
    (I : X.IdealSheafData)
    (Z : Set I.subscheme) (hZ : Z ∈ irreducibleComponents I.subscheme)
    (z : I.subscheme) (hz : z ∈ Z) :
    I.componentGenericPoint Z hZ ⤳ I.subschemeι z

def

componentBranchPrimeAt

L163 ↗

AlgebraicGeometry.Scheme.IdealSheafData.componentBranchPrimeAt

Documentation

The canonical branch prime in the ambient stalk at a point of a chosen component.

Source context 7 commands

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

noncomputable section
open CategoryTheory TopologicalSpace IsLocalRing
namespace AlgebraicGeometry.Scheme
universe u
variable {X : Scheme.{u}} {x y : X}
namespace IdealSheafData
variable {I : X.IdealSheafData}

Lean source · statement

def componentBranchPrimeAt
    (I : X.IdealSheafData)
    (Z : Set I.subscheme) (hZ : Z ∈ irreducibleComponents I.subscheme)
    (z : I.subscheme) (hz : z ∈ Z) :
    Spec (X.presheaf.stalk (I.subschemeι z))

theorem

fromSpecStalk_componentBranchPrimeAt

L173 ↗

AlgebraicGeometry.Scheme.IdealSheafData.fromSpecStalk_componentBranchPrimeAt

Documentation

The component branch represents the component generic point in the local scheme at the chosen specialization.

Source context 7 commands

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

noncomputable section
open CategoryTheory TopologicalSpace IsLocalRing
namespace AlgebraicGeometry.Scheme
universe u
variable {X : Scheme.{u}} {x y : X}
namespace IdealSheafData
variable {I : X.IdealSheafData}

Lean source · statement

theorem fromSpecStalk_componentBranchPrimeAt
    (I : X.IdealSheafData)
    (Z : Set I.subscheme) (hZ : Z ∈ irreducibleComponents I.subscheme)
    (z : I.subscheme) (hz : z ∈ Z) :
    X.fromSpecStalk (I.subschemeι z)
        (I.componentBranchPrimeAt Z hZ z hz) =
      I.componentGenericPoint Z hZ

theorem

componentBranchPrimeAt_height_eq_one

L184 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IsEffectiveCartier.componentBranchPrimeAt_height_eq_one

Documentation

On a locally Noetherian scheme, the canonical branch of an effective Cartier component has height one.

Source context 7 commands

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

noncomputable section
open CategoryTheory TopologicalSpace IsLocalRing
namespace AlgebraicGeometry.Scheme
universe u
variable {X : Scheme.{u}} {x y : X}
namespace IdealSheafData
variable {I : X.IdealSheafData}

Lean source · statement

theorem IsEffectiveCartier.componentBranchPrimeAt_height_eq_one
    [IsLocallyNoetherian X]
    (hI : I.IsEffectiveCartier)
    (Z : Set I.subscheme) (hZ : Z ∈ irreducibleComponents I.subscheme)
    (z : I.subscheme) (hz : z ∈ Z) :
    (I.componentBranchPrimeAt Z hZ z hz).asIdeal.height = 1

theorem

exists_componentGenericPoint_eq_fromSpecStalk

L198 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IsEffectiveCartier.exists_componentGenericPoint_eq_fromSpecStalk

Documentation

Every height-one prime of a stalk containing an effective Cartier ideal represents the generic point of an irreducible component of the divisor.

This is the converse to constructing a height-one stalk prime from a chosen component and specialization.

Source context 7 commands

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

noncomputable section
open CategoryTheory TopologicalSpace IsLocalRing
namespace AlgebraicGeometry.Scheme
universe u
variable {X : Scheme.{u}} {x y : X}
namespace IdealSheafData
variable {I : X.IdealSheafData}

Lean source · statement

theorem IsEffectiveCartier.exists_componentGenericPoint_eq_fromSpecStalk
    [IsLocallyNoetherian X]
    (hI : I.IsEffectiveCartier) (x : X)
    (q : Spec (X.presheaf.stalk x))
    (hqheight : q.asIdeal.height = 1)
    (hIq : I.stalkIdeal x ≤ q.asIdeal) :
    ∃ (Z : Set I.subscheme)
      (hZ : Z ∈ irreducibleComponents I.subscheme),
      I.componentGenericPoint Z hZ = X.fromSpecStalk x q

theorem

exists_componentBranchPrimeAt_eq

L251 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IsEffectiveCartier.exists_componentBranchPrimeAt_eq

Documentation

Every height-one prime in the stalk at a point of an effective Cartier divisor is the canonical branch prime of a component through that point.

Source context 7 commands

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

noncomputable section
open CategoryTheory TopologicalSpace IsLocalRing
namespace AlgebraicGeometry.Scheme
universe u
variable {X : Scheme.{u}} {x y : X}
namespace IdealSheafData
variable {I : X.IdealSheafData}

Lean source · statement

theorem IsEffectiveCartier.exists_componentBranchPrimeAt_eq
    [IsLocallyNoetherian X]
    (hI : I.IsEffectiveCartier) (z : I.subscheme)
    (q : Spec (X.presheaf.stalk (I.subschemeι z)))
    (hqheight : q.asIdeal.height = 1)
    (hIq : I.stalkIdeal (I.subschemeι z) ≤ q.asIdeal) :
    ∃ (Z : Set I.subscheme)
      (hZ : Z ∈ irreducibleComponents I.subscheme)
      (hz : z ∈ Z),
      I.componentBranchPrimeAt Z hZ z hz = q

theorem

stalkIdeal_le_componentBranchPrimeAt

L285 ↗

AlgebraicGeometry.Scheme.IdealSheafData.stalkIdeal_le_componentBranchPrimeAt

Documentation

The canonical component branch contains the boundary stalk ideal.

Source context 7 commands

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

noncomputable section
open CategoryTheory TopologicalSpace IsLocalRing
namespace AlgebraicGeometry.Scheme
universe u
variable {X : Scheme.{u}} {x y : X}
namespace IdealSheafData
variable {I : X.IdealSheafData}

Lean source · statement

theorem stalkIdeal_le_componentBranchPrimeAt
    (I : X.IdealSheafData)
    (Z : Set I.subscheme) (hZ : Z ∈ irreducibleComponents I.subscheme)
    (z : I.subscheme) (hz : z ∈ Z) :
    I.stalkIdeal (I.subschemeι z) ≤
      (I.componentBranchPrimeAt Z hZ z hz).asIdeal

Module documentation

Component branches in a specialized stalk

Declarations