NYLL
Module

RadicalGeneration.lean

Nyll.SchemeTheory.AbhyankarLemma.Kummer.RadicalGeneration
8 declarations indexed from sourceView source ↗

Module documentation

Radical sources for tame extensions

For a finite tamely ramified extension, the radical-generation theorem describes the extension over its maximal unramified subfield by finitely many radicals of orders prime to the residue characteristic. The definitions below state that conclusion literally. The first construction step is also proved: the order of every actual value-group coset kills the value of a chosen representative modulo the base value group, producing a base element whose value is the value of the corresponding power.

This is source data from the actual quotient w(Lˣ)/v(Kˣ), not a certificate for the final generation statement.

Imports2
Imported by2

Declarations

instance

exponentialValueGroupQuotientAddCommGroup

L37 ↗
AlgebraicNumberTheory.Valuations.exponentialValueGroupQuotientAddCommGroup
Documentation

The additive group structure is definitionally the quotient-group structure. Naming it here lets the order API unfold the transparent abbreviation reliably.

Source context 5 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
section ValueCosetAndPrincipalUnitRadicals
variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
Lean source · statement
instance exponentialValueGroupQuotientAddCommGroup
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L) :
    AddCommGroup (ExponentialValueGroupQuotient v w)
def

GeneratedByRadicalsPrimeTo

L49 ↗
AlgebraicNumberTheory.Valuations.GeneratedByRadicalsPrimeTo
Documentation

The literal radical-generation conclusion for a tame extension.

There is a concrete finite family of positive exponents, base elements and chosen roots in L; every exponent is prime to p, every displayed root satisfies its power equation, and those roots generate all of L over T.

Source context 6 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
section ValueCosetAndPrincipalUnitRadicals
variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
/-- The additive group structure is definitionally the quotient-group
structure.  Naming it here lets the order API unfold the transparent
abbreviation reliably. -/
@[reducible] local instance exponentialValueGroupQuotientAddCommGroup
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L) :
    AddCommGroup (ExponentialValueGroupQuotient v w) :=
  QuotientAddGroup.Quotient.addCommGroup _
Lean source · statement
def GeneratedByRadicalsPrimeTo
    (T : IntermediateField K L) (p : ℕ) : Prop
def

GeneratedOverMaximalUnramifiedByRadicals

L60 ↗
AlgebraicNumberTheory.Valuations.GeneratedOverMaximalUnramifiedByRadicals
Documentation

The precise radical predicate for tame generation, with T the maximal unramified subextension and p the actual residue characteristic.

Source context 6 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
section ValueCosetAndPrincipalUnitRadicals
variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
/-- The additive group structure is definitionally the quotient-group
structure.  Naming it here lets the order API unfold the transparent
abbreviation reliably. -/
@[reducible] local instance exponentialValueGroupQuotientAddCommGroup
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L) :
    AddCommGroup (ExponentialValueGroupQuotient v w) :=
  QuotientAddGroup.Quotient.addCommGroup _
Lean source · statement
def GeneratedOverMaximalUnramifiedByRadicals
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a) : Prop
theorem

exponentialValueGroupQuotient_addOrderOf_pos

L70 ↗
AlgebraicNumberTheory.Valuations.exponentialValueGroupQuotient_addOrderOf_pos
Documentation

In a finite valued extension, every element of the actual value-group quotient has positive finite additive order.

Source context 6 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
section ValueCosetAndPrincipalUnitRadicals
variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
/-- The additive group structure is definitionally the quotient-group
structure.  Naming it here lets the order API unfold the transparent
abbreviation reliably. -/
@[reducible] local instance exponentialValueGroupQuotientAddCommGroup
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L) :
    AddCommGroup (ExponentialValueGroupQuotient v w) :=
  QuotientAddGroup.Quotient.addCommGroup _
Lean source · statement
theorem exponentialValueGroupQuotient_addOrderOf_pos
    [FiniteDimensional K L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (q : ExponentialValueGroupQuotient v w) :
    0 < addOrderOf q
theorem

exponentialValueGroupQuotient_addOrderOf_dvd_ramificationIndex

L83 ↗
AlgebraicNumberTheory.Valuations.exponentialValueGroupQuotient_addOrderOf_dvd_ramificationIndex
Documentation

The order of an actual value-group coset divides the ramification index, because the latter is the cardinality of that quotient.

Source context 6 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
section ValueCosetAndPrincipalUnitRadicals
variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
/-- The additive group structure is definitionally the quotient-group
structure.  Naming it here lets the order API unfold the transparent
abbreviation reliably. -/
@[reducible] local instance exponentialValueGroupQuotientAddCommGroup
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L) :
    AddCommGroup (ExponentialValueGroupQuotient v w) :=
  QuotientAddGroup.Quotient.addCommGroup _
