NYLL
Module

CartierLocalFractionField.lean

Nyll.EtaleFundamentalGroups.Inertia.CartierLocalFractionField
3 declarations indexed from sourceView source ↗

Module documentation

The local fraction field as a point of the Cartier complement

At a point whose stalk is a domain, a local Cartier equation remains a nonzero element in the fraction field. Consequently the canonical map from the spectrum of that field to the ambient scheme factors through the complement of the Cartier support. The factorization is constructed with the open immersion's universal property and its composite is proved to be the canonical fraction-field-to-stalk morphism.

At the generic point of a boundary component, the required domain instance is supplied by isDomain_stalk_componentGenericPoint, proved from the paper's regularity-along-the-boundary assumption. This map allows actual finite etale covers of the complement to be pulled back to the local fraction field; it is not additional comparison data.

Imports4
Imported by4

Declarations

theorem

fractionStalkPoint_mem_supportComplement

L40 ↗
AlgebraicGeometry.Scheme.IdealSheafData.IsEffectiveCartier.fractionStalkPoint_mem_supportComplement
Documentation

The local fraction-field point misses every effective Cartier support.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace AlgebraicGeometry.Scheme.IdealSheafData
universe u
variable {X : Scheme.{u}} {I : X.IdealSheafData}
Lean source · statement
theorem IsEffectiveCartier.fractionStalkPoint_mem_supportComplement
    (hI : I.IsEffectiveCartier) (x : X) [IsDomain (X.presheaf.stalk x)]
    (y : Spec (.of (FractionRing (X.presheaf.stalk x)))) :
    (Spec.map (CommRingCat.ofHom
        (algebraMap (X.presheaf.stalk x)
          (FractionRing (X.presheaf.stalk x)))) ≫ X.fromSpecStalk x) y ∈
      I.supportComplement
def

fractionStalkToSupportComplement

L77 ↗
AlgebraicGeometry.Scheme.IdealSheafData.IsEffectiveCartier.fractionStalkToSupportComplement
Documentation

The canonical local fraction-field map, factored through the actual open complement of an effective Cartier divisor.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace AlgebraicGeometry.Scheme.IdealSheafData
universe u
variable {X : Scheme.{u}} {I : X.IdealSheafData}
Lean source · statement
def IsEffectiveCartier.fractionStalkToSupportComplement
    (hI : I.IsEffectiveCartier) (x : X) [IsDomain (X.presheaf.stalk x)] :
    Spec (.of (FractionRing (X.presheaf.stalk x))) ⟶ I.supportComplement
theorem

fractionStalkToSupportComplement_comp_ι

L90 ↗
AlgebraicGeometry.Scheme.IdealSheafData.IsEffectiveCartier.fractionStalkToSupportComplement_comp_ι
Documentation

The constructed local map lies over the canonical map to X.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory
namespace AlgebraicGeometry.Scheme.IdealSheafData
universe u
variable {X : Scheme.{u}} {I : X.IdealSheafData}
Lean source · statement
theorem IsEffectiveCartier.fractionStalkToSupportComplement_comp_ι
    (hI : I.IsEffectiveCartier) (x : X) [IsDomain (X.presheaf.stalk x)] :
    hI.fractionStalkToSupportComplement x ≫ I.supportComplement.ι =
      Spec.map (CommRingCat.ofHom
        (algebraMap (X.presheaf.stalk x)
          (FractionRing (X.presheaf.stalk x)))) ≫ X.fromSpecStalk x

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