Module

SingleRadical.lean

Nyll.SchemeTheory.AbhyankarLemma.Kummer.SingleRadical

14 declarations indexed from sourceView source ↗

Module documentation

A single radical in a tame extension

This file proves the root-of-unity descent used in the converse and degree calculation for a single prime-to-residue-characteristic radical.

Imports1

Nyll.SchemeTheory.AbhyankarLemma.Kummer.TameRadicalGeneration

Imported by3

theorem

eq_of_isRoot_of_isRoot_of_residue_eq_of_derivative_isUnit

L26 ↗

AlgebraicNumberTheory.Valuations.eq_of_isRoot_of_isRoot_of_residue_eq_of_derivative_isUnit

Documentation

A simple root in a fixed residue class is unique in any local domain. This is the elementary uniqueness half of Hensel's lemma.

Source context 4 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations

Lean source · statement

theorem eq_of_isRoot_of_isRoot_of_residue_eq_of_derivative_isUnit
    {R : Type u} [CommRing R] [IsDomain R] [IsLocalRing R]
    {f : Polynomial R} {a b : R}
    (ha : f.IsRoot a) (hb : f.IsRoot b)
    (hres : IsLocalRing.residue R b = IsLocalRing.residue R a)
    (hderiv : IsUnit (f.derivative.eval a)) :
    b = a

theorem

exists_rootOfUnity_lift_of_coprime

L79 ↗

AlgebraicNumberTheory.Valuations.exists_rootOfUnity_lift_of_coprime

Documentation

Every prime-to-p residue root of unity has a root-of-unity lift in a Henselian valued field.

Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations
section RootOfUnityLift
variable {K : Type u} [Field K]

Lean source · statement

theorem exists_rootOfUnity_lift_of_coprime
    (v : LubinTate.Valuations.ExponentialValuation K)
    (hhens : ValuationTheory.DiscreteValuationField.HenselianValuationByFactorization
      (LubinTate.Valuations.exponentialValuationSubringAsValuationSubring v).valuation)
    (hp : PositiveResidueCharacteristic v)
    (d : ℕ) (hcop : Nat.Coprime d (residueCharacteristic v))
    (c : IsLocalRing.ResidueField (LubinTate.Valuations.exponentialValuationSubring v))
    (hc : c ^ d = 1) :
    ∃ z : LubinTate.Valuations.exponentialValuationSubring v,
      z ^ d = 1 ∧ IsLocalRing.residue
        (LubinTate.Valuations.exponentialValuationSubring v) z = c

theorem

exists_base_rootOfUnity_eq_of_residue_preimage

L143 ↗

AlgebraicNumberTheory.Valuations.exists_base_rootOfUnity_eq_of_residue_preimage

Documentation

A prime-to-p root of unity whose residue class comes from the base already lies in the Henselian base field.

Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations
section RootOfUnityDescent
variable {K L : Type u} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem exists_base_rootOfUnity_eq_of_residue_preimage
    (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)
    (d : ℕ) (hcop : Nat.Coprime d (residueCharacteristic v))
    (zeta : LubinTate.Valuations.exponentialValuationSubring w)
    (hzetaPow : zeta ^ d = 1)
    (c : IsLocalRing.ResidueField (LubinTate.Valuations.exponentialValuationSubring v))
    (hc : tameResidueFieldMap v w hExt c =
      IsLocalRing.residue (LubinTate.Valuations.exponentialValuationSubring w) zeta) :
    ∃ z : LubinTate.Valuations.exponentialValuationSubring v,
      (unramifiedValuationRingValuationRingMap v w hExt) z = zeta

theorem

exists_base_unit_root_of_target_root_of_residue_preimage

L273 ↗

AlgebraicNumberTheory.Valuations.exists_base_unit_root_of_target_root_of_residue_preimage

Documentation

If a base unit acquires a prime-to-p root whose residue class comes from the base, it already has such a root in the Henselian base.

Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations
section UnitRootDescent
variable {K L : Type u} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem exists_base_unit_root_of_target_root_of_residue_preimage
    (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)
    (d : ℕ) (hcop : Nat.Coprime d (residueCharacteristic v))
    (u : LubinTate.Valuations.exponentialValuationSubring v)
    (huUnit : IsUnit u)
    (delta : LubinTate.Valuations.exponentialValuationSubring w)
    (hdeltaPow : delta ^ d =
      unramifiedValuationRingValuationRingMap v w hExt u)
    (c : IsLocalRing.ResidueField (LubinTate.Valuations.exponentialValuationSubring v))
    (hc : tameResidueFieldMap v w hExt c =
      IsLocalRing.residue (LubinTate.Valuations.exponentialValuationSubring w) delta) :
    ∃ z : LubinTate.Valuations.exponentialValuationSubring v, z ^ d = u

theorem

exists_base_unit_root_of_target_root

L355 ↗

AlgebraicNumberTheory.Valuations.exists_base_unit_root_of_target_root

