NYLL
Module

BasePlaceSelection.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.ClassFieldAxiom.SUnitKummerPrimeSelection.BasePlaceSelection
10 declarations indexed from sourceView source ↗

Module documentation

Base-place selection for S-unit Kummer extensions

This file constructs infinite full-decomposition candidate sets and chooses pairwise distinct base places outside the finite avoidance set. Distinctness is obtained from Mathlib's Hall marriage theorem.

Imports3
Imported by4

Declarations

def

sUnitKummerCoordinateBasePlaceCandidates

L36 ↗
GlobalClassFieldTheory.ClassFieldAxiom.sUnitKummerCoordinateBasePlaceCandidates
Documentation

Base finite places lying below a full-decomposition place for the cyclic coordinate extension N/N_i.

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 FinitePlaces
variable {K : Type} [Field K]
    [NumberField K]
Lean source · statement
def sUnitKummerCoordinateBasePlaceCandidates
    {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)) :
    Set (HeightOneSpectrum (𝓞 K))
theorem

sUnitKummerCoordinateBasePlaceCandidates_infinite

L92 ↗
GlobalClassFieldTheory.ClassFieldAxiom.sUnitKummerCoordinateBasePlaceCandidates_infinite
Documentation

Each cyclic coordinate extension supplies infinitely many base finite places below completely decomposed places.

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 FinitePlaces
variable {K : Type} [Field K]
    [NumberField K]
Lean source · statement
theorem sUnitKummerCoordinateBasePlaceCandidates_infinite
    {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)) :
    (sUnitKummerCoordinateBasePlaceCandidates
      (K := K) (Omega := Omega) E n hmu
      p v hp hv hn r eG S i).Infinite
def

sUnitKummerAvoidedBasePlaces

L183 ↗
GlobalClassFieldTheory.ClassFieldAxiom.sUnitKummerAvoidedBasePlaces
Documentation

The finite set avoided in the prime choice: the enlarged support, all base primes ramified in the full Kummer extension, and the support of the exponent 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 FinitePlaces
variable {K : Type} [Field K]
    [NumberField K]
Lean source · statement
def sUnitKummerAvoidedBasePlaces
    {Omega : Type} [Field Omega] [Algebra K Omega]
    [IsSepClosure K Omega]
    (E : IntermediateField K Omega)
    [FiniteDimensional K E] [IsGalois K E]
    (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    Finset (HeightOneSpectrum (𝓞 K))
theorem

enlargeByFiniteKummerRadicalSupport_subset_sUnitKummerAvoidedBasePlaces

L217 ↗
GlobalClassFieldTheory.ClassFieldAxiom.enlargeByFiniteKummerRadicalSupport_subset_sUnitKummerAvoidedBasePlaces
Documentation

The enlarged support is contained in the finite avoidance set.

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 FinitePlaces
variable {K : Type} [Field K]
    [NumberField K]
Lean source · statement
theorem
    enlargeByFiniteKummerRadicalSupport_subset_sUnitKummerAvoidedBasePlaces
    {Omega : Type} [Field Omega] [Algebra K Omega]
    [IsSepClosure K Omega]
    (E : IntermediateField K Omega)
    [FiniteDimensional K E] [IsGalois K E]
    (n : ℕ+)
    (hmu : (primitiveRoots (n : ℕ) K).Nonempty)
    (S : Finset (HeightOneSpectrum (𝓞 K))) :
    enlargeByFiniteKummerRadicalSupport
        (K := K) (L := E) n hmu S ⊆
      sUnitKummerAvoidedBasePlaces
        (K := K) (Omega := Omega) E n hmu S
theorem

exists_sUnitKummerChosenBasePlaces

L240 ↗
GlobalClassFieldTheory.ClassFieldAxiom.exists_sUnitKummerChosenBasePlaces
Documentation

Simultaneously choose distinct full-decomposition candidates outside the enlarged support, the ramified primes of N/K, and the support of 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 FinitePlaces
variable {K : Type} [Field K]
    [NumberField K]
Lean source · statement
theorem exists_sUnitKummerChosenBasePlaces
    {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))) :
    ∃ f :
        Fin
            (sUnitKummerPrimeCount
              (K := K) E n hmu r S) →
          HeightOneSpectrum (𝓞 K),
      Function.Injective f ∧
        ∀ i,
          f i ∈
              sUnitKummerCoordinateBasePlaceCandidates
                (K := K) (Omega := Omega) E n hmu
                p v hp hv hn r eG S i ∧
            f i ∉
              sUnitKummerAvoidedBasePlaces
                (K := K) (Omega := Omega) E n hmu S
