NYLL
Module

Setup.lean

Nyll.ClassFieldTheory.KroneckerWeber.Setup
29 declarations indexed from sourceView source ↗

Module documentation

Setup for the global Kronecker--Weber theorem

This file begins the global Kronecker–Weber construction. Two finite abelian extensions, embedded in one separable closure, have a finite abelian compositum. In particular this applies to the given number field and a cyclotomic field. The remaining arithmetic step is to choose the cyclotomic order from the local data and prove that the compositum has no larger degree than the cyclotomic subfield.

Imports8
Imported by4

Declarations

def

kroneckerWeberRamifiedPrimes

L47 ↗
KroneckerWeber.kroneckerWeberRamifiedPrimes
Documentation

The finite set S of ramified rational primes, primes. A prime belongs to this finset precisely when some height-one prime of 𝓞 L above it is ramified.

Source context 11 commands

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

noncomputable section
namespace KroneckerWeber
open AlgebraicNumberTheory
open HilbertRamification
open HilbertRamification.Dedekind
open scoped IsMulCommutative NumberField
section GlobalConductorCandidate
open AlgebraicNumberTheory.Valuations
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]
include hNF in
Lean source · statement
def kroneckerWeberRamifiedPrimes : Finset Nat.Primes
theorem

mem_kroneckerWeberRamifiedPrimes_iff

L59 ↗
KroneckerWeber.mem_kroneckerWeberRamifiedPrimes_iff
Documentation

Membership in the finite ramified-prime set, stated in height-one-prime language.

Source context 11 commands

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

noncomputable section
namespace KroneckerWeber
open AlgebraicNumberTheory
open HilbertRamification
open HilbertRamification.Dedekind
open scoped IsMulCommutative NumberField
section GlobalConductorCandidate
open AlgebraicNumberTheory.Valuations
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]
omit hLab in
Lean source · statement
theorem mem_kroneckerWeberRamifiedPrimes_iff
    (p : Nat.Primes) :
    p ∈ kroneckerWeberRamifiedPrimes (L := L) ↔
      ∃ w : IsDedekindDomain.HeightOneSpectrum (𝓞 L),
        (w.asIdeal : Ideal (𝓞 L)).LiesOver
          ((Rat.HeightOneSpectrum.primesEquiv.symm p).asIdeal : Ideal ℤ) ∧
        ¬ Algebra.IsUnramifiedAt ℤ w.asIdeal
def

kroneckerWeberPadicExtension

L80 ↗
KroneckerWeber.kroneckerWeberPadicExtension
Documentation

A chosen extension to L of the rational p-adic absolute value, constructed by pulling the absolute value on an algebraic closure of the completion back along a chosen embedding.

Source context 11 commands

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

noncomputable section
namespace KroneckerWeber
open AlgebraicNumberTheory
open HilbertRamification
open HilbertRamification.Dedekind
open scoped IsMulCommutative NumberField
section GlobalConductorCandidate
open AlgebraicNumberTheory.Valuations
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]
include hLab in
Lean source · statement
def kroneckerWeberPadicExtension
    (p : ℕ) [Fact p.Prime] :
  AbsoluteValueExtension (Rat.AbsoluteValue.padic p) L
def

kroneckerWeberLocalCyclotomicEmbeddingProperty

L109 ↗
KroneckerWeber.kroneckerWeberLocalCyclotomicEmbeddingProperty
Documentation

The concrete local embedding assertion attached to fixed structured parameters f and n. Its named form hides the localization instances while retaining the actual embedding needed for the ramification estimate in the global argument.

Source context 11 commands

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

noncomputable section
namespace KroneckerWeber
open AlgebraicNumberTheory
open HilbertRamification
open HilbertRamification.Dedekind
open scoped IsMulCommutative NumberField
section GlobalConductorCandidate
open AlgebraicNumberTheory.Valuations
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]
include L hNF hLab in
Lean source · statement
def kroneckerWeberLocalCyclotomicEmbeddingProperty
    (p : Nat.Primes) (f n : ℕ) : Prop
