NYLL
Module

UnramifiedCompositumSupport.lean

Nyll.ClassFieldTheory.KroneckerWeber.UnramifiedCompositumSupport
4 declarations indexed from sourceView source ↗

Module documentation

Ramification support of the auxiliary compositum

Let S be the finite set of rational primes ramified in L, let n = ∏ p∈S, p ^ e_p, and put M = L(μ_n). This file proves the global ramification assertion used in the inertia count: every finite prime of M outside S is unramified over ℤ.

The two factors are unramified outside S for different reasons. For L this is the definition of S; for the cyclotomic factor it is the standard formula saying that a rational prime not dividing the conductor has ramification index one. An inertia automorphism of the compositum restricts to inertia automorphisms of both factors. Since the factors generate the compositum, triviality of both restrictions implies triviality of the original inertia automorphism.

Imports4
Imported by3

Declarations

theorem

kroneckerWeber_prime_not_dvd_conductorCandidate

L46 ↗
KroneckerWeber.kroneckerWeber_prime_not_dvd_conductorCandidate
Documentation

A rational prime outside S does not divide the conductor candidate, whose prime-power factors are supported exactly on S.

Source context 9 commands

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

noncomputable section
namespace KroneckerWeber
open NumberField
open HilbertRamification.Dedekind
open AlgebraicNumberTheory.Ramification
open scoped NumberField
attribute [local instance] Ideal.Quotient.field
section ConductorSupport
variable (L : Type) [Field L] [NumberField L] [IsAbelianGalois ℚ L]
Lean source · statement
theorem kroneckerWeber_prime_not_dvd_conductorCandidate
    (p : Nat.Primes)
    (hp : p ∉ kroneckerWeberRamifiedPrimes (L := L)) :
    ¬ p.1 ∣ kroneckerWeberConductorCandidate (L := L)
theorem

kroneckerWeber_leftFactor_ramificationIdx_eq_one

L68 ↗
KroneckerWeber.kroneckerWeber_leftFactor_ramificationIdx_eq_one
Documentation

The copy of L in any isomorphic realization has ramification index one above a rational prime outside the defining support S.

Source context 10 commands

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

noncomputable section
namespace KroneckerWeber
open NumberField
open HilbertRamification.Dedekind
open AlgebraicNumberTheory.Ramification
open scoped NumberField
attribute [local instance] Ideal.Quotient.field
section FactorRamification
variable (L : Type) [Field L] [NumberField L] [IsAbelianGalois ℚ L]
omit [IsAbelianGalois ℚ L] in
Lean source · statement
theorem kroneckerWeber_leftFactor_ramificationIdx_eq_one
    {A : Type*} [Field A] [NumberField A]
    (eLA : L ≃ₐ[ℚ] A)
    (p : Nat.Primes)
    (hpS : p ∉ kroneckerWeberRamifiedPrimes (L := L))
    (PA : Ideal (𝓞 A)) [PA.IsPrime]
    [PA.LiesOver (rationalPrimeIdeal p)] :
    PA.ramificationIdx ℤ = 1
theorem

kroneckerWeber_cyclotomicFactor_ramificationIdx_eq_one

L111 ↗
KroneckerWeber.kroneckerWeber_cyclotomicFactor_ramificationIdx_eq_one
Documentation

The conductor cyclotomic factor has ramification index one outside S, since primes outside S do not divide the conductor candidate.

Source context 9 commands

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

noncomputable section
namespace KroneckerWeber
open NumberField
open HilbertRamification.Dedekind
open AlgebraicNumberTheory.Ramification
open scoped NumberField
attribute [local instance] Ideal.Quotient.field
section FactorRamification
variable (L : Type) [Field L] [NumberField L] [IsAbelianGalois ℚ L]
Lean source · statement
theorem kroneckerWeber_cyclotomicFactor_ramificationIdx_eq_one
    {B : Type*} [Field B] [NumberField B]
    (eCB :
      CyclotomicField (kroneckerWeberConductorCandidate (L := L)) ℚ
        ≃ₐ[ℚ] B)
    (p : Nat.Primes)
    (hpS : p ∉ kroneckerWeberRamifiedPrimes (L := L))
    (PB : Ideal (𝓞 B)) [PB.IsPrime]
    [PB.LiesOver (rationalPrimeIdeal p)] :
    PB.ramificationIdx ℤ = 1
theorem

kroneckerWeberCompositum_isUnramifiedAt_of_not_mem

L170 ↗
KroneckerWeber.kroneckerWeberCompositum_isUnramifiedAt_of_not_mem
Documentation

Ramification support of a realization of the auxiliary compositum. If the copies of L and the conductor cyclotomic field generate M, every finite prime of M outside the ramification support of L is unramified over ℤ.

Source context 10 commands

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

noncomputable section
namespace KroneckerWeber
open NumberField
open HilbertRamification.Dedekind
open AlgebraicNumberTheory.Ramification
open scoped NumberField
attribute [local instance] Ideal.Quotient.field
section CompositumSupport
variable (L : Type) [Field L]
variable [hNF : NumberField L] [hLab : IsAbelianGalois ℚ L]
Lean source · statement
theorem kroneckerWeberCompositum_isUnramifiedAt_of_not_mem
    {M : Type*} [Field M] [NumberField M] [IsGalois ℚ M]
    (A B : IntermediateField ℚ M) [Normal ℚ A] [Normal ℚ B]
    (eLA : L ≃ₐ[ℚ] A)
    (eCB :
      CyclotomicField (kroneckerWeberConductorCandidate (L := L)) ℚ
        ≃ₐ[ℚ] B)
    (hsup : A ⊔ B = ⊤)
    (Q : Ideal (𝓞 M))
    [Q.IsPrime] [Q.IsMaximal]
    (hQoutside :
      ¬ ∃ p ∈ kroneckerWeberRamifiedPrimes (L := L),
        rationalPrimeIdeal p = Q.under ℤ) :
    Algebra.IsUnramifiedAt ℤ Q

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