Module

CompletelySplitPrimes.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.NumberField.CompletelySplitPrimes

5 declarations indexed from sourceView source ↗

Module documentation

Completely split primes of number fields

Unramified degree-one primes in a finite Galois number field give complete splitting above the canonical rational finite place. Such primes exist outside any specified finite set.

Imports7

Nyll.ClassFieldTheory.AlgebraicNumberTheory.NumberField.DegreeOnePrimes
Nyll.ClassFieldTheory.AlgebraicNumberTheory.Ramification.Splitting.FinitePlaceIdeal
Nyll.ValuedFieldTheory.Ramification.HilbertRamification.Dedekind.Basic
Mathlib.FieldTheory.Galois.IsGaloisGroup
Mathlib.NumberTheory.Padics.HeightOneSpectrum
Mathlib.RingTheory.RamificationInertia.Ramification
Mathlib.Algebra.Group.Subgroup.Finite

Imported by3

theorem

rationalPrimePlace_asIdeal

L30 ↗

AlgebraicNumberTheory.PrimeSelection.rationalPrimePlace_asIdeal

Documentation

The canonical place of a rational prime is the principal prime ideal in the actual ring of integers of ℚ.

Source context 3 commands

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

open scoped NumberField Pointwise
open NumberField IsDedekindDomain HilbertRamification.Dedekind
namespace AlgebraicNumberTheory.PrimeSelection

Lean source · statement

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

theorem

under_rational_prime_eq_span

L37 ↗

AlgebraicNumberTheory.PrimeSelection.under_rational_prime_eq_span

Source context 3 commands

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

open scoped NumberField Pointwise
open NumberField IsDedekindDomain HilbertRamification.Dedekind
namespace AlgebraicNumberTheory.PrimeSelection

Lean source · statement

theorem under_rational_prime_eq_span
    (K : Type*) [Field K] [NumberField K] (q : ℕ)
    (W : HeightOneSpectrum (𝓞 K))
    (hOver : W.asIdeal.LiesOver (Ideal.span ({(q : ℤ)} : Set ℤ))) :
    W.asIdeal.under (𝓞 ℚ) = Ideal.span ({(q : 𝓞 ℚ)} : Set (𝓞 ℚ))

theorem

finitePlaceBelow_eq_rationalPrimePlace

L58 ↗

AlgebraicNumberTheory.PrimeSelection.finitePlaceBelow_eq_rationalPrimePlace

Documentation

A prime above q in a number field lies above the canonical rational finite place of q.

Source context 3 commands

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

open scoped NumberField Pointwise
open NumberField IsDedekindDomain HilbertRamification.Dedekind
namespace AlgebraicNumberTheory.PrimeSelection

Lean source · statement

theorem finitePlaceBelow_eq_rationalPrimePlace
    (K : Type*) [Field K] [NumberField K] (q : Nat.Primes)
    (W : HeightOneSpectrum (𝓞 K))
    (hOver : W.asIdeal.LiesOver (Ideal.span ({(q.val : ℤ)} : Set ℤ))) :
    finitePlaceBelow (K := ℚ) W =
      (Rat.HeightOneSpectrum.primesEquiv (R := 𝓞 ℚ)).symm q

theorem

finitePlaceSplitsCompletely_of_unramified_degree_one

L70 ↗

AlgebraicNumberTheory.PrimeSelection.finitePlaceSplitsCompletely_of_unramified_degree_one

Documentation

For a finite Galois number field, an unramified degree-one prime has trivial decomposition group, hence gives complete splitting.

Source context 3 commands

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

open scoped NumberField Pointwise
open NumberField IsDedekindDomain HilbertRamification.Dedekind
namespace AlgebraicNumberTheory.PrimeSelection

Lean source · statement

theorem finitePlaceSplitsCompletely_of_unramified_degree_one
    (K : Type) [Field K] [NumberField K] [IsGalois ℚ K]
    (q : Nat.Primes) (W : HeightOneSpectrum (𝓞 K))
    (hOver : W.asIdeal.LiesOver (Ideal.span ({(q.val : ℤ)} : Set ℤ)))
    (hf : W.asIdeal.inertiaDeg ℤ = 1)
    (hU : Algebra.IsUnramifiedAt ℤ W.asIdeal) :
    FinitePlaceSplitsCompletely (K := ℚ) (L := K)
      ((Rat.HeightOneSpectrum.primesEquiv (R := 𝓞 ℚ)).symm q)

theorem

exists_completelySplitPrime_not_mem

L105 ↗

AlgebraicNumberTheory.PrimeSelection.exists_completelySplitPrime_not_mem

Documentation

There is a completely split rational prime outside every finite set.

Source context 3 commands

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

open scoped NumberField Pointwise
open NumberField IsDedekindDomain HilbertRamification.Dedekind
namespace AlgebraicNumberTheory.PrimeSelection

Lean source · statement

theorem exists_completelySplitPrime_not_mem
    (K : Type) [Field K] [NumberField K] [IsGalois ℚ K] (bad : Finset ℕ) :
    ∃ q : Nat.Primes, q.val ∉ bad ∧
      FinitePlaceSplitsCompletely (K := ℚ) (L := K)
        ((Rat.HeightOneSpectrum.primesEquiv (R := 𝓞 ℚ)).symm q)

Module documentation

Completely split primes of number fields

Declarations

rationalPrimePlace_asIdeal

under_rational_prime_eq_span

finitePlaceBelow_eq_rationalPrimePlace

finitePlaceSplitsCompletely_of_unramified_degree_one

exists_completelySplitPrime_not_mem