structure

KroneckerWeberLocalCyclotomicData

L131 ↗
KroneckerWeber.KroneckerWeberLocalCyclotomicData
Documentation

The synchronized local data chosen from structured local Kronecker--Weber. In particular, the ramification exponent below and the embedding used to bound it come from one and the same witness.

Source context 10 commands

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

noncomputable section
namespace KroneckerWeber
open AlgebraicNumberTheory
open HilbertRamification
open HilbertRamification.Dedekind
open scoped IsMulCommutative NumberField
section GlobalConductorCandidate
open AlgebraicNumberTheory.Valuations
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]
Lean source · full declaration
structure KroneckerWeberLocalCyclotomicData (p : Nat.Primes) where
  /-- The unramified-degree parameter in the local cyclotomic order. -/
  unramifiedDegree : ℕ
  /-- The exponent of the `p`-power factor in the local cyclotomic order. -/
  ramificationExponent : ℕ
  /-- Positivity of the chosen unramified-degree parameter. -/
  unramifiedDegree_pos : 0 < unramifiedDegree
  /-- Positivity of the chosen ramification exponent. -/
  ramificationExponent_pos : 1 ≤ ramificationExponent
  /-- The structured local embedding associated with the two chosen parameters. -/
  embedding : kroneckerWeberLocalCyclotomicEmbeddingProperty
    (L := L) p unramifiedDegree ramificationExponent
def

kroneckerWeberLocalCyclotomicData

L146 ↗
KroneckerWeber.kroneckerWeberLocalCyclotomicData
Documentation

A chosen structured local cyclotomic witness at p.

Source context 11 commands

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

noncomputable section
namespace KroneckerWeber
open AlgebraicNumberTheory
open HilbertRamification
open HilbertRamification.Dedekind
open scoped IsMulCommutative NumberField
section GlobalConductorCandidate
open AlgebraicNumberTheory.Valuations
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]
include L hNF hLab in
Lean source · statement
def kroneckerWeberLocalCyclotomicData
    (p : Nat.Primes) :
    KroneckerWeberLocalCyclotomicData (L := L) p
def

kroneckerWeberLocalUnramifiedDegree

L164 ↗
KroneckerWeber.kroneckerWeberLocalUnramifiedDegree
Documentation

The prime-to-p residue degree in the chosen structured local cyclotomic witness.

Source context 11 commands

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

noncomputable section
namespace KroneckerWeber
open AlgebraicNumberTheory
open HilbertRamification
open HilbertRamification.Dedekind
open scoped IsMulCommutative NumberField
section GlobalConductorCandidate
open AlgebraicNumberTheory.Valuations
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]
include L hNF hLab in
Lean source · statement
def kroneckerWeberLocalUnramifiedDegree
    (p : Nat.Primes) : ℕ
def

kroneckerWeberLocalRamificationExponent

L171 ↗
KroneckerWeber.kroneckerWeberLocalRamificationExponent
Documentation

The p-power exponent supplied by the structured local Kronecker--Weber theorem for the chosen completion of L at p.

Source context 11 commands

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

noncomputable section
namespace KroneckerWeber
open AlgebraicNumberTheory
open HilbertRamification
open HilbertRamification.Dedekind
open scoped IsMulCommutative NumberField
section GlobalConductorCandidate
open AlgebraicNumberTheory.Valuations
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]
include L hNF hLab in
Lean source · statement
def kroneckerWeberLocalRamificationExponent
    (p : Nat.Primes) : ℕ
theorem

kroneckerWeberLocalUnramifiedDegree_pos

L177 ↗
KroneckerWeber.kroneckerWeberLocalUnramifiedDegree_pos
Documentation

The chosen prime-to-p residue degree is positive.

Source context 11 commands

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

