Module

GaloisRamificationIndex.lean

Nyll.EtaleFundamentalGroups.Normalization.Branch.GaloisRamificationIndex

12 declarations indexed from sourceView source ↗

Module documentation

The common branch ramification index in a Galois normalization

For a finite Galois extension, all normalization primes above one height-one branch have the same ramification index. This is the exponent needed by the root cover: unlike the product of all branch indices, it does not introduce a residual radical after selecting one actual branch factor.

Imports2

Mathlib.NumberTheory.RamificationInertia.Galois
Nyll.EtaleFundamentalGroups.Normalization.Branch.RamificationProduct

Imported by3

def

normalizationGaloisBranchRamificationIndex

L27 ↗

EtaleFundamentalGroups.normalizationGaloisBranchRamificationIndex

Documentation

The common ramification index above a height-one prime, computed in its canonical DVR localization.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uK uL

Lean source · statement

def normalizationGaloisBranchRamificationIndex
    {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] [IsGalois K L]
    (p : Ideal A) [p.IsPrime] : ℕ

theorem

ramificationIdxIn_eq_localPrime

L48 ↗

EtaleFundamentalGroups.ramificationIdxIn_eq_localPrime

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uK uL

Lean source · statement

theorem ramificationIdxIn_eq_localPrime
    {V : Type uA} {K : Type uK} {L : Type uL}
    [CommRing V] [IsDomain V] [IsDiscreteValuationRing V]
    [Field K] [Field L]
    [Algebra V K] [IsFractionRing V K]
    [Algebra K L] [Algebra V L] [IsScalarTower V K L]
    [FiniteDimensional K L] [IsGalois K L]
    (q : (IsLocalRing.maximalIdeal V).primesOver (integralClosure V L)) :
    (IsLocalRing.maximalIdeal V).ramificationIdxIn (integralClosure V L) =
      q.1.ramificationIdx V

theorem

localNormalizationPrime_ramificationIdx_eq_galoisBranchIndex

L73 ↗

EtaleFundamentalGroups.localNormalizationPrime_ramificationIdx_eq_galoisBranchIndex

Documentation

Every local normalization prime above the branch has the common Galois ramification index.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uK uL

Lean source · full declaration

theorem localNormalizationPrime_ramificationIdx_eq_galoisBranchIndex
    {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] [IsGalois K L]
    (p : Ideal A) [p.IsPrime] (hp : p.height = 1) :
    let V := Localization.AtPrime p
    letI : Algebra V K :=
      localizationAtPrimeToFractionFieldAlgebra (K := K) p
    letI : Algebra V L :=
      localizationAtPrimeToExtensionAlgebra (K := K) (L := L) p
    letI : IsScalarTower V K L :=
      localizationAtPrimeToFractionFieldToExtension_isScalarTower
        (K := K) (L := L) p
    let S := integralClosure V L
    ∀ q : (IsLocalRing.maximalIdeal V).primesOver S,
      q.1.ramificationIdx V =
        normalizationGaloisBranchRamificationIndex
          (K := K) (L := L) p := by
  dsimp only
  let V := Localization.AtPrime p
  let : Algebra V K :=
    localizationAtPrimeToFractionFieldAlgebra (K := K) p
  let : Algebra V L :=
    localizationAtPrimeToExtensionAlgebra (K := K) (L := L) p
  let : IsScalarTower V K L :=
    localizationAtPrimeToFractionFieldToExtension_isScalarTower
      (K := K) (L := L) p
  let : IsFractionRing V K :=
    localizationAtPrimeToFractionField_isFractionRing (K := K) p
  let : IsDiscreteValuationRing V :=
    isDiscreteValuationRing_localizationAtPrime_of_height_eq_one A p hp
  intro q
  exact (ramificationIdxIn_eq_localPrime
    (V := V) (K := K) (L := L) q).symm

theorem

normalizationGaloisBranchRamificationIndex_pos

L112 ↗

EtaleFundamentalGroups.normalizationGaloisBranchRamificationIndex_pos

Documentation

The common Galois branch index is positive.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uK uL

Lean source · statement

theorem normalizationGaloisBranchRamificationIndex_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] [IsGalois K L]
    (p : Ideal A) [p.IsPrime] (hp : p.height = 1) :
    0 < normalizationGaloisBranchRamificationIndex
      (K := K) (L := L) p

theorem

normalizationPrime_ramificationIdx_eq_galoisBranchIndex

L156 ↗

EtaleFundamentalGroups.normalizationPrime_ramificationIdx_eq_galoisBranchIndex

Documentation

A chosen prime of the original normalization has exactly the common Galois branch ramification index.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uK uL

Lean source · statement

