The finite place support is the inverse image of the six primes under the canonical equivalence between finite places of ℚ and rational primes.
The rational primes allowed to ramify in the initial tower.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open IsDedekindDomain
namespace ClassFieldTower.Sawindef sawinRationalPrimes : Finset ℕThe corresponding finite places of ℚ.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open IsDedekindDomain
namespace ClassFieldTower.Sawindef sawinRationalPrimeSupport : Set (HeightOneSpectrum (𝓞 ℚ))Membership of a rational prime's place is membership in the six-prime set.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open IsDedekindDomain
namespace ClassFieldTower.Sawintheorem rationalPrime_mem_sawinRationalPrimeSupport_iff (q : Nat.Primes) :
(Rat.HeightOneSpectrum.primesEquiv (R := 𝓞 ℚ)).symm q ∈
sawinRationalPrimeSupport ↔ (q : ℕ) ∈ sawinRationalPrimesTwo is excluded from the allowed finite ramification support.
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open IsDedekindDomain
namespace ClassFieldTower.Sawintheorem two_not_mem_sawinRationalPrimeSupport :
(Rat.HeightOneSpectrum.primesEquiv (R := 𝓞 ℚ)).symm
(⟨2, Nat.prime_two⟩ : Nat.Primes) ∉ sawinRationalPrimeSupport