Module

RationalRamificationSupport.lean

Nyll.SawinTotallyRealTowers.RationalRamificationSupport

5 declarations indexed from sourceView source ↗

Module documentation

Rational primes in the finite ramification support

The canonical identification of the integers of ℚ with ℤ identifies their local unramifiedness conditions. Under the equivalence between finite places of ℚ and positive rational primes, the allowed ramification support therefore contains exactly the prime divisors required by the absolute discriminant.

Imports4

Nyll.SawinTotallyRealTowers.RamificationSupport
Mathlib.NumberTheory.NumberField.Discriminant.Different
Mathlib.NumberTheory.Padics.HeightOneSpectrum
Mathlib.RingTheory.Unramified.Locus

Imported by5

theorem

isUnramifiedAt_rat_iff_int

L30 ↗

ClassFieldTower.Sawin.isUnramifiedAt_rat_iff_int

Documentation

The local unramifiedness conditions over the integers of ℚ and over ℤ agree. The canonical integer map onto 𝓞 ℚ is surjective.

Source context 4 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
universe u
namespace ClassFieldTower.Sawin

Lean source · statement

theorem isUnramifiedAt_rat_iff_int
    (L : Type u) [Field L] [NumberField L]
    (P : Ideal (𝓞 L)) [P.IsPrime] :
    Algebra.IsUnramifiedAt (𝓞 ℚ) P ↔ Algebra.IsUnramifiedAt ℤ P

theorem

rationalPrime_asIdeal

L45 ↗

ClassFieldTower.Sawin.rationalPrime_asIdeal

Source context 4 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
universe u
namespace ClassFieldTower.Sawin

Lean source · statement

theorem rationalPrime_asIdeal (q : Nat.Primes) :
    ((Rat.HeightOneSpectrum.primesEquiv (R := 𝓞 ℚ)).symm q).asIdeal =
      Ideal.span {(q : 𝓞 ℚ)}

theorem

finitePlaceBelow_eq_rationalPrime_iff

L53 ↗

ClassFieldTower.Sawin.finitePlaceBelow_eq_rationalPrime_iff

Source context 4 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
universe u
namespace ClassFieldTower.Sawin

Lean source · statement

theorem finitePlaceBelow_eq_rationalPrime_iff
    (L : Type u) [Field L] [NumberField L]
    (P : HeightOneSpectrum (𝓞 L)) (q : Nat.Primes) :
    finitePlaceBelow (K := ℚ) P =
      (Rat.HeightOneSpectrum.primesEquiv (R := 𝓞 ℚ)).symm q ↔
        (q : 𝓞 L) ∈ P.asIdeal

theorem

not_dvd_discr_iff_finitePlaceBelow

L77 ↗

ClassFieldTower.Sawin.not_dvd_discr_iff_finitePlaceBelow

Source context 4 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
universe u
namespace ClassFieldTower.Sawin

Lean source · statement

theorem not_dvd_discr_iff_finitePlaceBelow
    (L : Type u) [Field L] [NumberField L] (q : Nat.Primes) :
    ¬ (q : ℤ) ∣ NumberField.discr L ↔
      ∀ P : HeightOneSpectrum (𝓞 L),
        finitePlaceBelow (K := ℚ) P =
          (Rat.HeightOneSpectrum.primesEquiv (R := 𝓞 ℚ)).symm q →
            Algebra.IsUnramifiedAt (𝓞 ℚ) P.asIdeal

theorem

isUnramifiedAtFinitePlacesOutside_rat_iff_discr

L110 ↗

ClassFieldTower.Sawin.isUnramifiedAtFinitePlacesOutside_rat_iff_discr

Documentation

A number field is unramified outside the prescribed rational finite places exactly when that set contains every prime divisor of its absolute discriminant. No normality or degree restriction is needed.

Source context 4 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
universe u
namespace ClassFieldTower.Sawin

Lean source · statement

theorem isUnramifiedAtFinitePlacesOutside_rat_iff_discr
    (L : Type u) [Field L] [NumberField L]
    (T : Set (HeightOneSpectrum (𝓞 ℚ))) :
    IsUnramifiedAtFinitePlacesOutside ℚ L T ↔
      ∀ q : Nat.Primes, (q : ℤ) ∣ NumberField.discr L →
        (Rat.HeightOneSpectrum.primesEquiv (R := 𝓞 ℚ)).symm q ∈ T

Module documentation

Rational primes in the finite ramification support

Declarations

isUnramifiedAt_rat_iff_int

rationalPrime_asIdeal

finitePlaceBelow_eq_rationalPrime_iff

not_dvd_discr_iff_finitePlaceBelow

isUnramifiedAtFinitePlacesOutside_rat_iff_discr