ClassFieldTheory.IsAbelianConductor.mem_finiteSupport_iff_exists_ramified
A finite prime occurs in the conductor precisely when some prime above it is ramified.
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 IsAbelianConductor.mem_finiteSupport_iff_exists_ramified
{K : Type} [Field K] [NumberField K]
{L : Type} [Field L] [NumberField L]
[Algebra K L] [IsAbelianGalois K L]
{c : RayClassModulus K}
(hc : IsAbelianConductor K L c)
(v : HeightOneSpectrum (𝓞 K)) :
v ∈ c.finitePart.support ↔
∃ W : HeightOneSpectrum (𝓞 L),
W.asIdeal.LiesOver v.asIdeal ∧
¬ Algebra.IsUnramifiedAt (𝓞 K) W.asIdeal