noncomputable section
namespace KroneckerWeber
open AlgebraicNumberTheory
open HilbertRamification
open HilbertRamification.Dedekind
open scoped IsMulCommutative NumberField
section GlobalConductorCandidate
open AlgebraicNumberTheory.Valuations
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]
include L hNF in
Lean source · statement
theorem kroneckerWeberLocalUnramifiedDegree_pos
    (p : Nat.Primes) :
    0 < kroneckerWeberLocalUnramifiedDegree (L := L) p
theorem

kroneckerWeberLocalCyclotomicEmbedding

L186 ↗
KroneckerWeber.kroneckerWeberLocalCyclotomicEmbedding
Documentation

The actual local cyclotomic embedding selected together with the two local exponents.

Source context 11 commands

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

noncomputable section
namespace KroneckerWeber
open AlgebraicNumberTheory
open HilbertRamification
open HilbertRamification.Dedekind
open scoped IsMulCommutative NumberField
section GlobalConductorCandidate
open AlgebraicNumberTheory.Valuations
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]
include L hNF in
Lean source · statement
theorem kroneckerWeberLocalCyclotomicEmbedding
    (p : Nat.Primes) :
    kroneckerWeberLocalCyclotomicEmbeddingProperty
      (L := L) p
      (kroneckerWeberLocalUnramifiedDegree (L := L) p)
      (kroneckerWeberLocalRamificationExponent (L := L) p)
def

kroneckerWeberConductorCandidate

L197 ↗
KroneckerWeber.kroneckerWeberConductorCandidate
Documentation

The cyclotomic order n = ∏_{p ∈ S} p^{e_p} chosen from the ramification support.

Source context 11 commands

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

noncomputable section
namespace KroneckerWeber
open AlgebraicNumberTheory
open HilbertRamification
open HilbertRamification.Dedekind
open scoped IsMulCommutative NumberField
section GlobalConductorCandidate
open AlgebraicNumberTheory.Valuations
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]
include L hNF hLab in
Lean source · statement
def kroneckerWeberConductorCandidate : ℕ
def

kroneckerWeberConductorCoprimePart

L203 ↗
KroneckerWeber.kroneckerWeberConductorCoprimePart
Documentation

The part of the conductor candidate supported away from p.

Source context 11 commands

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

noncomputable section
namespace KroneckerWeber
open AlgebraicNumberTheory
open HilbertRamification
open HilbertRamification.Dedekind
open scoped IsMulCommutative NumberField
section GlobalConductorCandidate
open AlgebraicNumberTheory.Valuations
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]
include L hNF hLab in
Lean source · statement
def kroneckerWeberConductorCoprimePart
    (p : Nat.Primes) : ℕ
theorem

kroneckerWeberConductorCandidate_eq_primePower_mul_coprimePart

L211 ↗
KroneckerWeber.kroneckerWeberConductorCandidate_eq_primePower_mul_coprimePart
Documentation

At a ramified prime p, the conductor candidate splits into its chosen p-primary order and the product supported at the other ramified primes.

Source context 11 commands

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

noncomputable section
namespace KroneckerWeber
open AlgebraicNumberTheory
open HilbertRamification
open HilbertRamification.Dedekind
open scoped IsMulCommutative NumberField
section GlobalConductorCandidate
open AlgebraicNumberTheory.Valuations
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]
include L hNF in
Lean source · statement
theorem kroneckerWeberConductorCandidate_eq_primePower_mul_coprimePart
    (p : Nat.Primes)
    (hp : p ∈ kroneckerWeberRamifiedPrimes (L := L)) :
    kroneckerWeberConductorCandidate (L := L) =
      p.1 ^ kroneckerWeberLocalRamificationExponent (L := L) p *
        kroneckerWeberConductorCoprimePart (L := L) p
theorem

kroneckerWeberConductorCoprimePart_coprime

L226 ↗
KroneckerWeber.kroneckerWeberConductorCoprimePart_coprime
Documentation

The complementary factor really is prime to p; this is the arithmetic input which makes it part of the unramified factor in the local cyclotomic field used in the global construction.

Source context 11 commands

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

