NYLL
Module

RadicalRepresentatives.lean

Nyll.SchemeTheory.AbhyankarLemma.Kummer.RadicalRepresentatives
5 declarations indexed from sourceView source ↗

Module documentation

Corrected radical representatives for tame extensions

This file carries out the second concrete step in the tame-generation proof. A representative of each actual value-group coset is corrected first by a base element and then by a principal-unit root. The result has the same value coset and a prime-to-residue-characteristic power in the base field.

Imports1
Imported by2

Declarations

instance

exponentialValueGroupQuotientAddCommGroupRadicals

L29 ↗
AlgebraicNumberTheory.Valuations.exponentialValueGroupQuotientAddCommGroupRadicals
Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations
section CorrectedRadicals
variable {K L : Type u} [Field K] [Field L] [Algebra K L]
Lean source · statement
instance exponentialValueGroupQuotientAddCommGroupRadicals
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L) :
    AddCommGroup (ExponentialValueGroupQuotient v w)
theorem

residueCharacteristic_eq_of_exact_extension

L37 ↗
AlgebraicNumberTheory.Valuations.residueCharacteristic_eq_of_exact_extension
Documentation

Exact extensions of exponential valuations have the same actual residue characteristic.

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations
section CorrectedRadicals
variable {K L : Type u} [Field K] [Field L] [Algebra K L]
@[reducible] local instance exponentialValueGroupQuotientAddCommGroupRadicals
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L) :
    AddCommGroup (ExponentialValueGroupQuotient v w) :=
  QuotientAddGroup.Quotient.addCommGroup _
Lean source · statement
theorem residueCharacteristic_eq_of_exact_extension
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a) :
    residueCharacteristic v = residueCharacteristic w
theorem

exists_base_element_mul_value_eq_of_exponentialValueCoset_eq

L54 ↗
AlgebraicNumberTheory.Valuations.exists_base_element_mul_value_eq_of_exponentialValueCoset_eq
Documentation

Equality of actual value cosets can be cross-multiplied by a nonzero base element. This is the converse direction needed when the corrected radical representatives are used to recover the whole target value group.

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations
section CorrectedRadicals
variable {K L : Type u} [Field K] [Field L] [Algebra K L]
@[reducible] local instance exponentialValueGroupQuotientAddCommGroupRadicals
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L) :
    AddCommGroup (ExponentialValueGroupQuotient v w) :=
  QuotientAddGroup.Quotient.addCommGroup _
Lean source · statement
theorem exists_base_element_mul_value_eq_of_exponentialValueCoset_eq
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    {x y : L} (hx : x ≠ 0) (hy : y ≠ 0)
    (hcoset : exponentialValueCoset v w x hx = exponentialValueCoset v w y hy) :
    ∃ t : K, t ≠ 0 ∧ w x = w (algebraMap K L t * y)
theorem

exists_prime_to_radical_representing_valueCoset

L86 ↗
AlgebraicNumberTheory.Valuations.exists_prime_to_radical_representing_valueCoset
Documentation

Every actual value-group coset in a finite prime-to-p extension has a representative alpha whose positive prime-to-p power lies in the base field. This is the corrected radical used in tame generation.

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations
section CorrectedRadicals
variable {K L : Type u} [Field K] [Field L] [Algebra K L]
@[reducible] local instance exponentialValueGroupQuotientAddCommGroupRadicals
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L) :
    AddCommGroup (ExponentialValueGroupQuotient v w) :=
  QuotientAddGroup.Quotient.addCommGroup _
Lean source · statement
theorem exists_prime_to_radical_representing_valueCoset
    [FiniteDimensional K L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (hhens : ValuationTheory.DiscreteValuationField.HenselianValuationByFactorization
      (LubinTate.Valuations.exponentialValuationSubringAsValuationSubring v).valuation)
    (hp : PositiveResidueCharacteristic v)
    (hdegree : Nat.Coprime (Module.finrank K L)
      (residueCharacteristic v))
    (hresidue : Function.Surjective (tameResidueFieldMap v w hExt))
    (q : ExponentialValueGroupQuotient v w) :
    ∃ (m : ℕ) (a : K) (alpha : L),
      0 < m ∧
        Nat.Coprime m (residueCharacteristic v) ∧
          alpha ^ m = algebraMap K L a ∧
            ∃ halpha0 : alpha ≠ 0,
              exponentialValueCoset v w alpha halpha0 = q
theorem

maximalUnramifiedSubextension_residueMap_surjective_of_separable

L257 ↗
AlgebraicNumberTheory.Valuations.maximalUnramifiedSubextension_residueMap_surjective_of_separable
Documentation

If the ambient residue extension is separable, the maximal-residue theorem says that the residue map from the maximal unramified subextension onto the ambient residue field is surjective.

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations
section MaximalUnramifiedResidue
variable {K L : Type u} [Field K] [Field L] [Algebra K L]
variable [Algebra.IsAlgebraic K L]
Lean source · full declaration
theorem maximalUnramifiedSubextension_residueMap_surjective_of_separable
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (hhens : ValuationTheory.DiscreteValuationField.HenselianValuationByFactorization
      (LubinTate.Valuations.exponentialValuationSubringAsValuationSubring v).valuation)
    (hsep : ResidueExtensionIsSeparable v w hExt) :
    let T := maximalUnramifiedSubextension v w hExt
    let wT := exponentialValuationRestrict w T
    let hT : ∀ a : T, w (algebraMap T L a) = wT a := by
      intro a
      rfl
    Function.Surjective (tameResidueFieldMap wT w hT) := by
  classical
  let T := maximalUnramifiedSubextension v w hExt
  let wT := exponentialValuationRestrict w T
  let hT : ∀ a : T, w (algebraMap T L a) = wT a := by
    intro a
    rfl
  let V := LubinTate.Valuations.exponentialValuationSubring v
  let VT := LubinTate.Valuations.exponentialValuationSubring wT
  let W := LubinTate.Valuations.exponentialValuationSubring w
  let i := unramifiedValuationRingValuationRingMap v wT
    (exponentialValuationRestrict_extends v w hExt T)
  let b := unramifiedValuationRingValuationRingMap v w hExt
  let : IsLocalHom i :=
    unramifiedValuationRingValuationRingMap_isLocalHom v wT
      (exponentialValuationRestrict_extends v w hExt T)
  let : IsLocalHom b :=
    unramifiedValuationRingValuationRingMap_isLocalHom v w hExt
  let k := IsLocalRing.ResidueField V
  let kT := IsLocalRing.ResidueField VT
  let ell := IsLocalRing.ResidueField W
  let : Algebra k kT := (IsLocalRing.ResidueField.map i).toAlgebra
  let : Algebra k ell := (IsLocalRing.ResidueField.map b).toAlgebra
  have hrange :=
    maximalUnramifiedSubextension_residue_fieldRange_eq_separableClosure
      v w hExt hhens
  simp only at hrange
  have htop : separableClosure k ell = ⊤ :=
    (separableClosure.eq_top_iff (F := k) (E := ell)).2 hsep
  rw [htop] at hrange
  have hsur : Function.Surjective
      (restrictedResidueAlgHomToAmbient v w hExt T) :=
    AlgHom.fieldRange_eq_top.mp hrange
  simp only
  exact hsur

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