NYLL
Module

RamificationProduct.lean

Nyll.EtaleFundamentalGroups.Normalization.Branch.RamificationProduct
14 declarations indexed from sourceView source ↗

Module documentation

Products of the actual ramification indices above a boundary branch

For a finite normalization, the product of the ramification indices of all primes above one height-one branch is a common multiple of exactly the local ramification indices which must be cancelled by the Abhyankar root cover. Unlike a factorial of the total field degree, this product contains no unramified residue-degree factors.

Imports5
Imported by3

Declarations

def

finitePrimesOverFintype

L30 ↗
EtaleFundamentalGroups.finitePrimesOverFintype
Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uR uS uA uK uL
Lean source · statement
def finitePrimesOverFintype
    {R : Type uR} {S : Type uS}
    [CommRing R] [CommRing S] [Algebra R S]
    [Algebra.QuasiFinite R S] (p : Ideal R) :
    Fintype (p.primesOver S)
def

branchRamificationProduct

L39 ↗
EtaleFundamentalGroups.branchRamificationProduct
Documentation

The product of the actual ramification indices of all primes of S above p.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uR uS uA uK uL
Lean source · statement
def branchRamificationProduct
    {R : Type uR} {S : Type uS}
    [CommRing R] [CommRing S] [Algebra R S]
    [Algebra.QuasiFinite R S] (p : Ideal R) : ℕ
theorem

ramificationIdx_dvd_branchRamificationProduct

L47 ↗
EtaleFundamentalGroups.ramificationIdx_dvd_branchRamificationProduct
Documentation

Every actual ramification index above p divides the branch product.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uR uS uA uK uL
Lean source · statement
theorem ramificationIdx_dvd_branchRamificationProduct
    {R : Type uR} {S : Type uS}
    [CommRing R] [CommRing S] [Algebra R S]
    [Algebra.QuasiFinite R S]
    (p : Ideal R) (q : p.primesOver S) :
    q.1.ramificationIdx R ∣ branchRamificationProduct (S := S) p
theorem

branchRamificationProduct_pos

L60 ↗
EtaleFundamentalGroups.branchRamificationProduct_pos
Documentation

For a finite extension, the branch ramification product is positive.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uR uS uA uK uL
Lean source · statement
theorem branchRamificationProduct_pos
    {R : Type uR} {S : Type uS}
    [CommRing R] [CommRing S] [Algebra R S]
    [Module.Finite R S]
    (p : Ideal R) :
    0 < branchRamificationProduct (S := S) p
def

normalizationBranchRamificationProduct

L73 ↗
EtaleFundamentalGroups.normalizationBranchRamificationProduct
Documentation