Documentation

If a base unit acquires a prime-to-p root in an extension with the same residue field, it already has such a root in the Henselian base.

Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations
section UnitRootDescent
variable {K L : Type u} [Field K] [Field L] [Algebra K L]

Lean source · statement

theorem exists_base_unit_root_of_target_root
    (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)
    (hresidue : Function.Surjective (tameResidueFieldMap v w hExt))
    (d : ℕ) (hcop : Nat.Coprime d (residueCharacteristic v))
    (u : LubinTate.Valuations.exponentialValuationSubring v)
    (huUnit : IsUnit u)
    (delta : LubinTate.Valuations.exponentialValuationSubring w)
    (hdeltaPow : delta ^ d =
      unramifiedValuationRingValuationRingMap v w hExt u) :
    ∃ z : LubinTate.Valuations.exponentialValuationSubring v, z ^ d = u

instance

exponentialValueGroupQuotientAddCommGroupSingle

L381 ↗

AlgebraicNumberTheory.Valuations.exponentialValueGroupQuotientAddCommGroupSingle

Source context 6 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations
section SingleRadicalDegree
variable {K L : Type u} [Field K] [Field L] [Algebra K L]

Lean source · statement

instance exponentialValueGroupQuotientAddCommGroupSingle
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L) :
    AddCommGroup (ExponentialValueGroupQuotient v w)

def

SeparableResidueRootLifts

L391 ↗

AlgebraicNumberTheory.Valuations.SeparableResidueRootLifts

Documentation

Every target residue element which is a root of a separable polynomial over the base residue field already comes from the base. A purely inseparable residue extension has this property, and surjectivity is a stronger special case.

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations
section SingleRadicalDegree
variable {K L : Type u} [Field K] [Field L] [Algebra K L]
@[reducible] local instance exponentialValueGroupQuotientAddCommGroupSingle
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L) :
    AddCommGroup (ExponentialValueGroupQuotient v w) :=
  QuotientAddGroup.Quotient.addCommGroup _

Lean source · statement

def SeparableResidueRootLifts
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a) : Prop

theorem

exponentialValueCoset_addOrderOf_dvd_exponent_of_pow_eq_base

L403 ↗

AlgebraicNumberTheory.Valuations.exponentialValueCoset_addOrderOf_dvd_exponent_of_pow_eq_base

Documentation

If a power of a nonzero element lies in the base, the order of its actual value coset divides that exponent.

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations
section SingleRadicalDegree
variable {K L : Type u} [Field K] [Field L] [Algebra K L]
@[reducible] local instance exponentialValueGroupQuotientAddCommGroupSingle
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L) :
    AddCommGroup (ExponentialValueGroupQuotient v w) :=
  QuotientAddGroup.Quotient.addCommGroup _

Lean source · statement

theorem exponentialValueCoset_addOrderOf_dvd_exponent_of_pow_eq_base
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (alpha : L) (halpha0 : alpha ≠ 0)
    (m : ℕ) (a : K) (hpow : alpha ^ m = algebraMap K L a) :
    addOrderOf (exponentialValueCoset v w alpha halpha0) ∣ m

theorem

finrank_eq_addOrderOf_valueCoset_of_single_radical_of_separableResidue

L438 ↗

AlgebraicNumberTheory.Valuations.finrank_eq_addOrderOf_valueCoset_of_single_radical_of_separableResidue

Documentation

If all separable target residue elements descend, a one-generator prime-to-p radical extension has degree equal to the order of the generator's value coset.

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations
section SingleRadicalDegree
variable {K L : Type u} [Field K] [Field L] [Algebra K L]
@[reducible] local instance exponentialValueGroupQuotientAddCommGroupSingle
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L) :
    AddCommGroup (ExponentialValueGroupQuotient v w) :=
  QuotientAddGroup.Quotient.addCommGroup _

Lean source · statement

theorem finrank_eq_addOrderOf_valueCoset_of_single_radical_of_separableResidue
    [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)
    (hresidue : SeparableResidueRootLifts v w hExt)
    (alpha : L) (halpha0 : alpha ≠ 0)
    (hgen : IntermediateField.adjoin K ({alpha} : Set L) = ⊤)
    (m : ℕ) (hmpos : 0 < m)
    (hmcop : Nat.Coprime m (residueCharacteristic v))
    (a : K) (hpow : alpha ^ m = algebraMap K L a) :
    Module.finrank K L = addOrderOf (exponentialValueCoset v w alpha halpha0)

theorem

finrank_eq_addOrderOf_valueCoset_of_single_radical

L716 ↗

AlgebraicNumberTheory.Valuations.finrank_eq_addOrderOf_valueCoset_of_single_radical

Documentation

