Module

KummerLocalNormContainment.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.ClassFieldAxiom.KummerLocalNormContainment

4 declarations indexed from sourceView source ↗

Module documentation

Local norm containment for Kummer extensions

This module proves that local powers, and then the concrete simple-Kummer power subgroup, lie in the norm subgroup at a chosen finite place.

Imports6

Imported by2

theorem

galois_pow_eq_one_of_field_equiv_pi_zmod

L39 ↗

GlobalClassFieldTheory.ClassFieldAxiom.galois_pow_eq_one_of_field_equiv_pi_zmod

Documentation

Coordinates in (Z/nZ)^r show that every Galois automorphism has exponent dividing n.

Source context 10 commands

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

open scoped NumberField NNReal IsMulCommutative
open NumberField IsDedekindDomain
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open KummerTheory
open LocalFieldTheory
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type*} [Field K] [NumberField K]
omit [NumberField K] in

Lean source · statement

theorem galois_pow_eq_one_of_field_equiv_pi_zmod
    {L : Type*} [Field L] [Algebra K L]
    (n : ℕ+) (r : ℕ)
    (eG :
      (L ≃ₐ[K] L) ≃*
        (Fin r → Multiplicative (ZMod (n : ℕ)))) :
    ∀ sigma : L ≃ₐ[K] L, sigma ^ (n : ℕ) = 1

theorem

nthPowerSubgroup_le_chosenFinitePlaceLocalNormSubgroup_of_galois_pow_eq_one

L58 ↗

GlobalClassFieldTheory.ClassFieldAxiom.nthPowerSubgroup_le_chosenFinitePlaceLocalNormSubgroup_of_galois_pow_eq_one

Documentation

Local n-th powers are norms from the chosen finite-place completion when every global Galois automorphism has exponent dividing n. This is the shared local-field core used by the coordinate and simple-Kummer wrappers below.

Source context 9 commands

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

open scoped NumberField NNReal IsMulCommutative
open NumberField IsDedekindDomain
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open KummerTheory
open LocalFieldTheory
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type*} [Field K] [NumberField K]

Lean source · statement

theorem
    nthPowerSubgroup_le_chosenFinitePlaceLocalNormSubgroup_of_galois_pow_eq_one
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (n : ℕ+)
    (hGlobal :
      ∀ sigma : L ≃ₐ[K] L,
        sigma ^ (n : ℕ) = 1)
    (v : HeightOneSpectrum (𝓞 K)) :
    (powMonoidHom (n : ℕ) :
        (v.adicCompletion K)ˣ →*
          (v.adicCompletion K)ˣ).range ≤
      _root_.chosenFinitePlaceLocalNormSubgroup
        (K := K) (L := L) v

theorem

nthPowerSubgroup_le_chosenFinitePlaceLocalNormSubgroup

L175 ↗

GlobalClassFieldTheory.ClassFieldAxiom.nthPowerSubgroup_le_chosenFinitePlaceLocalNormSubgroup

Documentation

Local n-th powers are norms from the chosen finite-place completion when the global Galois group has exponent dividing n.

Source context 9 commands

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

open scoped NumberField NNReal IsMulCommutative
open NumberField IsDedekindDomain
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open KummerTheory
open LocalFieldTheory
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type*} [Field K] [NumberField K]

Lean source · statement

theorem nthPowerSubgroup_le_chosenFinitePlaceLocalNormSubgroup
    {K L : Type}
    [Field K] [NumberField K]
    [Field L] [Algebra K L]
    [FiniteDimensional K L] [IsGalois K L]
    (n : ℕ+) (r : ℕ)
    (eG :
      (L ≃ₐ[K] L) ≃*
        (Fin r → Multiplicative (ZMod (n : ℕ))))
    (v : HeightOneSpectrum (𝓞 K)) :
    (powMonoidHom (n : ℕ) :
        (v.adicCompletion K)ˣ →*
          (v.adicCompletion K)ˣ).range ≤
      _root_.chosenFinitePlaceLocalNormSubgroup
        (K := K) (L := L) v

theorem

chosenSimpleKummerNthPowerSubgroup_le_chosenFinitePlaceLocalNormSubgroup

L199 ↗

GlobalClassFieldTheory.ClassFieldAxiom.chosenSimpleKummerNthPowerSubgroup_le_chosenFinitePlaceLocalNormSubgroup

Documentation

For the actual simple Kummer extension K(ⁿ√b)/K, every local n-th power is a norm at every finite place. The exponent input is produced by the concrete Kummer character, rather than supplied as a hypothesis.

Source context 9 commands

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

open scoped NumberField NNReal IsMulCommutative
open NumberField IsDedekindDomain
open AlgebraicNumberTheory.Valuations
open HilbertRamification
open KummerTheory
open LocalFieldTheory
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
variable {K : Type*} [Field K] [NumberField K]

Lean source · full declaration

theorem chosenSimpleKummerNthPowerSubgroup_le_chosenFinitePlaceLocalNormSubgroup
    {K : Type} [Field K] [NumberField K]
    (n : ℕ+)
    (hnK : ((n : ℕ) : K) ≠ 0)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (b : Kˣ)
    (v : HeightOneSpectrum (𝓞 K)) :
    let E :=
      KummerTheory.chosenSimpleKummerExtension K n hnK b
    letI : FiniteDimensional K E :=
      KummerTheory.chosenSimpleKummerExtension_finiteDimensional
        K n hnK b
    letI : IsAbelianGalois K E :=
      KummerTheory.chosenSimpleKummerExtension_isAbelianGalois
        K n hnK hmu b
    (powMonoidHom (n : ℕ) :
        (v.adicCompletion K)ˣ →*
          (v.adicCompletion K)ˣ).range ≤
      _root_.chosenFinitePlaceLocalNormSubgroup
        (K := K) (L := E) v := by
  let E :=
    KummerTheory.chosenSimpleKummerExtension K n hnK b
  let : FiniteDimensional K E :=
    KummerTheory.chosenSimpleKummerExtension_finiteDimensional
      K n hnK b
  let : IsAbelianGalois K E :=
    KummerTheory.chosenSimpleKummerExtension_isAbelianGalois
      K n hnK hmu b
  exact
    nthPowerSubgroup_le_chosenFinitePlaceLocalNormSubgroup_of_galois_pow_eq_one
      (K := K) (L := E) n
      (KummerTheory.chosenSimpleKummerExtension_galois_pow_eq_one
        K n hnK hmu b) v

Module documentation

Local norm containment for Kummer extensions

Declarations

galois_pow_eq_one_of_field_equiv_pi_zmod

nthPowerSubgroup_le_chosenFinitePlaceLocalNormSubgroup_of_galois_pow_eq_one

nthPowerSubgroup_le_chosenFinitePlaceLocalNormSubgroup

chosenSimpleKummerNthPowerSubgroup_le_chosenFinitePlaceLocalNormSubgroup