Module

SchemeHeightTwoPrime.lean

Nyll.EtaleFundamentalGroups.Kummer.NormalCrossings.SchemeHeightTwoPrime

3 declarations indexed from sourceView source ↗

Module documentation

Height-two arithmetic specializations of normal-crossings branches

At a strict-normal-crossings point, a height-one boundary prime is one of the active parameter ideals. A positive integer which is noninvertible on that branch then produces a height-two prime containing the branch. This is the intrinsic codimension-two reduction used by local ramification arguments; the height-two prime is a conclusion, not input data.

Imports3

Imported by2

theorem

exists_heightTwoPrime_of_branch_nonunit_natCast

L34 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IsStrictNormalCrossingsAt.exists_heightTwoPrime_of_branch_nonunit_natCast

Documentation

A positive integer which is noninvertible on a height-one branch at a strict-normal-crossings point cuts out a height-two specialization of that branch. No finite-type, Nagata, or arithmetic-base hypothesis is used.

Source context 5 commands

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

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

Lean source · statement

theorem IsStrictNormalCrossingsAt.exists_heightTwoPrime_of_branch_nonunit_natCast
    (hI : I.IsStrictNormalCrossingsAt x)
    (q : Ideal (X.presheaf.stalk x)) [q.IsPrime]
    (hqheight : q.height = 1)
    (hIq : I.stalkIdeal x ≤ q)
    (e : ℕ) (he : 0 < e)
    [CharZero (X.presheaf.stalk x ⧸ q)]
    (he_nonunit : ¬ IsUnit (e : X.presheaf.stalk x ⧸ q)) :
    ∃ (P : Ideal (X.presheaf.stalk x)) (_ : P.IsPrime),
      q < P ∧ P.height = 2 ∧
        ¬ IsUnit
          (algebraMap (X.presheaf.stalk x) (Localization.AtPrime P)
            (e : X.presheaf.stalk x))

theorem

exists_heightTwoPrime_of_branch_residueCharacteristic

L70 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IsStrictNormalCrossingsAt.exists_heightTwoPrime_of_branch_residueCharacteristic

Documentation

A positive residue characteristic reached from a height-one branch produces a height-two specialization of that branch. Noninvertibility of the characteristic is derived from the residue-field map.

Source context 5 commands

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

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

Lean source · statement

theorem IsStrictNormalCrossingsAt.exists_heightTwoPrime_of_branch_residueCharacteristic
    (hI : I.IsStrictNormalCrossingsAt x)
    (q : Ideal (X.presheaf.stalk x)) [q.IsPrime]
    (hqheight : q.height = 1)
    (hIq : I.stalkIdeal x ≤ q)
    {k : Type uk} [CommRing k] [Nontrivial k]
    (phi : (X.presheaf.stalk x ⧸ q) →+* k)
    (p : ℕ) [CharZero (X.presheaf.stalk x ⧸ q)]
    [CharP k p] (hp : p.Prime) :
    ∃ (P : Ideal (X.presheaf.stalk x)) (_ : P.IsPrime),
      q < P ∧ P.height = 2 ∧
        ¬ IsUnit
          (algebraMap (X.presheaf.stalk x) (Localization.AtPrime P)
            (p : X.presheaf.stalk x))

theorem

exists_heightTwoPrime_of_branch_residueCharacteristic

L98 ↗

AlgebraicGeometry.Scheme.IdealSheafData.IsStrictNormalCrossings.exists_heightTwoPrime_of_branch_residueCharacteristic

Documentation

Global strict normal crossings supplies the pointwise height-two specialization above any height-one branch containing the boundary stalk ideal. Membership of the point in the boundary support is derived from that containment.

Source context 5 commands

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

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

Lean source · statement

theorem IsStrictNormalCrossings.exists_heightTwoPrime_of_branch_residueCharacteristic
    (hI : I.IsStrictNormalCrossings)
    (q : Ideal (X.presheaf.stalk x)) [q.IsPrime]
    (hqheight : q.height = 1)
    (hIq : I.stalkIdeal x ≤ q)
    {k : Type uk} [CommRing k] [Nontrivial k]
    (phi : (X.presheaf.stalk x ⧸ q) →+* k)
    (p : ℕ) [CharZero (X.presheaf.stalk x ⧸ q)]
    [CharP k p] (hp : p.Prime) :
    ∃ (P : Ideal (X.presheaf.stalk x)) (_ : P.IsPrime),
      q < P ∧ P.height = 2 ∧
        ¬ IsUnit
          (algebraMap (X.presheaf.stalk x) (Localization.AtPrime P)
            (p : X.presheaf.stalk x))

Module documentation

Height-two arithmetic specializations of normal-crossings branches

Declarations

exists_heightTwoPrime_of_branch_nonunit_natCast

exists_heightTwoPrime_of_branch_residueCharacteristic

exists_heightTwoPrime_of_branch_residueCharacteristic