Module

PrimeSet.lean

Nyll.ClassFieldTheory.GlobalClassFieldTheory.ClassFieldAxiom.SUnitKummerPrimeSelection.PrimeSet

3 declarations indexed from sourceView source ↗

Module documentation

The finite prime set for an S-unit Kummer extension

This file packages the chosen base places as a finite set and proves its cardinality and disjointness properties.

Imports1

Nyll.ClassFieldTheory.GlobalClassFieldTheory.ClassFieldAxiom.SUnitKummerPrimeSelection.BasePlaceSelection

Imported by3

def

sUnitKummerPrimeSet

L34 ↗

GlobalClassFieldTheory.ClassFieldAxiom.sUnitKummerPrimeSet

Documentation

The finite set T of primes chosen for the coordinate cyclic extensions that detect the enlarged S-unit Kummer radical.

Source context 8 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]
open scoped Classical in

Lean source · statement

def sUnitKummerPrimeSet
    {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))) :
    Finset (HeightOneSpectrum (𝓞 K))

theorem

sUnitKummerPrimeSet_card

L57 ↗

GlobalClassFieldTheory.ClassFieldAxiom.sUnitKummerPrimeSet_card

Documentation

The chosen prime set has the required cardinality s-r.

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 sUnitKummerPrimeSet_card
    {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))) :
    (sUnitKummerPrimeSet
      (K := K) (Omega := Omega) E n hmu
      p v hp hv hn r eG S).card =
        sUnitKummerPrimeCount
          (K := K) E n hmu r S

theorem

sUnitKummerPrimeSet_disjoint_enlargeByFiniteKummerRadicalSupport

L86 ↗

GlobalClassFieldTheory.ClassFieldAxiom.sUnitKummerPrimeSet_disjoint_enlargeByFiniteKummerRadicalSupport

Documentation

The chosen prime set is disjoint from the enlarged finite Kummer-radical support.

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 sUnitKummerPrimeSet_disjoint_enlargeByFiniteKummerRadicalSupport
    {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))) :
    Disjoint
      (sUnitKummerPrimeSet
        (K := K) (Omega := Omega) E n hmu
        p v hp hv hn r eG S)
      (enlargeByFiniteKummerRadicalSupport
        (K := K) (L := E) n hmu S)

Module documentation

The finite prime set for an S-unit Kummer extension

Declarations

sUnitKummerPrimeSet

sUnitKummerPrimeSet_card

sUnitKummerPrimeSet_disjoint_enlargeByFiniteKummerRadicalSupport