NYLL
Module

DegreeOnePrimes.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.NumberField.DegreeOnePrimes
2 declarations indexed from sourceView source ↗

Module documentation

Degree-one primes of number fields

Good prime divisors of primitive polynomial values give prime ideals of residue degree one. Every number field admits an unramified degree-one prime outside any specified finite set of rational primes.

Imports6
Imported by3

Declarations

theorem

exists_degreeOnePrime_of_dvd_minpoly_eval

L29 ↗
AlgebraicNumberTheory.PrimeSelection.exists_degreeOnePrime_of_dvd_minpoly_eval
Documentation

A good prime divisor of a primitive polynomial value gives an actual prime ideal whose residue degree is one.

Source context 3 commands

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

open scoped NumberField
open NumberField IsDedekindDomain Polynomial
namespace AlgebraicNumberTheory.PrimeSelection
Lean source · statement
theorem exists_degreeOnePrime_of_dvd_minpoly_eval
    (K : Type*) [Field K] [NumberField K]
    (θ : 𝓞 K) (q : ℕ) [Fact q.Prime]
    (hGood : ¬ q ∣ RingOfIntegers.exponent θ)
    (n : ℤ) (hn : (q : ℤ) ∣ (minpoly ℤ θ).eval n) :
    ∃ P : Ideal (𝓞 K), P.IsPrime ∧
      P.LiesOver (Ideal.span ({(q : ℤ)} : Set ℤ)) ∧
      P.inertiaDeg ℤ = 1
theorem

exists_unramified_degreeOnePrime_not_mem

L61 ↗
AlgebraicNumberTheory.PrimeSelection.exists_unramified_degreeOnePrime_not_mem
Documentation

Every number field has an unramified prime of residue degree one above a new rational prime, outside an arbitrary finite set.

Source context 3 commands

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

open scoped NumberField
open NumberField IsDedekindDomain Polynomial
namespace AlgebraicNumberTheory.PrimeSelection
Lean source · statement
theorem exists_unramified_degreeOnePrime_not_mem
    (K : Type*) [Field K] [NumberField K] (bad : Finset ℕ) :
    ∃ q : ℕ, q.Prime ∧ q ∉ bad ∧
      ∃ W : HeightOneSpectrum (𝓞 K),
        W.asIdeal.LiesOver (Ideal.span ({(q : ℤ)} : Set ℤ)) ∧
        W.asIdeal.inertiaDeg ℤ = 1 ∧ Algebra.IsUnramifiedAt ℤ W.asIdeal

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