Module

CartierLocalFractionFieldPullback.lean

Nyll.EtaleFundamentalGroups.Inertia.CartierLocalFractionFieldPullback

1 declaration indexed from sourceView source ↗

Module documentation

The actual fraction-stalk pullback of a Cartier complement

At a divisor point with discrete valuation stalk, the inverse image of the complement is the spectrum of the actual fraction field. The horizontal map is the previously constructed canonical factorization through the complement.

Imports3

Imported by4

theorem

isPullback_fractionStalkToSupportComplement

L29 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IsEffectiveCartier.isPullback_fractionStalkToSupportComplement

Documentation

At a discrete valuation stalk on an effective Cartier divisor, the canonical fraction-field diagram is the pullback of the actual complement.

Source context 4 commands

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

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

Lean source · statement

theorem IsEffectiveCartier.isPullback_fractionStalkToSupportComplement
    {X : Scheme.{u}} {I : X.IdealSheafData}
    (hI : I.IsEffectiveCartier) (x : X) (hx : x ∈ I.support)
    [IsDomain (X.presheaf.stalk x)] [IsDiscreteValuationRing (X.presheaf.stalk x)] :
    IsPullback (hI.fractionStalkToSupportComplement x)
      (Spec.map (CommRingCat.ofHom (algebraMap (X.presheaf.stalk x)
        (FractionRing (X.presheaf.stalk x)))))
      I.supportComplement.ι (X.fromSpecStalk x)

Module documentation

The actual fraction-stalk pullback of a Cartier complement

Declarations

isPullback_fractionStalkToSupportComplement