Lean source · statement
theorem exponentialValueGroupQuotient_addOrderOf_dvd_ramificationIndex
    [FiniteDimensional K L]
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (q : ExponentialValueGroupQuotient v w) :
    addOrderOf q ∣ exponentialRamificationIndex v w
theorem

exists_base_element_value_eq_pow_addOrderOf_valueCoset

L101 ↗
AlgebraicNumberTheory.Valuations.exists_base_element_value_eq_pow_addOrderOf_valueCoset
Documentation

Raising a nonzero element to the order of its value-group coset puts its value in the base value subgroup. This is the first concrete step in the radical construction.

Source context 7 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
section ValueCosetAndPrincipalUnitRadicals
variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
/-- The additive group structure is definitionally the quotient-group
structure.  Naming it here lets the order API unfold the transparent
abbreviation reliably. -/
@[reducible] local instance exponentialValueGroupQuotientAddCommGroup
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L) :
    AddCommGroup (ExponentialValueGroupQuotient v w) :=
  QuotientAddGroup.Quotient.addCommGroup _
omit [Algebra K L] in
Lean source · statement
theorem exists_base_element_value_eq_pow_addOrderOf_valueCoset
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (x : L) (hx : x ≠ 0) :
    ∃ a : K, a ≠ 0 ∧
      v a = w (x ^ addOrderOf (exponentialValueCoset v w x hx))
theorem

exists_base_element_and_value_zero_radical_correction

L161 ↗
AlgebraicNumberTheory.Valuations.exists_base_element_and_value_zero_radical_correction
Documentation

The base element supplied by the coset order turns the corresponding power into an actual value-zero unit after division.

Source context 6 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
section ValueCosetAndPrincipalUnitRadicals
variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
/-- The additive group structure is definitionally the quotient-group
structure.  Naming it here lets the order API unfold the transparent
abbreviation reliably. -/
@[reducible] local instance exponentialValueGroupQuotientAddCommGroup
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L) :
    AddCommGroup (ExponentialValueGroupQuotient v w) :=
  QuotientAddGroup.Quotient.addCommGroup _
Lean source · statement
theorem exists_base_element_and_value_zero_radical_correction
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L)
    (hExt : ∀ a : K, w (algebraMap K L a) = v a)
    (x : L) (hx : x ≠ 0) :
    ∃ a : K, a ≠ 0 ∧
      v a = w (x ^ addOrderOf (exponentialValueCoset v w x hx)) ∧
        w (x ^ addOrderOf (exponentialValueCoset v w x hx) /
          algebraMap K L a) = 0
theorem

exists_pow_eq_of_residue_eq_one_of_coprime

L198 ↗
AlgebraicNumberTheory.Valuations.exists_pow_eq_of_residue_eq_one_of_coprime
Documentation

Hensel's lemma supplies prime-to-residue-characteristic roots on the principal-unit fibre: if a valuation-ring element reduces to 1, then it is an m-th power whenever m is prime to the positive residue characteristic.

This is the root-producing step used in the forward tame-generation implication. The proof applies the separability criterion to the concrete factorization X^m - 1 = (X - 1) * (1 + X + ... + X^(m-1)); coprimality follows because the second factor takes the nonzero value m at 1.

Source context 6 commands

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

noncomputable section
namespace AlgebraicNumberTheory
namespace Valuations
section ValueCosetAndPrincipalUnitRadicals
variable {K : Type*} {L : Type*} [Field K] [Field L] [Algebra K L]
/-- The additive group structure is definitionally the quotient-group
structure.  Naming it here lets the order API unfold the transparent
abbreviation reliably. -/
@[reducible] local instance exponentialValueGroupQuotientAddCommGroup
    (v : LubinTate.Valuations.ExponentialValuation K)
    (w : LubinTate.Valuations.ExponentialValuation L) :
    AddCommGroup (ExponentialValueGroupQuotient v w) :=
  QuotientAddGroup.Quotient.addCommGroup _
Lean source · statement
theorem exists_pow_eq_of_residue_eq_one_of_coprime
    (v : LubinTate.Valuations.ExponentialValuation K)
    (hhens : ValuationTheory.DiscreteValuationField.HenselianValuationByFactorization
      (LubinTate.Valuations.exponentialValuationSubringAsValuationSubring v).valuation)
    (hp : PositiveResidueCharacteristic v)
    (m : ℕ)
    (hcop : Nat.Coprime m (residueCharacteristic v))
    (u : LubinTate.Valuations.exponentialValuationSubring v)
    (hu : IsLocalRing.residue (LubinTate.Valuations.exponentialValuationSubring v) u = 1) :
    ∃ β : LubinTate.Valuations.exponentialValuationSubring v,
      β ^ m = u ∧
        IsLocalRing.residue (LubinTate.Valuations.exponentialValuationSubring v) β = 1

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