def

sUnitKummerChosenBasePlaces

L313 ↗
GlobalClassFieldTheory.ClassFieldAxiom.sUnitKummerChosenBasePlaces
Documentation

The chosen ordered family of base primes.

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 FinitePlaces
variable {K : Type} [Field K]
    [NumberField K]
Lean source · statement
def sUnitKummerChosenBasePlaces
    {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))) :
    Fin
        (sUnitKummerPrimeCount
          (K := K) E n hmu r S) →
      HeightOneSpectrum (𝓞 K)
theorem

sUnitKummerChosenBasePlaces_injective

L338 ↗
GlobalClassFieldTheory.ClassFieldAxiom.sUnitKummerChosenBasePlaces_injective
Documentation

The chosen base primes are pairwise distinct.

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 FinitePlaces
variable {K : Type} [Field K]
    [NumberField K]
Lean source · statement
theorem sUnitKummerChosenBasePlaces_injective
    {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))) :
    Function.Injective
      (sUnitKummerChosenBasePlaces
        (K := K) (Omega := Omega) E n hmu
        p v hp hv hn r eG S)
theorem

sUnitKummerChosenBasePlaces_mem_coordinateBasePlaceCandidates

L364 ↗
GlobalClassFieldTheory.ClassFieldAxiom.sUnitKummerChosenBasePlaces_mem_coordinateBasePlaceCandidates
Documentation

Each chosen base prime lies below a completely decomposed place in its coordinate fixed 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 FinitePlaces
variable {K : Type} [Field K]
    [NumberField K]
Lean source · statement
theorem
    sUnitKummerChosenBasePlaces_mem_coordinateBasePlaceCandidates
    {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)) :
    sUnitKummerChosenBasePlaces
        (K := K) (Omega := Omega) E n hmu
        p v hp hv hn r eG S i ∈
      sUnitKummerCoordinateBasePlaceCandidates
        (K := K) (Omega := Omega) E n hmu
        p v hp hv hn r eG S i
theorem

sUnitKummerChosenBasePlaces_not_mem_avoided

L396 ↗
GlobalClassFieldTheory.ClassFieldAxiom.sUnitKummerChosenBasePlaces_not_mem_avoided
Documentation

Every chosen base prime avoids the enlarged support, the ramified primes of the full Kummer extension, and the support of 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 FinitePlaces
variable {K : Type} [Field K]
    [NumberField K]
Lean source · statement
theorem sUnitKummerChosenBasePlaces_not_mem_avoided
    {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)) :
    sUnitKummerChosenBasePlaces
        (K := K) (Omega := Omega) E n hmu
        p v hp hv hn r eG S i ∉
      sUnitKummerAvoidedBasePlaces
        (K := K) (Omega := Omega) E n hmu S
theorem

sUnitKummerChosenBasePlaces_valuation_natCast_eq_one

L425 ↗
GlobalClassFieldTheory.ClassFieldAxiom.sUnitKummerChosenBasePlaces_valuation_natCast_eq_one
Documentation

The exponent n is a unit at every chosen base prime.

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 FinitePlaces
variable {K : Type} [Field K]
    [NumberField K]
Lean source · statement
theorem sUnitKummerChosenBasePlaces_valuation_natCast_eq_one
    {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)) :
    (sUnitKummerChosenBasePlaces
        (K := K) (Omega := Omega) E n hmu
        p v hp hv hn r eG S i).valuation K
          ((n : ℕ) : K) =
      1

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