noncomputable section
namespace KroneckerWeber
open AlgebraicNumberTheory
open HilbertRamification
open HilbertRamification.Dedekind
open scoped IsMulCommutative NumberField
section GlobalConductorCandidate
open AlgebraicNumberTheory.Valuations
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]
include L hNF in
Lean source · statement
theorem kroneckerWeberConductorCoprimePart_coprime
    (p : Nat.Primes) :
    Nat.Coprime p.1
      (kroneckerWeberConductorCoprimePart (L := L) p)
theorem

kroneckerWeberConductorCandidate_pos

L241 ↗
KroneckerWeber.kroneckerWeberConductorCandidate_pos
Documentation

The constructed global cyclotomic order is nonzero.

Source context 11 commands

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

noncomputable section
namespace KroneckerWeber
open AlgebraicNumberTheory
open HilbertRamification
open HilbertRamification.Dedekind
open scoped IsMulCommutative NumberField
section GlobalConductorCandidate
open AlgebraicNumberTheory.Valuations
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]
include L hNF in
Lean source · statement
theorem kroneckerWeberConductorCandidate_pos :
    0 < kroneckerWeberConductorCandidate (L := L)
instance

kroneckerWeberConductorCandidate_neZero

L259 ↗
KroneckerWeber.kroneckerWeberConductorCandidate_neZero
Documentation

The conductor candidate is nonzero.

Source context 10 commands

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

noncomputable section
namespace KroneckerWeber
open AlgebraicNumberTheory
open HilbertRamification
open HilbertRamification.Dedekind
open scoped IsMulCommutative NumberField
section GlobalCompositum
open AlgebraicNumberTheory.Valuations
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]
Lean source · statement
instance kroneckerWeberConductorCandidate_neZero :
    NeZero (kroneckerWeberConductorCandidate (L := L))
instance

kroneckerWeberCyclotomicField_isAbelianGalois

L265 ↗
KroneckerWeber.kroneckerWeberCyclotomicField_isAbelianGalois
Documentation

The cyclotomic field at the conductor candidate is abelian Galois over the rationals.

Source context 10 commands

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

noncomputable section
namespace KroneckerWeber
open AlgebraicNumberTheory
open HilbertRamification
open HilbertRamification.Dedekind
open scoped IsMulCommutative NumberField
section GlobalCompositum
open AlgebraicNumberTheory.Valuations
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]
Lean source · statement
instance kroneckerWeberCyclotomicField_isAbelianGalois :
    IsAbelianGalois ℚ
      (CyclotomicField (kroneckerWeberConductorCandidate (L := L)) ℚ)
def

kroneckerWeberCompositumField

L276 ↗
KroneckerWeber.kroneckerWeberCompositumField
Documentation

The concrete compositum M = L(μ_n) in a fixed separable closure of ℚ, for the conductor candidate constructed above.

Source context 11 commands

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

noncomputable section
namespace KroneckerWeber
open AlgebraicNumberTheory
open HilbertRamification
open HilbertRamification.Dedekind
open scoped IsMulCommutative NumberField
section GlobalCompositum
open AlgebraicNumberTheory.Valuations
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]
include L hNF hLab in
Lean source · statement
def kroneckerWeberCompositumField :
    IntermediateField ℚ (SeparableClosure ℚ)
instance

kroneckerWeberCompositumField_finiteDimensional

L283 ↗
KroneckerWeber.kroneckerWeberCompositumField_finiteDimensional
Documentation

The global Kronecker--Weber compositum is finite-dimensional over the rationals.

Source context 10 commands

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

noncomputable section
namespace KroneckerWeber
open AlgebraicNumberTheory
open HilbertRamification
open HilbertRamification.Dedekind
open scoped IsMulCommutative NumberField
section GlobalCompositum
open AlgebraicNumberTheory.Valuations
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]
Lean source · statement
instance kroneckerWeberCompositumField_finiteDimensional :
    FiniteDimensional ℚ (kroneckerWeberCompositumField L)
instance

kroneckerWeberCompositumField_isAbelianGalois