The branch product for a height-one prime of a regular model, computed in the canonical DVR localization and its normalization in L.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uR uS uA uK uL
Lean source · statement
def normalizationBranchRamificationProduct
    {A : Type uA} {K : Type uK} {L : Type uL}
    [CommRing A] [IsDomain A] [IsRegularRing A]
    [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    (p : Ideal A) [p.IsPrime] (hp : p.height = 1) : ℕ
theorem

normalizationBranchRamificationProduct_pos

L100 ↗
EtaleFundamentalGroups.normalizationBranchRamificationProduct_pos
Documentation

The branch product is positive.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uR uS uA uK uL
Lean source · statement
theorem normalizationBranchRamificationProduct_pos
    {A : Type uA} {K : Type uK} {L : Type uL}
    [CommRing A] [IsDomain A] [IsRegularRing A]
    [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    (p : Ideal A) [p.IsPrime] (hp : p.height = 1) :
    0 < normalizationBranchRamificationProduct
      (K := K) (L := L) p hp
theorem

normalizationPrime_ramificationIdx_dvd_branchRamificationProduct

L132 ↗
EtaleFundamentalGroups.normalizationPrime_ramificationIdx_dvd_branchRamificationProduct
Documentation

The ramification index of a chosen normalization prime divides the branch product computed after localizing at its height-one contraction.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uR uS uA uK uL
Lean source · statement
theorem normalizationPrime_ramificationIdx_dvd_branchRamificationProduct
    {A : Type uA} {K : Type uK} {L : Type uL}
    [CommRing A] [IsDomain A] [IsRegularRing A]
    [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    (p : Ideal A) [p.IsPrime] (hp : p.height = 1)
    (Q : Ideal (integralClosure A L)) [Q.IsPrime] [Q.LiesOver p] :
    Q.ramificationIdx A ∣
      normalizationBranchRamificationProduct
        (K := K) (L := L) p hp
def

normalizationPrimeElementRamificationProduct

L178 ↗
EtaleFundamentalGroups.normalizationPrimeElementRamificationProduct
Documentation

The branch product attached directly to a prime element.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uR uS uA uK uL
Lean source · statement
def normalizationPrimeElementRamificationProduct
    {A : Type uA} {K : Type uK} {L : Type uL}
    [CommRing A] [IsDomain A] [IsRegularRing A]
    [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    (t : A) (ht : Prime t) : ℕ
theorem

normalizationPrimeElementRamificationProduct_pos

L194 ↗
EtaleFundamentalGroups.normalizationPrimeElementRamificationProduct_pos
Documentation

A prime element's branch product is positive.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uR uS uA uK uL
Lean source · statement
theorem normalizationPrimeElementRamificationProduct_pos
    {A : Type uA} {K : Type uK} {L : Type uL}
    [CommRing A] [IsDomain A] [IsRegularRing A]
    [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    (t : A) (ht : Prime t) :
    0 < normalizationPrimeElementRamificationProduct
      (K := K) (L := L) t ht
theorem

normalizationPrime_ramificationIdx_dvd_primeElementProduct

L213 ↗
EtaleFundamentalGroups.normalizationPrime_ramificationIdx_dvd_primeElementProduct
Documentation

A chosen normalization prime above a prime element has ramification index dividing that element's branch product.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uR uS uA uK uL
Lean source · statement
theorem normalizationPrime_ramificationIdx_dvd_primeElementProduct
    {A : Type uA} {K : Type uK} {L : Type uL}
    [CommRing A] [IsDomain A] [IsRegularRing A]
    [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    (t : A) (ht : Prime t)
    (Q : Ideal (integralClosure A L)) [Q.IsPrime]
    [Q.LiesOver (Ideal.span {t})] :
    Q.ramificationIdx A ∣
      normalizationPrimeElementRamificationProduct
        (K := K) (L := L) t ht
def

splitStrictNormalCrossingsBranchRamificationProduct

L236 ↗
EtaleFundamentalGroups.splitStrictNormalCrossingsBranchRamificationProduct
Documentation

The actual ramification-product exponent on every labelled branch of a split strict-normal-crossings chart; non-boundary parameters receive exponent one.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uR uS uA uK uL
Lean source · statement
def splitStrictNormalCrossingsBranchRamificationProduct
    {A : Type uA} {K : Type uK} {L : Type uL}
    [CommRing A] [IsDomain A] [IsLocalRing A] [IsRegularRing A]
    [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    {d r : ℕ} {f : A} (t : Fin d → A)
    (hNC : IsSplitStrictNormalCrossingsAt f t r) (j : Fin d) : ℕ
theorem

splitStrictNormalCrossingsBranchRamificationProduct_pos

L252 ↗
EtaleFundamentalGroups.splitStrictNormalCrossingsBranchRamificationProduct_pos
Documentation

Every exponent in the strict-normal-crossings branch-product family is positive.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uR uS uA uK uL
Lean source · statement
theorem splitStrictNormalCrossingsBranchRamificationProduct_pos
    {A : Type uA} {K : Type uK} {L : Type uL}
    [CommRing A] [IsDomain A] [IsLocalRing A] [IsRegularRing A]
    [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    {d r : ℕ} {f : A} (t : Fin d → A)
    (hNC : IsSplitStrictNormalCrossingsAt f t r) (j : Fin d) :
    0 < splitStrictNormalCrossingsBranchRamificationProduct
      (K := K) (L := L) t hNC j
theorem

splitStrictNormalCrossingsBranchRamificationProduct_eq

L273 ↗
EtaleFundamentalGroups.splitStrictNormalCrossingsBranchRamificationProduct_eq
Documentation

On a labelled boundary branch, the chart exponent is the corresponding normalization branch product.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uR uS uA uK uL
Lean source · statement
theorem splitStrictNormalCrossingsBranchRamificationProduct_eq
    {A : Type uA} {K : Type uK} {L : Type uL}
    [CommRing A] [IsDomain A] [IsLocalRing A] [IsRegularRing A]
    [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    {d r : ℕ} {f : A} (t : Fin d → A)
    (hNC : IsSplitStrictNormalCrossingsAt f t r)
    (j : Fin d) (hj : j.1 < r) :
    splitStrictNormalCrossingsBranchRamificationProduct
        (K := K) (L := L) t hNC j =
      normalizationPrimeElementRamificationProduct
        (K := K) (L := L) (t j) (hNC.2.2.2.1 j hj)
theorem

normalizationPrime_ramificationIdx_dvd_splitStrictNormalCrossingsProduct

L291 ↗
EtaleFundamentalGroups.normalizationPrime_ramificationIdx_dvd_splitStrictNormalCrossingsProduct
Documentation

A chosen normalization prime's ramification index divides its labelled strict-normal-crossings branch exponent.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uR uS uA uK uL
Lean source · statement
theorem normalizationPrime_ramificationIdx_dvd_splitStrictNormalCrossingsProduct
    {A : Type uA} {K : Type uK} {L : Type uL}
    [CommRing A] [IsDomain A] [IsLocalRing A] [IsRegularRing A]
    [Field K] [Field L]
    [Algebra A K] [IsFractionRing A K]
    [Algebra K L] [Algebra A L] [IsScalarTower A K L]
    [FiniteDimensional K L] [Algebra.IsSeparable K L]
    {d r : ℕ} {f : A} (t : Fin d → A)
    (hNC : IsSplitStrictNormalCrossingsAt f t r)
    (j : Fin d) (hj : j.1 < r)
    (Q : Ideal (integralClosure A L)) [Q.IsPrime]
    [Q.LiesOver (Ideal.span {t j})] :
    Q.ramificationIdx A ∣
      splitStrictNormalCrossingsBranchRamificationProduct
        (K := K) (L := L) t hNC j

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