A one-generator prime-to-p radical extension with unchanged residue field has degree equal to the order of the generator's value coset.

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations
section SingleRadicalDegree
variable {K L : Type u} [Field K] [Field L] [Algebra K L]
@[reducible] local instance exponentialValueGroupQuotientAddCommGroupSingle
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L) :
    AddCommGroup (ExponentialValueGroupQuotient v w) :=
  QuotientAddGroup.Quotient.addCommGroup _

Lean source · statement

theorem finrank_eq_addOrderOf_valueCoset_of_single_radical
    [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)
    (hresidue : Function.Surjective (tameResidueFieldMap v w hExt))
    (alpha : L) (halpha0 : alpha ≠ 0)
    (hgen : IntermediateField.adjoin K ({alpha} : Set L) = ⊤)
    (m : ℕ) (hmpos : 0 < m)
    (hmcop : Nat.Coprime m (residueCharacteristic v))
    (a : K) (hpow : alpha ^ m = algebraMap K L a) :
    Module.finrank K L = addOrderOf (exponentialValueCoset v w alpha halpha0)

theorem

exponentialRamificationIndex_eq_finrank_of_single_radical_of_separableResidue

L742 ↗

AlgebraicNumberTheory.Valuations.exponentialRamificationIndex_eq_finrank_of_single_radical_of_separableResidue

Documentation

Under descent of separable residue elements, a one-generator prime-to-p radical extension is totally ramified: its actual value-group index equals its field degree.

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations
section SingleRadicalDegree
variable {K L : Type u} [Field K] [Field L] [Algebra K L]
@[reducible] local instance exponentialValueGroupQuotientAddCommGroupSingle
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L) :
    AddCommGroup (ExponentialValueGroupQuotient v w) :=
  QuotientAddGroup.Quotient.addCommGroup _

Lean source · statement

theorem exponentialRamificationIndex_eq_finrank_of_single_radical_of_separableResidue
    [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)
    (hresidue : SeparableResidueRootLifts v w hExt)
    (alpha : L) (halpha0 : alpha ≠ 0)
    (hgen : IntermediateField.adjoin K ({alpha} : Set L) = ⊤)
    (m : ℕ) (hmpos : 0 < m)
    (hmcop : Nat.Coprime m (residueCharacteristic v))
    (a : K) (hpow : alpha ^ m = algebraMap K L a) :
    exponentialRamificationIndex v w = Module.finrank K L

theorem

tameResidueFieldMap_surjective_of_single_radical_of_separableResidue

L782 ↗

AlgebraicNumberTheory.Valuations.tameResidueFieldMap_surjective_of_single_radical_of_separableResidue

Documentation

Under descent of separable residue elements, a single prime-to-p radical creates no residue-field extension.

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations
section SingleRadicalDegree
variable {K L : Type u} [Field K] [Field L] [Algebra K L]
@[reducible] local instance exponentialValueGroupQuotientAddCommGroupSingle
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L) :
    AddCommGroup (ExponentialValueGroupQuotient v w) :=
  QuotientAddGroup.Quotient.addCommGroup _

Lean source · statement

theorem tameResidueFieldMap_surjective_of_single_radical_of_separableResidue
    [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)
    (hresidue : SeparableResidueRootLifts v w hExt)
    (alpha : L) (halpha0 : alpha ≠ 0)
    (hgen : IntermediateField.adjoin K ({alpha} : Set L) = ⊤)
    (m : ℕ) (hmpos : 0 < m)
    (hmcop : Nat.Coprime m (residueCharacteristic v))
    (a : K) (hpow : alpha ^ m = algebraMap K L a) :
    Function.Surjective (tameResidueFieldMap v w hExt)

theorem

exponentialRamificationIndex_eq_finrank_of_single_radical

L871 ↗

AlgebraicNumberTheory.Valuations.exponentialRamificationIndex_eq_finrank_of_single_radical

Documentation

A one-generator prime-to-p radical extension with unchanged residue field is totally ramified.

Source context 7 commands

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

noncomputable section
universe u
namespace AlgebraicNumberTheory
namespace Valuations
section SingleRadicalDegree
variable {K L : Type u} [Field K] [Field L] [Algebra K L]
@[reducible] local instance exponentialValueGroupQuotientAddCommGroupSingle
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L) :
    AddCommGroup (ExponentialValueGroupQuotient v w) :=
  QuotientAddGroup.Quotient.addCommGroup _

Lean source · statement

theorem exponentialRamificationIndex_eq_finrank_of_single_radical
    [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)
    (hresidue : Function.Surjective (tameResidueFieldMap v w hExt))
    (alpha : L) (halpha0 : alpha ≠ 0)
    (hgen : IntermediateField.adjoin K ({alpha} : Set L) = ⊤)
    (m : ℕ) (hmpos : 0 < m)
    (hmcop : Nat.Coprime m (residueCharacteristic v))
    (a : K) (hpow : alpha ^ m = algebraMap K L a) :
    exponentialRamificationIndex v w = Module.finrank K L

Module documentation

A single radical in a tame extension

Declarations