Nyll.SchemeTheory.Divisors.NormalCrossings.HeightTwo.BranchPair

Module documentation

Two strict-normal-crossings branches at a height-two point

If a height-two prime contains two distinct labelled branches of a split strict-normal-crossings chart, those two branch equations form a regular system of parameters after localization at that prime.

The proof first moves the two indexed occurrences to the front of the given regular system. Their two-term prefix remains weakly regular after localization. For generation, the ideal spanned by the two equations is prime: after quotienting by the first equation, the second is again a member of a regular system and hence is prime. Its height is at least two, so its inclusion in the given height-two prime is an equality.

theorem

regular_pair_localizationAtPrime_of_two_splitStrictNormalCrossingsParameters

L40 ↗

EtaleFundamentalGroups.regular_pair_localizationAtPrime_of_two_splitStrictNormalCrossingsParameters

Documentation

At a height-two point containing two distinct parameters of a split strict normal crossings chart, the two localized parameters are a regular pair and generate the localized maximal ideal. In particular this applies to any two distinct labelled branches through the point.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open IsLocalRing
open RingTheory.Sequence
universe u

Lean source · statement

theorem regular_pair_localizationAtPrime_of_two_splitStrictNormalCrossingsParameters
    {A : Type u} [CommRing A] [IsDomain A] [IsLocalRing A]
    [IsRegularRing A] {d r : ℕ} {f : A} {t : Fin d → A}
    (hNC : IsSplitStrictNormalCrossingsAt f t r)
    (i j : Fin d) (hij : i ≠ j)
    (P : Ideal A) [P.IsPrime] (hP : P.height = 2)
    (htiP : t i ∈ P) (htjP : t j ∈ P) :
    IsRegular (Localization.AtPrime P)
        [algebraMap A (Localization.AtPrime P) (t i),
          algebraMap A (Localization.AtPrime P) (t j)] ∧
      Ideal.ofList
          [algebraMap A (Localization.AtPrime P) (t i),
            algebraMap A (Localization.AtPrime P) (t j)] =
        maximalIdeal (Localization.AtPrime P)

Module documentation

Two strict-normal-crossings branches at a height-two point

Declarations

regular_pair_localizationAtPrime_of_two_splitStrictNormalCrossingsParameters