NYLL
Module

IndexAbsorption.lean

Nyll.SchemeTheory.AbhyankarLemma.TameRamification.Book.IndexAbsorption
3 declarations indexed from sourceView source ↗

Module documentation

Classical Abhyankar index absorption for book valuations

The value subgroup of the actual compositum is generated by the two lower value subgroups. Since the target value group is discrete cyclic, the two upper subgroup indices are coprime. Multiplicativity in the two towers then gives the classical e / gcd bound.

Imports30
Imported by2

Declarations

theorem

bookAbhyankarIndexBound_commonTop_of_finiteTame

L58 ↗
TameAbhyankar.bookAbhyankarIndexBound_commonTop_of_finiteTame
Documentation

The classical Abhyankar ramification-index bound on the actual compositum, in the exponential-valuation presentation.

Source context 5 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open AlgebraicNumberTheory.Valuations
open DiscreteValuationField.FieldCompositum
Lean source · full declaration
theorem bookAbhyankarIndexBound_commonTop_of_finiteTame
    {K Omega : Type u} [Field K] [Field Omega] [Algebra K Omega]
    [Algebra.IsAlgebraic K Omega]
    (L K' : IntermediateField K Omega)
    [FiniteDimensional K L] [FiniteDimensional K K']
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation Omega)
    (hExt : forall a : K, w (algebraMap K Omega a) = v a)
    (hhens : ValuationTheory.DiscreteValuationField.HenselianValuationByFactorization
      (LubinTate.Valuations.exponentialValuationSubringAsValuationSubring v).valuation)
    (hTame : FiniteTamelyRamifiedExtension v
      (exponentialValuationRestrict w L)
      (exponentialValuationRestrict_extends v w hExt L))
    (hwTopDiscrete :
      let Top := (L ⊔ K' : IntermediateField K Omega)
      LubinTate.Valuations.DiscreteExponentialValuation
        (exponentialValuationRestrict w Top)) :
    let Top := (L ⊔ K' : IntermediateField K Omega)
    let wLeft := exponentialValuationRestrict w L
    let wRight := exponentialValuationRestrict w K'
    let wTop := exponentialValuationRestrict w Top
    AbhyankarIndexBound
      (exponentialRamificationIndex v wLeft)
      (exponentialRamificationIndex v wRight)
      (exponentialRamificationIndex wRight wTop) := by
  let Top := (L ⊔ K' : IntermediateField K Omega)
  let wLeft := exponentialValuationRestrict w L
  let wRight := exponentialValuationRestrict w K'
  let wTop := exponentialValuationRestrict w Top
  let hLeft := exponentialValuationRestrict_extends v w hExt L
  let hBaseRight := exponentialValuationRestrict_extends v w hExt K'
  let hRightTop : forall a : K',
      wTop (algebraMap K' Top a) = wRight a := by
    intro a
    rfl
  let hLeftTop : forall a : L,
      wTop (algebraMap L Top a) = wLeft a := by
    intro a
    rfl
  let : FiniteDimensional K' Top :=
    finiteDimensional_sup_over_right L K'
  let : FiniteDimensional L Top :=
    DiscreteValuationField.FieldCompositum.finiteDimensional_sup_over_left L K'
  have hvalue :=
    bookExponentialValueSubgroup_commonTop_eq_sup_of_finiteTame
      L K' v w hExt hhens hTame
  have hcop : Nat.Coprime
      (exponentialRamificationIndex wRight wTop)
      (exponentialRamificationIndex wLeft wTop) :=
    bookRamificationIndex_coprime_of_valueSubgroup_sup_eq
      wRight wLeft wTop hwTopDiscrete (by
        simpa [sup_comm] using hvalue.symm)
  have hrightTower :
      exponentialRamificationIndex v wRight *
          exponentialRamificationIndex wRight wTop =
        exponentialRamificationIndex v wTop :=
    exponentialRamificationIndex_mul_in_tower
      v wRight wTop hBaseRight hRightTop
  have hleftTower :
      exponentialRamificationIndex v wLeft *
          exponentialRamificationIndex wLeft wTop =
        exponentialRamificationIndex v wTop :=
    exponentialRamificationIndex_mul_in_tower
      v wLeft wTop hLeft hLeftTop
  have hsquare :
      exponentialRamificationIndex v wRight *
          exponentialRamificationIndex wRight wTop =
        exponentialRamificationIndex v wLeft *
          exponentialRamificationIndex wLeft wTop :=
    hrightTower.trans hleftTower.symm
  have hrightDvd : exponentialRamificationIndex wRight wTop ∣
      exponentialRamificationIndex v wLeft := by
    apply hcop.dvd_of_dvd_mul_right
    refine ⟨exponentialRamificationIndex v wRight, ?_⟩
    simpa [mul_comm] using hsquare.symm
  have hleftTopDvd : exponentialRamificationIndex wLeft wTop ∣
      exponentialRamificationIndex v wRight := by
    apply hcop.symm.dvd_of_dvd_mul_right
    refine ⟨exponentialRamificationIndex v wLeft, ?_⟩
    simpa [mul_comm] using hsquare
  exact TameAbhyankar.abhyankarIndexBound_of_mul_eq_mul_of_dvd_of_dvd_of_coprime
    (bookRamificationIndex_pos v wRight hBaseRight)
    (bookRamificationIndex_pos wRight wTop hRightTop)
    (bookRamificationIndex_pos wLeft wTop hLeftTop)
    hsquare hrightDvd hleftTopDvd hcop
theorem

bookRamificationIndex_commonTop_dvd_div_gcd_of_finiteTame

L145 ↗
TameAbhyankar.bookRamificationIndex_commonTop_dvd_div_gcd_of_finiteTame
Documentation

Literal divisibility form of the classical Abhyankar bound.

Source context 5 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open AlgebraicNumberTheory.Valuations
open DiscreteValuationField.FieldCompositum
Lean source · full declaration
theorem bookRamificationIndex_commonTop_dvd_div_gcd_of_finiteTame
    {K Omega : Type u} [Field K] [Field Omega] [Algebra K Omega]
    [Algebra.IsAlgebraic K Omega]
    (L K' : IntermediateField K Omega)
    [FiniteDimensional K L] [FiniteDimensional K K']
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation Omega)
    (hExt : forall a : K, w (algebraMap K Omega a) = v a)
    (hhens : ValuationTheory.DiscreteValuationField.HenselianValuationByFactorization
      (LubinTate.Valuations.exponentialValuationSubringAsValuationSubring v).valuation)
    (hTame : FiniteTamelyRamifiedExtension v
      (exponentialValuationRestrict w L)
      (exponentialValuationRestrict_extends v w hExt L))
    (hwTopDiscrete :
      let Top := (L ⊔ K' : IntermediateField K Omega)
      LubinTate.Valuations.DiscreteExponentialValuation
        (exponentialValuationRestrict w Top)) :
    let Top := (L ⊔ K' : IntermediateField K Omega)
    let wLeft := exponentialValuationRestrict w L
    let wRight := exponentialValuationRestrict w K'
    let wTop := exponentialValuationRestrict w Top
    exponentialRamificationIndex wRight wTop ∣
      exponentialRamificationIndex v wLeft /
        Nat.gcd (exponentialRamificationIndex v wLeft)
          (exponentialRamificationIndex v wRight) := by
  exact bookAbhyankarIndexBound_commonTop_of_finiteTame
    L K' v w hExt hhens hTame hwTopDiscrete
theorem

bookRamificationIndex_commonTop_eq_one_of_finiteTame_of_dvd

L175 ↗
TameAbhyankar.bookRamificationIndex_commonTop_eq_one_of_finiteTame_of_dvd
Documentation

If the base-change ramification index absorbs the original tame index, the upper-right Book ramification index is one.

Source context 5 commands

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

noncomputable section
universe u
namespace TameAbhyankar
open AlgebraicNumberTheory.Valuations
open DiscreteValuationField.FieldCompositum
Lean source · full declaration
theorem bookRamificationIndex_commonTop_eq_one_of_finiteTame_of_dvd
    {K Omega : Type u} [Field K] [Field Omega] [Algebra K Omega]
    [Algebra.IsAlgebraic K Omega]
    (L K' : IntermediateField K Omega)
    [FiniteDimensional K L] [FiniteDimensional K K']
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation Omega)
    (hExt : forall a : K, w (algebraMap K Omega a) = v a)
    (hhens : ValuationTheory.DiscreteValuationField.HenselianValuationByFactorization
      (LubinTate.Valuations.exponentialValuationSubringAsValuationSubring v).valuation)
    (hTame : FiniteTamelyRamifiedExtension v
      (exponentialValuationRestrict w L)
      (exponentialValuationRestrict_extends v w hExt L))
    (hwTopDiscrete :
      let Top := (L ⊔ K' : IntermediateField K Omega)
      LubinTate.Valuations.DiscreteExponentialValuation
        (exponentialValuationRestrict w Top))
    (hdiv : exponentialRamificationIndex v
        (exponentialValuationRestrict w L) ∣
      exponentialRamificationIndex v
        (exponentialValuationRestrict w K')) :
    let Top := (L ⊔ K' : IntermediateField K Omega)
    exponentialRamificationIndex
      (exponentialValuationRestrict w K')
      (exponentialValuationRestrict w Top) = 1 := by
  let wLeft := exponentialValuationRestrict w L
  let hLeft := exponentialValuationRestrict_extends v w hExt L
  exact eq_one_of_abhyankarIndexBound_of_dvd
    (bookRamificationIndex_pos v wLeft hLeft)
    (bookAbhyankarIndexBound_commonTop_of_finiteTame
      L K' v w hExt hhens hTame hwTopDiscrete) hdiv

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