ClassFieldTheory.IsAbelianConductor.finiteExponent_le_one_iff_residueChar_not_dvd_ramificationIdx
At any prime above v, the finite conductor exponent is at most one exactly when the residue characteristic is prime to the ramification index. The criterion is independent of the chosen prime above v.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField ValuativeRel
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheoryLean source · statement
theorem IsAbelianConductor.finiteExponent_le_one_iff_residueChar_not_dvd_ramificationIdx
{K L : Type}
[Field K] [NumberField K]
[Field L] [NumberField L] [Algebra K L]
[FiniteDimensional K L] [IsAbelianGalois K L]
{c : RayClassModulus K}
(hc : IsAbelianConductor K L c)
(v : HeightOneSpectrum (𝓞 K))
(W : HeightOneSpectrum (𝓞 L))
(hW : W.asIdeal.LiesOver v.asIdeal) :
c.finitePart v ≤ 1 ↔
¬ ringChar (𝓞 K ⧸ v.asIdeal) ∣
W.asIdeal.ramificationIdx (𝓞 K)