ClassFieldTheory.realLowerRamificationGroup_canonical_antitone
The public real lower groups of a finite Abelian local extension form a decreasing filtration of its canonical decomposition group.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace ClassFieldTheory
universe u vLean source · statement
theorem realLowerRamificationGroup_canonical_antitone
(K : Type u) (L : Type v) [Field K] [Field L] [Algebra K L]
[FiniteDimensional K L] [IsAbelianGalois K L]
[ValuativeRel K] [TopologicalSpace K]
[IsNonarchimedeanLocalField K]
[ValuativeRel L] [TopologicalSpace L]
[IsNonarchimedeanLocalField L]
[Valuation.HasExtension (ValuativeRel.valuation K) (ValuativeRel.valuation L)] :
Antitone (ClassFieldTheory.realLowerRamificationGroup K
(ValuativeRel.valuation L).valuationSubring)