theorem normalizationPrime_ramificationIdx_eq_galoisBranchIndex
    {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] [IsGalois K L]
    (p : Ideal A) [p.IsPrime] (hp : p.height = 1)
    (Q : Ideal (integralClosure A L)) [Q.IsPrime] [Q.LiesOver p] :
    Q.ramificationIdx A =
      normalizationGaloisBranchRamificationIndex
        (K := K) (L := L) p

def

normalizationPrimeElementGaloisRamificationIndex

L196 ↗

EtaleFundamentalGroups.normalizationPrimeElementGaloisRamificationIndex

Documentation

The common Galois ramification index attached to a prime element.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uK uL

Lean source · statement

def normalizationPrimeElementGaloisRamificationIndex
    {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] [IsGalois K L]
    (t : A) (ht : Prime t) : ℕ

theorem

normalizationPrimeElementGaloisRamificationIndex_pos

L210 ↗

EtaleFundamentalGroups.normalizationPrimeElementGaloisRamificationIndex_pos

Documentation

A prime element's common Galois branch index is positive.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uK uL

Lean source · statement

theorem normalizationPrimeElementGaloisRamificationIndex_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] [IsGalois K L]
    (t : A) (ht : Prime t) :
    0 < normalizationPrimeElementGaloisRamificationIndex
      (K := K) (L := L) t ht

theorem

normalizationPrime_ramificationIdx_eq_primeElementGaloisIndex

L229 ↗

EtaleFundamentalGroups.normalizationPrime_ramificationIdx_eq_primeElementGaloisIndex

Documentation

A chosen normalization prime over a prime element has exactly that element's common Galois branch index.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uK uL

Lean source · statement

theorem normalizationPrime_ramificationIdx_eq_primeElementGaloisIndex
    {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] [IsGalois K L]
    (t : A) (ht : Prime t)
    (Q : Ideal (integralClosure A L)) [Q.IsPrime]
    [Q.LiesOver (Ideal.span {t})] :
    Q.ramificationIdx A =
      normalizationPrimeElementGaloisRamificationIndex
        (K := K) (L := L) t ht

def

splitStrictNormalCrossingsGaloisRamificationIndex

L252 ↗

EtaleFundamentalGroups.splitStrictNormalCrossingsGaloisRamificationIndex

Documentation

The actual common Galois 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 uA uK uL

Lean source · statement

def splitStrictNormalCrossingsGaloisRamificationIndex
    {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] [IsGalois K L]
    {d r : ℕ} {f : A} (t : Fin d → A)
    (hNC : IsSplitStrictNormalCrossingsAt f t r) (j : Fin d) : ℕ

theorem

splitStrictNormalCrossingsGaloisRamificationIndex_pos

L267 ↗

EtaleFundamentalGroups.splitStrictNormalCrossingsGaloisRamificationIndex_pos

Documentation

Every strict-normal-crossings Galois branch exponent is positive.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uK uL

Lean source · statement

theorem splitStrictNormalCrossingsGaloisRamificationIndex_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] [IsGalois K L]
    {d r : ℕ} {f : A} (t : Fin d → A)
    (hNC : IsSplitStrictNormalCrossingsAt f t r) (j : Fin d) :
    0 < splitStrictNormalCrossingsGaloisRamificationIndex
      (K := K) (L := L) t hNC j

theorem

splitStrictNormalCrossingsGaloisRamificationIndex_eq

L288 ↗

EtaleFundamentalGroups.splitStrictNormalCrossingsGaloisRamificationIndex_eq

Documentation

On a labelled boundary branch, the chart exponent is the common Galois ramification index.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uK uL

Lean source · statement

theorem splitStrictNormalCrossingsGaloisRamificationIndex_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] [IsGalois K L]
    {d r : ℕ} {f : A} (t : Fin d → A)
    (hNC : IsSplitStrictNormalCrossingsAt f t r)
    (j : Fin d) (hj : j.1 < r) :
    splitStrictNormalCrossingsGaloisRamificationIndex
        (K := K) (L := L) t hNC j =
      normalizationPrimeElementGaloisRamificationIndex
        (K := K) (L := L) (t j) (hNC.2.2.2.1 j hj)

theorem

normalizationPrime_ramificationIdx_eq_splitStrictNormalCrossingsGaloisIndex

L306 ↗

EtaleFundamentalGroups.normalizationPrime_ramificationIdx_eq_splitStrictNormalCrossingsGaloisIndex

Documentation

A chosen normalization prime over a labelled boundary branch has exactly the exponent used by the Galois strict-normal-crossings root cover.

Source context 3 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe uA uK uL

Lean source · statement

theorem
    normalizationPrime_ramificationIdx_eq_splitStrictNormalCrossingsGaloisIndex
    {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] [IsGalois 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} : Set A))] :
    Q.ramificationIdx A =
      splitStrictNormalCrossingsGaloisRamificationIndex
        (K := K) (L := L) t hNC j

Module documentation

The common branch ramification index in a Galois normalization

Declarations