ClassFieldTheory.finitePrime_splitsCompletelyInBigHilbertClassField_iff_positivePrincipal
Equivalently, a prime splits completely in the big Hilbert class field exactly when it has a totally positive generator.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheoryLean source · statement
theorem finitePrime_splitsCompletelyInBigHilbertClassField_iff_positivePrincipal
(K : Type) [Field K] [NumberField K]
(E : FiniteAbelianExtension K) (hE : IsBigHilbertClassField E)
(v : HeightOneSpectrum (𝓞 K)) :
FinitePrimeSplitsCompletely K E v ↔
∃ x : Kˣ,
(∀ w : RayClassRealPlace K,
0 < w.1.embedding_of_isReal w.2 (x : K)) ∧
toPrincipalIdeal (𝓞 K) K x = finitePrimeFractionalIdeal v