ClassFieldTheory.rayLocalHigherUnitGroup_antitone
Deeper local congruence conditions give smaller higher-unit groups.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open scoped NumberField
noncomputable section
namespace ClassFieldTheory
universe u
open NumberField IsDedekindDomainLean source · statement
theorem rayLocalHigherUnitGroup_antitone
{K : Type u} [Field K] [NumberField K]
(v : HeightOneSpectrum (𝓞 K))
{m n : ℕ} (hmn : m ≤ n) :
rayLocalHigherUnitGroup v n ≤ rayLocalHigherUnitGroup v m