Module

ActualFactorPrescribedExponent.lean

Nyll.EtaleFundamentalGroups.Kummer.Completions.HigherRadical.ActualFactorPrescribedExponent

2 declarations indexed from sourceView source ↗

Module documentation

Complete higher-radical factors at a prescribed common exponent

The factorial exponent is only one way to obtain a common multiple of local ramification indices. For the absolute Abhyankar argument the useful common multiple is instead built from the actual ramification indices above a boundary divisor. This file keeps the exponent and its divisibility proof explicit while still constructing the target uniformizer and its unit decomposition from the complete-DVF data.

Imports1

Nyll.EtaleFundamentalGroups.Kummer.Completions.HigherRadical.ActualFactor

Imported by2

theorem

exists_higherRadicalActualFactorData_of_completeTarget_of_root

L35 ↗

EtaleFundamentalGroups.Kummer.exists_higherRadicalActualFactorData_of_completeTarget_of_root

Documentation

A prescribed root whose exponent is divisible by the intrinsic ramification index produces the actual finite-etale higher-radical factor.

Unlike the degree-factorial wrapper, the target complete valuation is part of the input. This is the form consumed by the product of the actual ramification indices over a boundary divisor.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Kummer
open ValuationTheory.DiscreteValuationField
open ValuationTheory.DiscreteValuationField.ValuedExtension
universe uK uKv uL uLv

Lean source · statement

theorem exists_higherRadicalActualFactorData_of_completeTarget_of_root
    {K : Type uK} {L : Type uL} [Field K] [Field L] [Algebra K L]
    (base : CompleteDVF.{uK, uKv} K)
    (target : CompleteDVF.{uL, uLv} L)
    [base.valuation.HasExtension target.valuation]
    [CharZero base.residueField]
    [Module.Finite base.valuationSubring target.valuationSubring]
    (varpi : base.valuationSubring)
    (hvarpi : base.valuation.IsUniformizer (varpi : K))
    (N : ℕ)
    (hdiv : ramificationIndex base.toDVF target.toDVF ∣ N)
    (beta : AlgebraicClosure L)
    (hbeta :
      beta ^ N =
        algebraMap K (AlgebraicClosure L) (varpi : K)) :
    ∃ (pi : target.valuationSubring)
        (unit : target.valuationSubringˣ),
      target.valuation.IsUniformizer (pi : L) ∧
        integerMap base.toDVF target.toDVF varpi =
          (unit : target.valuationSubring) *
            pi ^ ramificationIndex base.toDVF target.toDVF ∧
        Nonempty
          (HigherRadicalActualFactorData
            base.toDVF target.toDVF varpi N beta)

theorem

exists_higherRadicalActualFactorData_of_completeTarget

L72 ↗

EtaleFundamentalGroups.Kummer.exists_higherRadicalActualFactorData_of_completeTarget