NYLL
Module

LocalHilbertPairing.lean

Nyll.ClassFieldTheory.LocalClassFieldTheory.Kummer.LocalHilbertPairing
7 declarations indexed from sourceView source ↗

Module documentation

Comparison of maximal and simple local Kummer pairings

The chosen simple Kummer extension attached to one radical lies in the maximal finite Kummer extension. Restriction of the maximal local Artin automorphism to that simple extension, together with functoriality of root quotients, identifies the maximal pairing with the existing local Hilbert symbol.

Imports4
Imported by4

Declarations

theorem

rootQuotient_map_intermediateFieldInclusion

L36 ↗
KummerTheory.rootQuotient_map_intermediateFieldInclusion
Documentation

Root quotients commute with inclusion between normal intermediate fields in a common ambient extension.

Source context 5 commands

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

noncomputable section
namespace KummerTheory
open RamificationTheory
universe u v
variable {K : Type u} {Omega : Type v}
  [Field K] [Field Omega] [Algebra K Omega]
Lean source · statement
theorem rootQuotient_map_intermediateFieldInclusion
    (E F : IntermediateField K Omega) (hEF : E ≤ F)
    [Normal K E] (beta : Eˣ) (sigma : Gal(F/K)) :
    rootQuotient (K := K) (L := F)
        (Units.map (IntermediateField.inclusion hEF).toMonoidHom beta) sigma =
      Units.map (IntermediateField.inclusion hEF).toMonoidHom
        (rootQuotient (K := K) (L := E) beta
          (intermediateFieldRestrictNormalHom E F hEF sigma))
theorem

maximalLocalArtin_restrict_chosenSimpleKummer

L82 ↗
LocalClassFieldTheory.Kummer.maximalLocalArtin_restrict_chosenSimpleKummer
Documentation

Restricting the maximal Kummer Artin automorphism to the simple Kummer extension gives its defining simple-extension Artin automorphism.

Source context 6 commands

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

noncomputable section
namespace LocalClassFieldTheory
namespace Kummer
open KummerTheory LocalFieldTheory RamificationTheory
variable (K : Type) [Field K]
variable [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · full declaration
theorem maximalLocalArtin_restrict_chosenSimpleKummer
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (a b : Kˣ) :
    letI : IsAbelianGalois K (chosenSimpleKummerExtension K n hnK b) :=
      chosenSimpleKummerExtension_isAbelianGalois K n hnK hmu b
    intermediateFieldRestrictNormalHom
        (chosenSimpleKummerExtension K n hnK b)
        (maximalLocalKummerExtension K n)
        (chosenSimpleKummerExtension_le_maximalKummerExtension K n hnK b)
        (maximalLocalKummerNormResidueAutomorphism K n hnK hmu a) =
      chosenSimpleKummerNormResidueAutomorphism K n hnK hmu b a := by
  let E := chosenSimpleKummerExtension K n hnK b
  let F := maximalLocalKummerExtension K n
  let hEF : E ≤ F :=
    chosenSimpleKummerExtension_le_maximalKummerExtension K n hnK b
  let Delta := maximalKummerSubgroup K n
  let : FiniteDimensional K E :=
    chosenSimpleKummerExtension_finiteDimensional K n hnK b
  let : IsAbelianGalois K E :=
    chosenSimpleKummerExtension_isAbelianGalois K n hnK hmu b
  let : FiniteDimensional K F :=
    maximalKummerRadicalExtension_finiteDimensional K n hnK hmu
  let : IsAbelianGalois K F :=
    kummerRadicalExtension_isAbelianGalois
      (K := K) (Omega := SeparableClosure K) n hmu Delta.1
  change intermediateFieldRestrictNormalHom E F hEF
      (abelianLocalArtinMonoidHom K F a) =
    abelianLocalArtinMonoidHom K E a
  exact DFunLike.congr_fun
    (abelianLocalArtinMonoidHom_restrict K E F hEF) a
theorem

maximalLocalKummerPairingRightHom_eq_localHilbertSymbolHom

L115 ↗
LocalClassFieldTheory.Kummer.maximalLocalKummerPairingRightHom_eq_localHilbertSymbolHom
Documentation

The maximal pairing evaluated at (a,b) agrees with the local Hilbert symbol homomorphism for the simple extension generated by b.

Source context 6 commands

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

noncomputable section
namespace LocalClassFieldTheory
namespace Kummer
open KummerTheory LocalFieldTheory RamificationTheory
variable (K : Type) [Field K]
variable [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem maximalLocalKummerPairingRightHom_eq_localHilbertSymbolHom
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (a b : Kˣ) :
    maximalLocalKummerPairingRightHom K n hnK hmu a b =
      localHilbertSymbolHom K n hnK hmu b a
theorem

localHilbertSymbol_mul_right

L199 ↗
LocalClassFieldTheory.Kummer.localHilbertSymbol_mul_right
Documentation

The local Hilbert symbol is multiplicative in its second argument.

Source context 6 commands

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

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

localHilbertSymbol_steinberg

L221 ↗
LocalClassFieldTheory.Kummer.localHilbertSymbol_steinberg
Documentation

The local Hilbert symbol of a unit and its nonzero complement is one.

Source context 6 commands

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

noncomputable section
namespace LocalClassFieldTheory
namespace Kummer
open KummerTheory LocalFieldTheory RamificationTheory
variable (K : Type) [Field K]
variable [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem localHilbertSymbol_steinberg
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (a : Kˣ) (h_one_sub : 1 - (a : K) ≠ 0) :
    localHilbertSymbol K n hnK hmu a
        (Units.mk0 (1 - (a : K)) h_one_sub) = 1
theorem

localHilbertSymbol_neg_self

L236 ↗
LocalClassFieldTheory.Kummer.localHilbertSymbol_neg_self
Documentation

The local Hilbert symbol of a unit and its negative is one.

Source context 6 commands

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

noncomputable section
namespace LocalClassFieldTheory
namespace Kummer
open KummerTheory LocalFieldTheory RamificationTheory
variable (K : Type) [Field K]
variable [ValuativeRel K] [TopologicalSpace K]
  [IsNonarchimedeanLocalField K]
Lean source · statement
theorem localHilbertSymbol_neg_self
    (n : ℕ+) (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty) (a : Kˣ) :
    localHilbertSymbol K n hnK hmu a (-a) = 1
theorem

localHilbertSymbol_skew

L309 ↗
LocalClassFieldTheory.Kummer.localHilbertSymbol_skew
Documentation

The local Hilbert symbol is skew-symmetric.

Source context 6 commands

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

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

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