Module

GlobalCompositumCyclotomicTarget.lean

Nyll.ClassFieldTheory.KroneckerWeber.GlobalCompositumCyclotomicTarget

6 declarations indexed from sourceView source ↗

Module documentation

The common local cyclotomic target

At a ramified prime p, the structured local embedding of L has order (p^f - 1) * p^e, while the global conductor has order p^e * c with c prime to p. Their common target has order ((p^f - 1) * c) * p^e; crucially, it uses the same exponent e.

Imports1

Nyll.ClassFieldTheory.KroneckerWeber.Setup

Imported by3

def

kroneckerWeberLocalCompositumCoprimePart

L26 ↗

KroneckerWeber.kroneckerWeberLocalCompositumCoprimePart

Documentation

The prime-to-p factor of the common local target.

Source context 4 commands

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

noncomputable section
namespace KroneckerWeber
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]

Lean source · statement

def kroneckerWeberLocalCompositumCoprimePart
    (p : Nat.Primes) : ℕ

def

kroneckerWeberLocalCompositumOrder

L33 ↗

KroneckerWeber.kroneckerWeberLocalCompositumOrder

Documentation

The common local cyclotomic order, retaining exactly the conductor exponent chosen at p.

Source context 4 commands

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

noncomputable section
namespace KroneckerWeber
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]

Lean source · statement

def kroneckerWeberLocalCompositumOrder
    (p : Nat.Primes) : ℕ

theorem

kroneckerWeberLocalCompositumCoprimePart_coprime

L39 ↗

KroneckerWeber.kroneckerWeberLocalCompositumCoprimePart_coprime

Documentation

The prime-to-p part of the common local target is coprime to p.

Source context 4 commands

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

noncomputable section
namespace KroneckerWeber
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]

Lean source · statement

theorem kroneckerWeberLocalCompositumCoprimePart_coprime
    (p : Nat.Primes) :
    Nat.Coprime p.1
      (kroneckerWeberLocalCompositumCoprimePart (L := L) p)

theorem

kroneckerWeberLocalCompositumOrder_pos

L70 ↗

KroneckerWeber.kroneckerWeberLocalCompositumOrder_pos

Documentation

The common local cyclotomic order is positive.

Source context 4 commands

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

noncomputable section
namespace KroneckerWeber
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]

Lean source · statement

theorem kroneckerWeberLocalCompositumOrder_pos
    (p : Nat.Primes) :
    0 < kroneckerWeberLocalCompositumOrder (L := L) p

theorem

kroneckerWeberLocalStructuredOrder_dvd_compositumOrder

L85 ↗

KroneckerWeber.kroneckerWeberLocalStructuredOrder_dvd_compositumOrder

Documentation

The structured local cyclotomic order divides the common local order.

Source context 4 commands

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

noncomputable section
namespace KroneckerWeber
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]

Lean source · statement

theorem kroneckerWeberLocalStructuredOrder_dvd_compositumOrder
    (p : Nat.Primes) :
    (p.1 ^ kroneckerWeberLocalUnramifiedDegree (L := L) p - 1) *
        p.1 ^ kroneckerWeberLocalRamificationExponent (L := L) p ∣
      kroneckerWeberLocalCompositumOrder (L := L) p

theorem

kroneckerWeberConductorCandidate_dvd_localCompositumOrder

L97 ↗

KroneckerWeber.kroneckerWeberConductorCandidate_dvd_localCompositumOrder

Documentation

At a ramified prime, the global conductor candidate divides the common local cyclotomic order.

Source context 4 commands

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

noncomputable section
namespace KroneckerWeber
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]

Lean source · statement

theorem kroneckerWeberConductorCandidate_dvd_localCompositumOrder
    (p : Nat.Primes)
    (hp : p ∈ kroneckerWeberRamifiedPrimes (L := L)) :
    kroneckerWeberConductorCandidate (L := L) ∣
      kroneckerWeberLocalCompositumOrder (L := L) p

Module documentation

The common local cyclotomic target

Declarations

kroneckerWeberLocalCompositumCoprimePart

kroneckerWeberLocalCompositumOrder

kroneckerWeberLocalCompositumCoprimePart_coprime

kroneckerWeberLocalCompositumOrder_pos

kroneckerWeberLocalStructuredOrder_dvd_compositumOrder

kroneckerWeberConductorCandidate_dvd_localCompositumOrder