NYLL
Module

CompletelySplitPrimesModFour.lean

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

Module documentation

Completely split primes congruent to one modulo four

A finite Galois number field admits completely split rational primes congruent to one modulo four and outside any specified finite set. The construction passes through an extension containing a square root of minus one.

Imports9
Imported by2

Declarations

theorem

modFour_eq_one_of_degreeOnePrime_sq_neg_one

L33 ↗
AlgebraicNumberTheory.PrimeSelection.modFour_eq_one_of_degreeOnePrime_sq_neg_one
Documentation

At an odd degree-one prime in a field containing i, reduction of i makes -1 a square in the prime field, forcing q ≡ 1 mod 4.

Source context 3 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
namespace AlgebraicNumberTheory.PrimeSelection
Lean source · statement
theorem modFour_eq_one_of_degreeOnePrime_sq_neg_one
    (K : Type*) [Field K] [NumberField K]
    (q : ℕ) [Fact q.Prime] (hqTwo : q ≠ 2)
    (W : HeightOneSpectrum (𝓞 K))
    (hOver : W.asIdeal.LiesOver (Ideal.span ({(q : ℤ)} : Set ℤ)))
    (hf : W.asIdeal.inertiaDeg ℤ = 1)
    (j : 𝓞 K) (hj : j ^ 2 = -1) : q % 4 = 1
theorem

exists_completelySplitPrime_modFour_one_not_mem

L64 ↗
AlgebraicNumberTheory.PrimeSelection.exists_completelySplitPrime_modFour_one_not_mem
Documentation

Prime selection with complete splitting, the congruence q ≡ 1 mod 4, and avoidance of an arbitrary finite set. The proof applies the elementary polynomial prime-divisor argument to K(i), then contracts its degree-one unramified prime to K.

Source context 3 commands

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

open scoped NumberField
open NumberField IsDedekindDomain
namespace AlgebraicNumberTheory.PrimeSelection
Lean source · statement
theorem exists_completelySplitPrime_modFour_one_not_mem
    (K : Type) [Field K] [NumberField K] [IsGalois ℚ K] (bad : Finset ℕ) :
    ∃ q : Nat.Primes, q.val ∉ bad ∧ q.val % 4 = 1 ∧
      FinitePlaceSplitsCompletely (K := ℚ) (L := K)
        ((Rat.HeightOneSpectrum.primesEquiv (R := 𝓞 ℚ)).symm q)

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