NYLL
Module

CartierGenericPoint.lean

Nyll.EtaleFundamentalGroups.StrictHenselian.CartierGenericPoint
4 declarations indexed from sourceView source ↗

Module documentation

The strict-Henselian generic point of a Cartier boundary

The fraction field of the actual geometric etale stalk maps to the complement of an effective Cartier divisor. Its structure map is injective, whereas the stalk ideal of a Cartier divisor contains a regular element. Normality of the base local ring supplies the domain property of the geometric stalk. This proves that the generic point misses the divisor, and constructs the required factorization through the open complement. At a regular boundary component the DVR input is obtained from the component's actual local ring.

Imports9
Imported by6

Declarations

theorem

fieldFromStalk_mem_complement

L38 ↗
EtaleFundamentalGroups.StrictHenselian.fieldFromStalk_mem_complement
Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.StrictHenselian
universe u
Lean source · statement
theorem fieldFromStalk_mem_complement
    {X : Scheme.{u}} (D : X.EffectiveCartierDivisor) (x : X)
    {F : Type u} [Field F] (a : X.presheaf.stalk x →+* F)
    (ha : Function.Injective a) (y : Spec (.of F)) :
    X.fromSpecStalk x (Spec.map (CommRingCat.ofHom a) y) ∈ D.1.supportComplement
def

geometricStalkFractionFieldToComplement

L59 ↗
EtaleFundamentalGroups.StrictHenselian.geometricStalkFractionFieldToComplement
Documentation

The generic point of the actual geometric etale stalk factors through the Cartier complement over any normal domain stalk. The displayed source is the fraction field of that geometric stalk.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.StrictHenselian
universe u
Lean source · statement
def geometricStalkFractionFieldToComplement
    {X : Scheme.{u}} (D : X.EffectiveCartierDivisor) (x : X)
    [IsDomain (X.presheaf.stalk x)] [IsIntegrallyClosed (X.presheaf.stalk x)]
    {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (φ : X.presheaf.stalk x →+* Ω) [IsLocalHom φ] :
    Spec (.of (FractionRing (geometricStalk (Spec.map (CommRingCat.ofHom φ))))) ⟶
      D.1.supportComplement
theorem

geometricStalkFractionFieldToComplement_comp_ι

L81 ↗
EtaleFundamentalGroups.StrictHenselian.geometricStalkFractionFieldToComplement_comp_ι
Documentation

The constructed morphism has the original local structure morphism as its composite with the open inclusion.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.StrictHenselian
universe u
Lean source · statement
theorem geometricStalkFractionFieldToComplement_comp_ι
    {X : Scheme.{u}} (D : X.EffectiveCartierDivisor) (x : X)
    [IsDomain (X.presheaf.stalk x)] [IsIntegrallyClosed (X.presheaf.stalk x)]
    {Ω : Type u} [Field Ω] [IsSepClosed Ω]
    (φ : X.presheaf.stalk x →+* Ω) [IsLocalHom φ] :
    geometricStalkFractionFieldToComplement D x φ ≫ D.1.supportComplement.ι =
      Spec.map (CommRingCat.ofHom
        ((algebraMap (geometricStalk (Spec.map (CommRingCat.ofHom φ)))
          (FractionRing (geometricStalk (Spec.map (CommRingCat.ofHom φ))))).comp
            (geometricStalkStructureMap φ))) ≫ X.fromSpecStalk x
def

cartierComponentStrictHenselianGenericMorphism

L96 ↗
EtaleFundamentalGroups.StrictHenselian.cartierComponentStrictHenselianGenericMorphism
Documentation

At a regular Cartier component, the residue map into its algebraic closure constructs the strict-Henselian generic point used for divisorial inertia. The DVR properties are derived from regularity along the boundary.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace EtaleFundamentalGroups.StrictHenselian
universe u
Lean source · full declaration
def cartierComponentStrictHenselianGenericMorphism
    {X : Scheme.{u}} [IsLocallyNoetherian X]
    (D : X.EffectiveCartierDivisor) (hreg : D.IsAmbientRegularAlongSupport)
    (Z : Set D.1.subscheme) (hZ : Z ∈ irreducibleComponents D.1.subscheme) :
    let x := D.1.componentGenericPoint Z hZ
    let φ := (algebraMap (IsLocalRing.ResidueField (X.presheaf.stalk x))
      (AlgebraicClosure (IsLocalRing.ResidueField (X.presheaf.stalk x)))).comp
      (IsLocalRing.residue (X.presheaf.stalk x))
    Spec (.of (FractionRing (geometricStalk (Spec.map (CommRingCat.ofHom φ))))) ⟶
      D.1.supportComplement := by
  intro x φ
  letI : IsDomain (X.presheaf.stalk x) := isDomain_stalk_componentGenericPoint D hreg Z hZ
  letI : IsDiscreteValuationRing (X.presheaf.stalk x) :=
    isDiscreteValuationRing_stalk_componentGenericPoint D hreg Z hZ
  letI : IsLocalHom φ := RingHom.isLocalHom_comp
    (algebraMap (IsLocalRing.ResidueField (X.presheaf.stalk x))
      (AlgebraicClosure (IsLocalRing.ResidueField (X.presheaf.stalk x))))
    (IsLocalRing.residue (X.presheaf.stalk x))
  exact geometricStalkFractionFieldToComplement D x φ

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