NYLL
Module

RestrictionKernel.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.ClassFieldAxiom.SUnitKummerPrimeSelection.RestrictionKernel
6 declarations indexed from sourceView source ↗

Module documentation

Restriction kernels of S-unit Kummer extensions

This file specializes the chosen restriction-kernel coordinates of an enlarged S-unit Kummer extension to coordinate generators, their required number, and their cyclic fixed fields.

Imports1
Imported by3

Declarations

def

sUnitKummerPrimeCount

L34 ↗
GlobalClassFieldTheory.ClassFieldAxiom.sUnitKummerPrimeCount
Documentation

The number s-r of finite places required to detect the restriction kernel for the chosen source-produced enlargement of S.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
section GeneralKummer
variable {K : Type*} [Field K]
    [NumberField K]
Lean source · statement
def sUnitKummerPrimeCount
    {Omega : Type*} [Field Omega] [Algebra K Omega]
    (E : IntermediateField K Omega)
    [FiniteDimensional K E] [IsGalois K E]
    (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (r : ℕ)
    (S : Finset (HeightOneSpectrum (𝓞 K))) : ℕ
def

sUnitKummerKernelGenerator

L48 ↗
GlobalClassFieldTheory.ClassFieldAxiom.sUnitKummerKernelGenerator
Documentation

The i-th standard generator of the actual restriction kernel Gal(N/E).

Source context 7 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
section GeneralKummer
variable {K : Type*} [Field K]
    [NumberField K]
Lean source · statement
def sUnitKummerKernelGenerator
    {Omega : Type*} [Field Omega] [Algebra K Omega]
    [IsSepClosure K Omega]
    (E : IntermediateField K Omega)
    [FiniteDimensional K E] [IsGalois K E]
    [IsMulCommutative Gal(E/K)]
    (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (p v : ℕ) (hp : p.Prime) (hv : 0 < v)
    (hn : (n : ℕ) = p ^ v)
    (r : ℕ)
    (eG :
      Gal(E/K) ≃*
        (Fin r → Multiplicative (ZMod (n : ℕ))))
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (i : Fin
      (sUnitKummerPrimeCount
        (K := K) E n hmu r S))
theorem

iSup_zpowers_sUnitKummerKernelGenerator_eq_top

L74 ↗
GlobalClassFieldTheory.ClassFieldAxiom.iSup_zpowers_sUnitKummerKernelGenerator_eq_top
Documentation

The standard coordinate generators span the actual restriction kernel Gal(N / E).

Source context 7 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
section GeneralKummer
variable {K : Type*} [Field K]
    [NumberField K]
Lean source · statement
theorem iSup_zpowers_sUnitKummerKernelGenerator_eq_top
    {Omega : Type*} [Field Omega] [Algebra K Omega]
    [IsSepClosure K Omega]
    (E : IntermediateField K Omega)
    [FiniteDimensional K E] [IsGalois K E]
    [IsMulCommutative Gal(E/K)]
    (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (p v : ℕ) (hp : p.Prime) (hv : 0 < v)
    (hn : (n : ℕ) = p ^ v)
    (r : ℕ)
    (eG :
      Gal(E/K) ≃*
        (Fin r → Multiplicative (ZMod (n : ℕ))))
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    (⨆ i :
        Fin
          (sUnitKummerPrimeCount
            (K := K) E n hmu r S),
      Subgroup.zpowers
        (sUnitKummerKernelGenerator
          (K := K) (Omega := Omega) E n hmu
          p v hp hv hn r eG S i)) =
      ⊤
theorem

orderOf_sUnitKummerKernelGenerator

L170 ↗
GlobalClassFieldTheory.ClassFieldAxiom.orderOf_sUnitKummerKernelGenerator
Documentation

Every standard restriction-kernel generator has exact order n.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
section GeneralKummer
variable {K : Type*} [Field K]
    [NumberField K]
Lean source · statement
theorem orderOf_sUnitKummerKernelGenerator
    {Omega : Type*} [Field Omega] [Algebra K Omega]
    [IsSepClosure K Omega]
    (E : IntermediateField K Omega)
    [FiniteDimensional K E] [IsGalois K E]
    [IsMulCommutative Gal(E/K)]
    (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (p v : ℕ) (hp : p.Prime) (hv : 0 < v)
    (hn : (n : ℕ) = p ^ v)
    (r : ℕ)
    (eG :
      Gal(E/K) ≃*
        (Fin r → Multiplicative (ZMod (n : ℕ))))
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (i : Fin
      (sUnitKummerPrimeCount
        (K := K) E n hmu r S)) :
    orderOf
        (sUnitKummerKernelGenerator
          (K := K) (Omega := Omega) E n hmu
          p v hp hv hn r eG S i) =
      (n : ℕ)
def

sUnitKummerCoordinateFixedField

L215 ↗
GlobalClassFieldTheory.ClassFieldAxiom.sUnitKummerCoordinateFixedField
Documentation

The cyclic fixed field attached to the i-th coordinate of the actual relative Galois group Gal(N/E).

Source context 7 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
section GeneralKummer
variable {K : Type*} [Field K]
    [NumberField K]
Lean source · statement
def sUnitKummerCoordinateFixedField
    {Omega : Type*} [Field Omega] [Algebra K Omega]
    [IsSepClosure K Omega]
    (E : IntermediateField K Omega)
    [FiniteDimensional K E] [IsGalois K E]
    [IsMulCommutative Gal(E/K)]
    (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (p v : ℕ) (hp : p.Prime) (hv : 0 < v)
    (hn : (n : ℕ) = p ^ v)
    (r : ℕ)
    (eG :
      Gal(E/K) ≃*
        (Fin r → Multiplicative (ZMod (n : ℕ))))
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (i : Fin
      (sUnitKummerPrimeCount
        (K := K) E n hmu r S))
theorem

sUnitKummerCoordinateFixedField_finrank

L243 ↗
GlobalClassFieldTheory.ClassFieldAxiom.sUnitKummerCoordinateFixedField_finrank
Documentation

Each coordinate fixed field has relative degree exactly n in the full S-unit Kummer field.

Source context 7 commands

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

open scoped NumberField IsMulCommutative
open NumberField IsDedekindDomain
open KummerTheory
noncomputable section
namespace GlobalClassFieldTheory.ClassFieldAxiom
section GeneralKummer
variable {K : Type*} [Field K]
    [NumberField K]
Lean source · statement
theorem sUnitKummerCoordinateFixedField_finrank
    {Omega : Type*} [Field Omega] [Algebra K Omega]
    [IsSepClosure K Omega]
    (E : IntermediateField K Omega)
    [FiniteDimensional K E] [IsGalois K E]
    [IsMulCommutative Gal(E/K)]
    (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (p v : ℕ) (hp : p.Prime) (hv : 0 < v)
    (hn : (n : ℕ) = p ^ v)
    (r : ℕ)
    (eG :
      Gal(E/K) ≃*
        (Fin r → Multiplicative (ZMod (n : ℕ))))
    (S : Finset (HeightOneSpectrum (𝓞 K)))
    (i : Fin
      (sUnitKummerPrimeCount
        (K := K) E n hmu r S)) :
    Module.finrank
        (sUnitKummerCoordinateFixedField
          (K := K) (Omega := Omega) E n hmu
          p v hp hv hn r eG S i)
        (fullSUnitKummerExtension
          (K := K) (Omega := Omega) n
          (enlargeByFiniteKummerRadicalSupport
            (K := K) (L := E) n hmu S)) =
      (n : ℕ)

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