ClassFieldTheory.finitePrime_inertiaDegreeInRayClassSubgroupField_eq_orderOf
The residue degree above a prime away from the modulus is the order of its ray class in the quotient by the defining subgroup.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
noncomputable section
namespace ClassFieldTheory
open NumberField IsDedekindDomain
universe uLean source · statement
theorem finitePrime_inertiaDegreeInRayClassSubgroupField_eq_orderOf
(K : Type u) [Field K] [NumberField K]
(m : RayClassModulus K) (H : Subgroup (RayClassGroup m))
(R : RayClassSubgroupRealization K m H)
(v : HeightOneSpectrum (𝓞 K))
(hv : v ∉ m.finitePart.support)
(w : HeightOneSpectrum (𝓞 R.extension))
(hw : w.asIdeal.LiesOver v.asIdeal) :
w.asIdeal.inertiaDeg (𝓞 K) =
orderOf (QuotientGroup.mk' H (rayClassOfFinitePrime m v hv))