NYLL
Module

PowerResidueTameFormula.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Kummer.PowerResidueTameFormula
23 declarations indexed from sourceView source ↗

Module documentation

Tame local power-residue formula

This file constructs reduction of local roots of unity, proves its injectivity, identifies the arithmetic-Frobenius root quotient with the finite-field power residue symbol, and derives the tame formula for the local Hilbert symbol.

Imports9
Imported by2

Declarations

theorem

nthRootsSubgroup_valuationMap_eq_zero

L40 ↗
LocalClassFieldTheory.Kummer.nthRootsSubgroup_valuationMap_eq_zero
Documentation

Every field-valued n-th root of unity has normalized valuation zero.

Source context 8 commands

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

open scoped ValuativeRel
noncomputable section
namespace LocalClassFieldTheory
namespace Kummer
open KummerTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem nthRootsSubgroup_valuationMap_eq_zero
    (n : ℕ+) (z : nthRootsSubgroup K (n : ℕ)) :
    valuationMap K (Additive.ofMul z.1) = 0
def

nthRootIntegerUnit

L52 ↗
LocalClassFieldTheory.Kummer.nthRootIntegerUnit
Documentation

The canonical valuation-ring unit underlying a local n-th root of unity.

Source context 8 commands

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

open scoped ValuativeRel
noncomputable section
namespace LocalClassFieldTheory
namespace Kummer
open KummerTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
def nthRootIntegerUnit
    (n : ℕ+) (z : nthRootsSubgroup K (n : ℕ)) : 𝒪[K]ˣ
theorem

integerUnitsToFieldUnits_nthRootIntegerUnit

L58 ↗
LocalClassFieldTheory.Kummer.integerUnitsToFieldUnits_nthRootIntegerUnit
Source context 8 commands

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

open scoped ValuativeRel
noncomputable section
namespace LocalClassFieldTheory
namespace Kummer
open KummerTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem integerUnitsToFieldUnits_nthRootIntegerUnit
    (n : ℕ+) (z : nthRootsSubgroup K (n : ℕ)) :
    integerUnitsToFieldUnits K (nthRootIntegerUnit K n z) = z.1
theorem

nthRootIntegerUnit_pow

L64 ↗
LocalClassFieldTheory.Kummer.nthRootIntegerUnit_pow
Source context 8 commands

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

open scoped ValuativeRel
noncomputable section
namespace LocalClassFieldTheory
namespace Kummer
open KummerTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem nthRootIntegerUnit_pow
    (n : ℕ+) (z : nthRootsSubgroup K (n : ℕ)) :
    nthRootIntegerUnit K n z ^ (n : ℕ) = 1
def

localNthRootsReduction

L72 ↗
LocalClassFieldTheory.Kummer.localNthRootsReduction
Documentation

Reduction of roots of unity from a nonarchimedean local field to its residue field.

Source context 8 commands

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

open scoped ValuativeRel
noncomputable section
namespace LocalClassFieldTheory
namespace Kummer
open KummerTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · full declaration
def localNthRootsReduction
    (n : ℕ+) :
    nthRootsSubgroup K (n : ℕ) →* rootsOfUnity (n : ℕ) 𝓀[K] where
  toFun z :=
    ⟨integerUnitsToResidueUnits K (nthRootIntegerUnit K n z), by
      change
        integerUnitsToResidueUnits K (nthRootIntegerUnit K n z) ^
            (n : ℕ) = 1
      rw [← map_pow, nthRootIntegerUnit_pow, map_one]⟩
  map_one' := by
    apply Subtype.ext
    apply Units.ext
    rfl
  map_mul' := by
    intro z w
    apply Subtype.ext
    apply Units.ext
    rfl
theorem

localNthRootsReduction_apply

L92 ↗
LocalClassFieldTheory.Kummer.localNthRootsReduction_apply
Source context 8 commands

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

open scoped ValuativeRel
noncomputable section
namespace LocalClassFieldTheory
namespace Kummer
open KummerTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem localNthRootsReduction_apply
    (n : ℕ+) (z : nthRootsSubgroup K (n : ℕ)) :
    (localNthRootsReduction K n z).1 =
      integerUnitsToResidueUnits K (nthRootIntegerUnit K n z)
theorem

localNthRootsReduction_nthRootsSubgroupMap