L292 ↗
KroneckerWeber.kroneckerWeberCompositumField_isAbelianGalois
Documentation

The global Kronecker--Weber compositum is abelian Galois over the rationals.

Source context 10 commands

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

noncomputable section
namespace KroneckerWeber
open AlgebraicNumberTheory
open HilbertRamification
open HilbertRamification.Dedekind
open scoped IsMulCommutative NumberField
section GlobalCompositum
open AlgebraicNumberTheory.Valuations
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]
Lean source · statement
instance kroneckerWeberCompositumField_isAbelianGalois :
    IsAbelianGalois ℚ (kroneckerWeberCompositumField L)
instance

kroneckerWeberCompositumField_numberField

L298 ↗
KroneckerWeber.kroneckerWeberCompositumField_numberField
Documentation

The global Kronecker--Weber compositum is a number field.

Source context 10 commands

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

noncomputable section
namespace KroneckerWeber
open AlgebraicNumberTheory
open HilbertRamification
open HilbertRamification.Dedekind
open scoped IsMulCommutative NumberField
section GlobalCompositum
open AlgebraicNumberTheory.Valuations
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]
Lean source · statement
instance kroneckerWeberCompositumField_numberField :
    NumberField (kroneckerWeberCompositumField L)
def

kroneckerWeberCompositumEmbeddingLeft

L303 ↗
KroneckerWeber.kroneckerWeberCompositumEmbeddingLeft
Documentation

The original abelian extension embeds into M = L(μ_n).

Source context 11 commands

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

noncomputable section
namespace KroneckerWeber
open AlgebraicNumberTheory
open HilbertRamification
open HilbertRamification.Dedekind
open scoped IsMulCommutative NumberField
section GlobalCompositum
open AlgebraicNumberTheory.Valuations
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]
include L hNF hLab in
Lean source · statement
def kroneckerWeberCompositumEmbeddingLeft :
    L →ₐ[ℚ] kroneckerWeberCompositumField L
def

kroneckerWeberCompositumEmbeddingRight

L310 ↗
KroneckerWeber.kroneckerWeberCompositumEmbeddingRight
Documentation

The conductor cyclotomic field embeds into M = L(μ_n).

Source context 11 commands

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

noncomputable section
namespace KroneckerWeber
open AlgebraicNumberTheory
open HilbertRamification
open HilbertRamification.Dedekind
open scoped IsMulCommutative NumberField
section GlobalCompositum
open AlgebraicNumberTheory.Valuations
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]
include L hNF hLab in
Lean source · statement
def kroneckerWeberCompositumEmbeddingRight :
    CyclotomicField (kroneckerWeberConductorCandidate (L := L)) ℚ →ₐ[ℚ]
      kroneckerWeberCompositumField L
def

kroneckerWeberCompositumLeftField

L318 ↗
KroneckerWeber.kroneckerWeberCompositumLeftField
Documentation

The copy of L inside the concrete compositum.

Source context 11 commands

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

noncomputable section
namespace KroneckerWeber
open AlgebraicNumberTheory
open HilbertRamification
open HilbertRamification.Dedekind
open scoped IsMulCommutative NumberField
section GlobalCompositum
open AlgebraicNumberTheory.Valuations
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]
include L hNF hLab in
Lean source · statement
def kroneckerWeberCompositumLeftField :
    IntermediateField ℚ (kroneckerWeberCompositumField L)
def

kroneckerWeberCompositumLeftEquiv

L325 ↗
KroneckerWeber.kroneckerWeberCompositumLeftEquiv
Documentation

The chosen copy of L in the compositum is canonically isomorphic to L.

Source context 11 commands

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

noncomputable section
namespace KroneckerWeber
open AlgebraicNumberTheory
open HilbertRamification
open HilbertRamification.Dedekind
open scoped IsMulCommutative NumberField
section GlobalCompositum
open AlgebraicNumberTheory.Valuations
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]
include L hNF hLab in
Lean source · statement
def kroneckerWeberCompositumLeftEquiv :
    L ≃ₐ[ℚ] kroneckerWeberCompositumLeftField (L := L)
