NYLL
Module

BranchSupport.lean

Nyll.SchemeTheory.Divisors.NormalCrossings.HeightTwo.BranchSupport
2 declarations indexed from sourceView source ↗

Module documentation

Branch support at a height-two strict-normal-crossings point

A height-two prime contains at most two members of a regular system of parameters. Applied to the labelled part of a split strict-normal-crossings chart, this gives the exact dichotomy needed by the local Abhyankar construction: either the selected branch is the only branch through the point, or there is one further branch and every branch through the point is one of those two.

The proof does not use ramification data. Three distinct parameters in the prime would remain a three-term regular sequence after localization, whereas the localized ring has Krull dimension two.

Imports4
Imported by3

Declarations

theorem

eq_left_or_eq_right_of_three_parameters_mem_heightTwo

L39 ↗
EtaleFundamentalGroups.eq_left_or_eq_right_of_three_parameters_mem_heightTwo
Documentation

Three members of a regular system of parameters cannot all lie in a height-two prime. Equivalently, once two distinct parameters in the prime have been fixed, every further parameter in the prime is one of them.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open RingTheory.Sequence
open scoped List
universe u
Lean source · statement
theorem eq_left_or_eq_right_of_three_parameters_mem_heightTwo
    {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)
    (k : Fin d) (htkP : t k ∈ P) :
    k = i ∨ k = j
theorem

splitStrictNormalCrossings_heightTwo_branchSupport

L136 ↗
EtaleFundamentalGroups.splitStrictNormalCrossings_heightTwo_branchSupport
Documentation

Exact branch-support dichotomy at a height-two point containing a selected labelled branch. In the second case the additional branch is distinct from the selected one and exhausts all remaining labelled branches through the point.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
open RingTheory.Sequence
open scoped List
universe u
Lean source · statement
theorem splitStrictNormalCrossings_heightTwo_branchSupport
    {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 : Fin d)
    (P : Ideal A) [P.IsPrime] (hP : P.height = 2)
    (htiP : t i ∈ P) :
    (∀ j : Fin d, j.1 < r → t j ∈ P → j = i) ∨
      ∃ j : Fin d, j.1 < r ∧ j ≠ i ∧ t j ∈ P ∧
        ∀ k : Fin d, k.1 < r → t k ∈ P → k = i ∨ k = j

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