L99 ↗
LocalClassFieldTheory.Kummer.localNthRootsReduction_nthRootsSubgroupMap
Documentation

Reduction of roots of unity commutes with extension of valued fields.

Source context 8 commands

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

open scoped ValuativeRel
noncomputable section
namespace LocalClassFieldTheory
namespace Kummer
open KummerTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · full declaration
theorem localNthRootsReduction_nthRootsSubgroupMap
    (L : Type) [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L] [Algebra K L]
    [Valuation.HasExtension
      (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    (n : ℕ+) (z : nthRootsSubgroup K (n : ℕ)) :
    localNthRootsReduction L n
        (nthRootsSubgroupMap K L (n : ℕ) z) =
      ⟨residueUnitsMapOfValuationExtension K L
          (localNthRootsReduction K n z).1,
        by
          change
            residueUnitsMapOfValuationExtension K L
                (localNthRootsReduction K n z).1 ^ (n : ℕ) = 1
          rw [← map_pow, (localNthRootsReduction K n z).2, map_one]⟩ := by
  apply Subtype.ext
  change
    integerUnitsToResidueUnits L
        (nthRootIntegerUnit L n
          (nthRootsSubgroupMap K L (n : ℕ) z)) =
      residueUnitsMapOfValuationExtension K L
        (integerUnitsToResidueUnits K (nthRootIntegerUnit K n z))
  rw [residueUnitsMap_integerUnitsToResidueUnits]
  congr 1
  apply Units.ext
  apply Subtype.ext
  rfl
theorem

valuationMap_eq_zero_of_pow_eq_map_integerUnit

L130 ↗
LocalClassFieldTheory.Kummer.valuationMap_eq_zero_of_pow_eq_map_integerUnit
Documentation

An n-th root of the image of a valuation-ring unit again has normalized valuation zero.

Source context 9 commands

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

open scoped ValuativeRel
noncomputable section
namespace LocalClassFieldTheory
namespace Kummer
open KummerTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
omit [TopologicalSpace K] [IsNonarchimedeanLocalField K] in
Lean source · statement
theorem valuationMap_eq_zero_of_pow_eq_map_integerUnit
    (L : Type) [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L] [Algebra K L]
    [Valuation.HasExtension
      (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    (n : ℕ+) (u : 𝒪[K]ˣ) (beta : Lˣ)
    (hbetaPow :
      beta ^ (n : ℕ) =
        Units.map (algebraMap K L).toMonoidHom
          (integerUnitsToFieldUnits K u)) :
    valuationMap L (Additive.ofMul beta) = 0
theorem

integerUnitOfValuationMapZero_pow_eq_integerUnitsMap

L162 ↗
LocalClassFieldTheory.Kummer.integerUnitOfValuationMapZero_pow_eq_integerUnitsMap
Documentation

The canonical valuation-ring lift of such a root has the prescribed n-th power.

Source context 9 commands

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

open scoped ValuativeRel
noncomputable section
namespace LocalClassFieldTheory
namespace Kummer
open KummerTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
omit [TopologicalSpace K] [IsNonarchimedeanLocalField K] in
Lean source · statement
theorem integerUnitOfValuationMapZero_pow_eq_integerUnitsMap
    (L : Type) [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L] [Algebra K L]
    [Valuation.HasExtension
      (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    (n : ℕ+) (u : 𝒪[K]ˣ) (beta : Lˣ)
    (hbetaPow :
      beta ^ (n : ℕ) =
        Units.map (algebraMap K L).toMonoidHom
          (integerUnitsToFieldUnits K u)) :
    integerUnitOfValuationMapZero L beta
        (valuationMap_eq_zero_of_pow_eq_map_integerUnit
          K L n u beta hbetaPow) ^ (n : ℕ) =
      integerUnitsMapOfValuationExtension K L u
theorem

residue_arithmeticFrobenius_integerUnitQuotient

L193 ↗
LocalClassFieldTheory.Kummer.residue_arithmeticFrobenius_integerUnitQuotient
Documentation

Arithmetic Frobenius divided by the original integer unit reduces to its q - 1 power, where q is the base residue-field cardinality.

Source context 8 commands

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

open scoped ValuativeRel
noncomputable section
namespace LocalClassFieldTheory
namespace Kummer
open KummerTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem residue_arithmeticFrobenius_integerUnitQuotient
    (L : Type) [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [Valuation.HasExtension
      (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    [Module.Finite 𝒪[K] 𝒪[L]]
    [IsUnramifiedValuedExtension K L]
    (u : 𝒪[L]ˣ) :
    residueUnitsConcreteEquiv L
        (integerUnitsToResidueUnits L
          (Units.mapEquiv
              (galoisGroupIntegerRingEquivOfIsIntegralClosure K L
                (arithmeticFrobeniusOfUnramifiedValuation K L)).toMulEquiv
              u / u)) =
      (residueUnitsConcreteEquiv L (integerUnitsToResidueUnits L u)) ^
        (Nat.card 𝓀[K] - 1)
theorem

localNthRootsReduction_injective

L268 ↗
LocalClassFieldTheory.Kummer.localNthRootsReduction_injective
Documentation

If n is a valuation-ring unit, reduction is injective on the local n-th roots of unity.

Source context 8 commands

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

open scoped ValuativeRel
noncomputable section
namespace LocalClassFieldTheory
namespace Kummer
open KummerTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem localNthRootsReduction_injective
    (n : ℕ+)
    (hn : ValuativeRel.valuation K ((n : ℕ) : K) = 1) :
    Function.Injective (localNthRootsReduction K n)
def

localNthRootsReductionEquiv

L344 ↗
LocalClassFieldTheory.Kummer.localNthRootsReductionEquiv
Documentation

Away from the residue characteristic, reduction identifies the local and residue-field n-th roots of unity.

Source context 8 commands

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

open scoped ValuativeRel
noncomputable section
namespace LocalClassFieldTheory
namespace Kummer
open KummerTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
def localNthRootsReductionEquiv
    (n : ℕ+)
    (hn : ValuativeRel.valuation K ((n : ℕ) : K) = 1)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    nthRootsSubgroup K (n : ℕ) ≃* rootsOfUnity (n : ℕ) 𝓀[K]
theorem

dvd_residueCard_sub_one_of_primitiveRoots

L386 ↗
LocalClassFieldTheory.Kummer.dvd_residueCard_sub_one_of_primitiveRoots
Documentation

If K contains the n-th roots of unity and n is a local unit, then n divides the order of the residue-field unit group.

Source context 8 commands

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

open scoped ValuativeRel
noncomputable section
namespace LocalClassFieldTheory
namespace Kummer
open KummerTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem dvd_residueCard_sub_one_of_primitiveRoots
    (n : ℕ+)
    (hn : ValuativeRel.valuation K ((n : ℕ) : K) = 1)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) :
    (n : ℕ) ∣ Nat.card 𝓀[K] - 1
theorem

residue_arithmeticFrobenius_kummerRootQuotient

L413 ↗
LocalClassFieldTheory.Kummer.residue_arithmeticFrobenius_kummerRootQuotient
Documentation

For an n-th root of a base integer unit, the residue of its arithmetic Frobenius quotient is the base residue unit raised to (q - 1) / n.

Source context 8 commands

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

open scoped ValuativeRel
noncomputable section
namespace LocalClassFieldTheory
namespace Kummer
open KummerTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · full declaration
theorem residue_arithmeticFrobenius_kummerRootQuotient
    (L : Type) [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [Valuation.HasExtension
      (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    [Module.Finite 𝒪[K] 𝒪[L]]
    [IsUnramifiedValuedExtension K L]
    (n : ℕ+)
    (hn : ValuativeRel.valuation K ((n : ℕ) : K) = 1)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (u : 𝒪[K]ˣ) (beta : Lˣ)
    (hbetaPow :
      beta ^ (n : ℕ) =
        Units.map (algebraMap K L).toMonoidHom
          (integerUnitsToFieldUnits K u)) :
    let betaO :=
      integerUnitOfValuationMapZero L beta
        (valuationMap_eq_zero_of_pow_eq_map_integerUnit
          K L n u beta hbetaPow)
    residueUnitsConcreteEquiv L
        (integerUnitsToResidueUnits L
          (Units.mapEquiv
              (galoisGroupIntegerRingEquivOfIsIntegralClosure K L
                (arithmeticFrobeniusOfUnramifiedValuation K L)).toMulEquiv
              betaO / betaO)) =
      residueUnitsConcreteEquiv L
          (residueUnitsMapOfValuationExtension K L
            (integerUnitsToResidueUnits K u)) ^
        ((Nat.card 𝓀[K] - 1) / (n : ℕ)) := by
  let betaO : 𝒪[L]ˣ :=
    integerUnitOfValuationMapZero L beta
      (valuationMap_eq_zero_of_pow_eq_map_integerUnit
        K L n u beta hbetaPow)
  let betaBar : 𝓀[L]ˣ :=
    residueUnitsConcreteEquiv L (integerUnitsToResidueUnits L betaO)
  let uBar : 𝓀[L]ˣ :=
    residueUnitsConcreteEquiv L
      (residueUnitsMapOfValuationExtension K L
        (integerUnitsToResidueUnits K u))
  have hdvd : (n : ℕ) ∣ Nat.card 𝓀[K] - 1 :=
    dvd_residueCard_sub_one_of_primitiveRoots K n hn hmu
  let m := (Nat.card 𝓀[K] - 1) / (n : ℕ)
  have hcard : Nat.card 𝓀[K] - 1 = (n : ℕ) * m := by
    exact (Nat.div_mul_cancel hdvd).symm.trans (Nat.mul_comm _ _)
  have hbetaOPow :
      betaO ^ (n : ℕ) = integerUnitsMapOfValuationExtension K L u := by
    simpa only [betaO] using
      integerUnitOfValuationMapZero_pow_eq_integerUnitsMap
        K L n u beta hbetaPow
  have hbetaBarPow : betaBar ^ (n : ℕ) = uBar := by
    calc
      betaBar ^ (n : ℕ) =
          residueUnitsConcreteEquiv L
            (integerUnitsToResidueUnits L (betaO ^ (n : ℕ))) := by
        rw [map_pow, map_pow]
      _ = residueUnitsConcreteEquiv L
          (integerUnitsToResidueUnits L
            (integerUnitsMapOfValuationExtension K L u)) := by
        rw [hbetaOPow]
      _ = uBar := by
        rw [← residueUnitsMap_integerUnitsToResidueUnits K L u]
  change
    residueUnitsConcreteEquiv L
        (integerUnitsToResidueUnits L
          (Units.mapEquiv
              (galoisGroupIntegerRingEquivOfIsIntegralClosure K L
                (arithmeticFrobeniusOfUnramifiedValuation K L)).toMulEquiv
              betaO / betaO)) = uBar ^ m
  calc
    residueUnitsConcreteEquiv L
        (integerUnitsToResidueUnits L
          (Units.mapEquiv
              (galoisGroupIntegerRingEquivOfIsIntegralClosure K L
                (arithmeticFrobeniusOfUnramifiedValuation K L)).toMulEquiv
              betaO / betaO)) =
        betaBar ^ (Nat.card 𝓀[K] - 1) := by
      simpa only [betaBar] using
        residue_arithmeticFrobenius_integerUnitQuotient K L betaO
    _ = betaBar ^ ((n : ℕ) * m) := by rw [hcard]
    _ = (betaBar ^ (n : ℕ)) ^ m := by rw [pow_mul]
    _ = uBar ^ m := by rw [hbetaBarPow]
def

localTamePowerResidueSymbol

L499 ↗
LocalClassFieldTheory.Kummer.localTamePowerResidueSymbol
Documentation

The finite-field tame power-residue symbol, lifted canonically to the local n-th roots of unity.

Source context 8 commands

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

open scoped ValuativeRel
noncomputable section
namespace LocalClassFieldTheory
namespace Kummer
open KummerTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
def localTamePowerResidueSymbol
    (n : ℕ+)
    (hn : ValuativeRel.valuation K ((n : ℕ) : K) = 1)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (u : 𝒪[K]ˣ) :
    nthRootsSubgroup K (n : ℕ)
theorem

localNthRootsReductionEquiv_localTamePowerResidueSymbol

L517 ↗
LocalClassFieldTheory.Kummer.localNthRootsReductionEquiv_localTamePowerResidueSymbol
Documentation

Reduction of the lifted tame symbol is the literal finite-field power-residue symbol.

Source context 8 commands

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

open scoped ValuativeRel
noncomputable section
namespace LocalClassFieldTheory
namespace Kummer
open KummerTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · full declaration
theorem localNthRootsReductionEquiv_localTamePowerResidueSymbol
    (n : ℕ+)
    (hn : ValuativeRel.valuation K ((n : ℕ) : K) = 1)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (u : 𝒪[K]ˣ) :
    letI : Fintype 𝓀[K] := Fintype.ofFinite _
    localNthRootsReductionEquiv K n hn hmu
        (localTamePowerResidueSymbol K n hn hmu u) =
      AlgebraicNumberTheory.PowerResidueSymbols.finiteFieldPowerResidueSymbol
        𝓀[K] n
        (by
          rw [← Nat.card_eq_fintype_card]
          exact dvd_residueCard_sub_one_of_primitiveRoots K n hn hmu)
        (integerUnitsToResidueUnits K u) := by
  let : Fintype 𝓀[K] := Fintype.ofFinite _
  exact (localNthRootsReductionEquiv K n hn hmu).apply_symm_apply _
theorem

nthRootsSubgroupMap_localTamePowerResidueSymbol_eq_arithmeticFrobenius_rootQuotient

L536 ↗
LocalClassFieldTheory.Kummer.nthRootsSubgroupMap_localTamePowerResidueSymbol_eq_arithmeticFrobenius_rootQuotient
Documentation

The tame power-residue symbol embedded in an unramified extension is the root quotient of an n-th root by arithmetic Frobenius.

Source context 8 commands

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

open scoped ValuativeRel
noncomputable section
namespace LocalClassFieldTheory
namespace Kummer
open KummerTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem nthRootsSubgroupMap_localTamePowerResidueSymbol_eq_arithmeticFrobenius_rootQuotient
    (L : Type) [Field L] [ValuativeRel L] [TopologicalSpace L]
    [IsNonarchimedeanLocalField L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    [Valuation.HasExtension
      (ValuativeRel.valuation K) (ValuativeRel.valuation L)]
    [IsIntegralClosure 𝒪[L] 𝒪[K] L]
    [Module.Finite 𝒪[K] 𝒪[L]]
    [IsUnramifiedValuedExtension K L]
    (n : ℕ+)
    (hn : ValuativeRel.valuation K ((n : ℕ) : K) = 1)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (u : 𝒪[K]ˣ) (beta : Lˣ)
    (hbetaPow :
      beta ^ (n : ℕ) =
        Units.map (algebraMap K L).toMonoidHom
          (integerUnitsToFieldUnits K u)) :
    (nthRootsSubgroupMap K L (n : ℕ)
        (localTamePowerResidueSymbol K n hn hmu u)).1 =
      rootQuotient (K := K) (L := L) beta
        (arithmeticFrobeniusOfUnramifiedValuation K L)
theorem

natCast_ne_zero_of_valuation_eq_one

L698 ↗
LocalClassFieldTheory.Kummer.natCast_ne_zero_of_valuation_eq_one
Documentation

If n is a valuation-ring unit, then its image in the local field is nonzero. This supplies the characteristic hypothesis required by the chosen simple Kummer extension without adding a redundant assumption to the tame formula.

Source context 9 commands

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

open scoped ValuativeRel
noncomputable section
namespace LocalClassFieldTheory
namespace Kummer
open KummerTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
omit [TopologicalSpace K] [IsNonarchimedeanLocalField K] in
Lean source · statement
theorem natCast_ne_zero_of_valuation_eq_one
    (n : ℕ+)
    (hn : ValuativeRel.valuation K ((n : ℕ) : K) = 1) :
    ((n : ℕ) : K) ≠ 0
theorem

localHilbertSymbol_inverseIntegerRingUniformizerFieldUnit_integerUnit_eq_tame

L713 ↗
LocalClassFieldTheory.Kummer.localHilbertSymbol_inverseIntegerRingUniformizerFieldUnit_integerUnit_eq_tame
Documentation

For a valuation-ring unit u, the Hilbert symbol with the chosen inverse prime element in the first slot is the tame residue symbol of u. The proof constructs the unramified certificate for the chosen simple Kummer extension from its unit radical and then uses the arithmetic-Frobenius normalization of the local Artin map.

Source context 8 commands

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

open scoped ValuativeRel
noncomputable section
namespace LocalClassFieldTheory
namespace Kummer
open KummerTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem
    localHilbertSymbol_inverseIntegerRingUniformizerFieldUnit_integerUnit_eq_tame
    (n : ℕ+)
    (hn : ValuativeRel.valuation K ((n : ℕ) : K) = 1)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (u : 𝒪[K]ˣ) :
    localHilbertSymbol K n
        (natCast_ne_zero_of_valuation_eq_one K n hn) hmu
        (inverseIntegerRingUniformizerFieldUnit K)
        (integerUnitsToFieldUnits K u) =
      localTamePowerResidueSymbol K n hn hmu u
theorem

localHilbertSymbol_integerUnit_inverseIntegerRingUniformizerFieldUnit_eq_tame_inv

L806 ↗
LocalClassFieldTheory.Kummer.localHilbertSymbol_integerUnit_inverseIntegerRingUniformizerFieldUnit_eq_tame_inv
Documentation

Tame local Hilbert-symbol formula in the unit-first convention. It is the skew-symmetric form of the preceding arithmetic-Frobenius calculation.

Source context 8 commands

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

open scoped ValuativeRel
noncomputable section
namespace LocalClassFieldTheory
namespace Kummer
open KummerTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem
    localHilbertSymbol_integerUnit_inverseIntegerRingUniformizerFieldUnit_eq_tame_inv
    (n : ℕ+)
    (hn : ValuativeRel.valuation K ((n : ℕ) : K) = 1)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (u : 𝒪[K]ˣ) :
    localHilbertSymbol K n
        (natCast_ne_zero_of_valuation_eq_one K n hn) hmu
        (integerUnitsToFieldUnits K u)
        (inverseIntegerRingUniformizerFieldUnit K) =
      (localTamePowerResidueSymbol K n hn hmu u)⁻¹
theorem

localHilbertSymbol_zpow_right

L837 ↗
LocalClassFieldTheory.Kummer.localHilbertSymbol_zpow_right
Documentation

The local Hilbert symbol is compatible with arbitrary integral powers in its second argument.

Source context 8 commands

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

open scoped ValuativeRel
noncomputable section
namespace LocalClassFieldTheory
namespace Kummer
open KummerTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem localHilbertSymbol_zpow_right
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (a b : Kˣ) (m : ℤ) :
    localHilbertSymbol K n hnK hmu a (b ^ m) =
      localHilbertSymbol K n hnK hmu a b ^ m
theorem

localHilbertSymbol_integerUnit_integerUnit_eq_one

L858 ↗
LocalClassFieldTheory.Kummer.localHilbertSymbol_integerUnit_integerUnit_eq_one
Documentation

In the tame case, the local Hilbert symbol of two valuation-ring units is trivial. The chosen simple Kummer extension generated by the second unit is unramified, so the first unit has trivial local Artin symbol.

Source context 8 commands

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

open scoped ValuativeRel
noncomputable section
namespace LocalClassFieldTheory
namespace Kummer
open KummerTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem localHilbertSymbol_integerUnit_integerUnit_eq_one
    (n : ℕ+)
    (hn : ValuativeRel.valuation K ((n : ℕ) : K) = 1)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (u v : 𝒪[K]ˣ) :
    localHilbertSymbol K n
        (natCast_ne_zero_of_valuation_eq_one K n hn) hmu
        (integerUnitsToFieldUnits K u)
        (integerUnitsToFieldUnits K v) = 1
theorem

localHilbertSymbol_tame_formula

L948 ↗
LocalClassFieldTheory.Kummer.localHilbertSymbol_tame_formula
Documentation

General tame local Hilbert-symbol formula with a valuation-ring unit in the first slot. Decomposing the second argument into its unit factor and the chosen valuation-one prime power reduces the calculation to the unit-unit vanishing and the inverse-prime special case above.

Source context 8 commands

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

open scoped ValuativeRel
noncomputable section
namespace LocalClassFieldTheory
namespace Kummer
open KummerTheory
open LocalFieldTheory
open LocalFieldTheory.IsNonarchimedeanLocalField
variable (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem localHilbertSymbol_tame_formula
    (n : ℕ+)
    (hn : ValuativeRel.valuation K ((n : ℕ) : K) = 1)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (u : 𝒪[K]ˣ) (x : Kˣ) :
    localHilbertSymbol K n
        (natCast_ne_zero_of_valuation_eq_one K n hn) hmu
        (integerUnitsToFieldUnits K u) x =
      localTamePowerResidueSymbol K n hn hmu u ^
        (-valuationMap K (Additive.ofMul x))

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