Module

Final.lean

Nyll.ClassFieldTheory.KroneckerWeber.Final

2 declarations indexed from sourceView source ↗

Module documentation

Global Kronecker--Weber

The synchronized prime above each member of the finite ramification support has inertia cardinality at most the corresponding prime-power totient. Outside that support the auxiliary compositum is unramified. The finite inertia groups therefore generate its full abelian Galois group, and their product bounds its degree by the degree of the conductor cyclotomic field.

Imports4

Imported by2

theorem

kroneckerWeberCompositum_finrank_le_totient

L37 ↗

KroneckerWeber.kroneckerWeberCompositum_finrank_le_totient

Documentation

The global degree estimate which completes the arithmetic part of the Kronecker–Weber argument.

Source context 9 commands

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

noncomputable section
namespace KroneckerWeber
open NumberField
open AlgebraicNumberTheory
open AlgebraicNumberTheory.Ramification
open HilbertRamification.Dedekind
open scoped NumberField
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]

Lean source · statement

theorem kroneckerWeberCompositum_finrank_le_totient :
    Module.finrank ℚ (kroneckerWeberCompositumField L) ≤
      Nat.totient (kroneckerWeberConductorCandidate (L := L))

def

kroneckerWeberCyclotomicEmbedding

L120 ↗

KroneckerWeber.kroneckerWeberCyclotomicEmbedding