ClassFieldTheory.IsAbelianConductor.finiteExponent_isLeast_tensorNorm
The conductor exponent is the least index whose higher-unit group lies in the finite-place tensor norm image. In particular this set is nonempty.
Source context 4 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField TensorProduct
open NumberField IsDedekindDomain
noncomputable section
namespace ClassFieldTheoryLean source · full declaration
theorem IsAbelianConductor.finiteExponent_isLeast_tensorNorm
{K : Type} [Field K] [NumberField K]
{L : Type} [Field L] [NumberField L] [Algebra K L]
[FiniteDimensional K L] [IsAbelianGalois K L]
{c : RayClassModulus K}
(hc : IsAbelianConductor K L c)
(v : HeightOneSpectrum (𝓞 K)) :
IsLeast (α := ℕ) (fun n =>
rayLocalHigherUnitGroup v n ≤
(Units.map (Algebra.norm (v.adicCompletion K)) :
(v.adicCompletion K ⊗[K] L)ˣ →*
(v.adicCompletion K)ˣ).range) (c.finitePart v) := by
constructor
· exact (hc.finiteExponent_le_iff_higherUnit_le_tensorNorm v
(c.finitePart v)).mp le_rfl
· intro n hn
exact (hc.finiteExponent_le_iff_higherUnit_le_tensorNorm v n).mpr hn