theorem

kroneckerWeberCyclotomic_finrank_le_compositum

L332 ↗
KroneckerWeber.kroneckerWeberCyclotomic_finrank_le_compositum
Documentation

The elementary lower degree bound for the cyclotomic factor of M.

Source context 11 commands

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

noncomputable section
namespace KroneckerWeber
open AlgebraicNumberTheory
open HilbertRamification
open HilbertRamification.Dedekind
open scoped IsMulCommutative NumberField
section GlobalCompositum
open AlgebraicNumberTheory.Valuations
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]
include L hNF hLab in
Lean source · statement
theorem kroneckerWeberCyclotomic_finrank_le_compositum :
      Module.finrank ℚ
        (CyclotomicField (kroneckerWeberConductorCandidate (L := L)) ℚ) ≤
      Module.finrank ℚ (kroneckerWeberCompositumField L)
def

kroneckerWeberCompositumEquivCyclotomicOfFinrankLe

L343 ↗
KroneckerWeber.kroneckerWeberCompositumEquivCyclotomicOfFinrankLe
Documentation

Once the global inertia count supplies the upper degree bound, the cyclotomic inclusion in M is an isomorphism. This isolates the purely linear-algebraic final step of the global construction.

Source context 11 commands

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

noncomputable section
namespace KroneckerWeber
open AlgebraicNumberTheory
open HilbertRamification
open HilbertRamification.Dedekind
open scoped IsMulCommutative NumberField
section GlobalCompositum
open AlgebraicNumberTheory.Valuations
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]
include L hNF hLab in
Lean source · statement
def kroneckerWeberCompositumEquivCyclotomicOfFinrankLe
    (hupper :
      Module.finrank ℚ (kroneckerWeberCompositumField L) ≤
        Nat.totient (kroneckerWeberConductorCandidate (L := L))) :
    kroneckerWeberCompositumField L ≃ₐ[ℚ]
      CyclotomicField (kroneckerWeberConductorCandidate (L := L)) ℚ
def

kroneckerWeberEmbeddingOfCompositumFinrankLe

L373 ↗
KroneckerWeber.kroneckerWeberEmbeddingOfCompositumFinrankLe
Documentation

The promised embedding of L into the conductor cyclotomic field, deduced from the global upper degree bound.

Source context 11 commands

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

noncomputable section
namespace KroneckerWeber
open AlgebraicNumberTheory
open HilbertRamification
open HilbertRamification.Dedekind
open scoped IsMulCommutative NumberField
section GlobalCompositum
open AlgebraicNumberTheory.Valuations
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]
include L hNF hLab in
Lean source · statement
def kroneckerWeberEmbeddingOfCompositumFinrankLe
    (hupper :
      Module.finrank ℚ (kroneckerWeberCompositumField L) ≤
        Nat.totient (kroneckerWeberConductorCandidate (L := L))) :
    L →ₐ[ℚ]
      CyclotomicField (kroneckerWeberConductorCandidate (L := L)) ℚ
def

kroneckerWeberCompositumPrimeAbove

L385 ↗
KroneckerWeber.kroneckerWeberCompositumPrimeAbove
Documentation

A chosen prime of M = L(μ_n) over the rational prime p.

Source context 11 commands

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

noncomputable section
namespace KroneckerWeber
open AlgebraicNumberTheory
open HilbertRamification
open HilbertRamification.Dedekind
open scoped IsMulCommutative NumberField
section GlobalCompositum
open AlgebraicNumberTheory.Valuations
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]
include L hNF hLab in
Lean source · statement
def kroneckerWeberCompositumPrimeAbove
    (p : Nat.Primes) :
    Ideal.primesOver
      ((Rat.HeightOneSpectrum.primesEquiv.symm p).asIdeal : Ideal ℤ)
      (𝓞 (kroneckerWeberCompositumField L))

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