Module

Scheme.lean

Nyll.EtaleFundamentalGroups.Kummer.NormalCrossings.Scheme

5 declarations indexed from sourceView source ↗

Module documentation

Scheme strict-normal-crossings charts and local algebra

This file compares the scheme-theoretic strict-normal-crossings predicate with the explicit local-algebra data used by the Kummer inertia results. The scheme predicate itself produces the regular system, so domain, primality, and regular-local quotient properties are conclusions rather than additional hypotheses.

Imports6

Imported by5

theorem

boundaryProduct_eq_initialParameterProduct

L34 ↗

EtaleFundamentalGroups.boundaryProduct_eq_initialParameterProduct

Documentation

The two finite-product conventions used for an initial segment of a parameter family agree.

Source context 4 commands

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

noncomputable section
open scoped BigOperators
namespace EtaleFundamentalGroups
universe u

Lean source · statement

theorem boundaryProduct_eq_initialParameterProduct
    {R : Type u} [CommMonoid R] {d r : ℕ}
    (t : Fin d → R) (hr : r ≤ d) :
    boundaryProduct t r =
      AlgebraicGeometry.Scheme.initialParameterProduct t r hr

theorem

localParameterGeometry

L75 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IsStrictNormalCrossingsAt.localParameterGeometry

Documentation

A scheme-theoretic strict-normal-crossings chart produces the local domain and branch geometry needed by the explicit Kummer construction.

In particular, primality of a branch parameter and regular-local geometry of its quotient are not separate assumptions.

Source context 6 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicGeometry.Scheme.IdealSheafData
open EtaleFundamentalGroups
universe u
variable {X : Scheme.{u}} {I : X.IdealSheafData} {x : X}

Lean source · statement

theorem IsStrictNormalCrossingsAt.localParameterGeometry
    (hI : I.IsStrictNormalCrossingsAt x) :
    ∃ (d r : ℕ) (t : Fin d → X.presheaf.stalk x),
      0 < r ∧ ∃ (_hr : r ≤ d),
        EtaleFundamentalGroups.IsRegularSystemOfParameters t ∧
          I.stalkIdeal x =
            Ideal.span {EtaleFundamentalGroups.boundaryProduct t r} ∧
          IsDomain (X.presheaf.stalk x) ∧
          (∀ i : Fin d, i.val < r → Prime (t i)) ∧
          (∀ i : Fin d, i.val < r →
            IsDomain
                (X.presheaf.stalk x ⧸ Ideal.span {t i}) ∧
              IsRegularLocalRing
                (X.presheaf.stalk x ⧸ Ideal.span {t i}))

theorem

localSplitChart_of_dimension_two

L126 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IsStrictNormalCrossingsAt.localSplitChart_of_dimension_two

Documentation

At a two-dimensional strict-normal-crossings point, the scheme chart supplies the full explicit split chart required by the Kummer inertia theorem. In dimension two both the ambient regular local domain and each one-dimensional branch quotient are regular rings, so no general regular-local-localization theorem is needed.

Source context 7 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicGeometry.Scheme.IdealSheafData
open EtaleFundamentalGroups
open IsLocalRing
universe u
variable {X : Scheme.{u}} {I : X.IdealSheafData} {x : X}

Lean source · statement

theorem IsStrictNormalCrossingsAt.localSplitChart_of_dimension_two
    (hI : I.IsStrictNormalCrossingsAt x)
    (hdim : ringKrullDim (X.presheaf.stalk x) =
      ((2 : ℕ∞) : WithBot ℕ∞)) :
    ∃ (r : ℕ) (t : Fin 2 → X.presheaf.stalk x),
      IsDomain (X.presheaf.stalk x) ∧
        IsRegularRing (X.presheaf.stalk x) ∧
        I.stalkIdeal x = Ideal.span {boundaryProduct t r} ∧
        EtaleFundamentalGroups.IsSplitStrictNormalCrossingsAt
          (boundaryProduct t r) t r

theorem

localSplitChart_at_fromSpecStalk_of_height_two

L224 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IsStrictNormalCrossings.localSplitChart_at_fromSpecStalk_of_height_two

Documentation

A height-two point of the local scheme lying on a global strict-normal- crossings boundary carries the complete split Kummer chart. The point is represented by an actual prime of 𝒪_{X,x}; its height is transported to the dimension of the corresponding scheme stalk.

Source context 6 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicGeometry.Scheme.IdealSheafData
open EtaleFundamentalGroups
universe u
variable {X : Scheme.{u}} {I : X.IdealSheafData} {x : X}

Lean source · statement

theorem IsStrictNormalCrossings.localSplitChart_at_fromSpecStalk_of_height_two
    (hI : I.IsStrictNormalCrossings)
    (p : Spec (X.presheaf.stalk x))
    (hp : p.asIdeal.height = 2)
    (hpI : X.fromSpecStalk x p ∈ I.support) :
    ∃ (r : ℕ) (t : Fin 2 →
        X.presheaf.stalk (X.fromSpecStalk x p)),
      IsDomain (X.presheaf.stalk (X.fromSpecStalk x p)) ∧
        IsRegularRing (X.presheaf.stalk (X.fromSpecStalk x p)) ∧
        I.stalkIdeal (X.fromSpecStalk x p) =
          Ideal.span {boundaryProduct t r} ∧
        EtaleFundamentalGroups.IsSplitStrictNormalCrossingsAt
          (boundaryProduct t r) t r

theorem

localSplitChart_at_fromSpecStalk_of_height_two_of_stalkIdeal_le

L242 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IsStrictNormalCrossings.localSplitChart_at_fromSpecStalk_of_height_two_of_stalkIdeal_le

Documentation

A height-two prime containing the boundary stalk ideal supplies the same local split Kummer chart, with support membership derived rather than assumed.

Source context 6 commands

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

noncomputable section
open scoped BigOperators
namespace AlgebraicGeometry.Scheme.IdealSheafData
open EtaleFundamentalGroups
universe u
variable {X : Scheme.{u}} {I : X.IdealSheafData} {x : X}

Lean source · statement

theorem IsStrictNormalCrossings.localSplitChart_at_fromSpecStalk_of_height_two_of_stalkIdeal_le
    (hI : I.IsStrictNormalCrossings)
    (p : Spec (X.presheaf.stalk x))
    (hp : p.asIdeal.height = 2)
    (hpI : I.stalkIdeal x ≤ p.asIdeal) :
    ∃ (r : ℕ) (t : Fin 2 →
        X.presheaf.stalk (X.fromSpecStalk x p)),
      IsDomain (X.presheaf.stalk (X.fromSpecStalk x p)) ∧
        IsRegularRing (X.presheaf.stalk (X.fromSpecStalk x p)) ∧
        I.stalkIdeal (X.fromSpecStalk x p) =
          Ideal.span {boundaryProduct t r} ∧
        EtaleFundamentalGroups.IsSplitStrictNormalCrossingsAt
          (boundaryProduct t r) t r

Module documentation

Scheme strict-normal-crossings charts and local algebra

Declarations

boundaryProduct_eq_initialParameterProduct

localParameterGeometry

localSplitChart_of_dimension_two

localSplitChart_at_fromSpecStalk_of_height_two

localSplitChart_at_fromSpecStalk_of_height_two_of_stalkIdeal_le