ClassFormation.ValuationData.normTopology_open_iff_closed_finiteIndex
The norm-subgroup basis characterization: in the norm topology, the open subgroups are exactly the closed subgroups of finite index. Finiteness of every defining norm quotient is obtained from the abstract reciprocity theorem, not assumed.
Source context 6 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
namespace ClassFormation
open ClassFormation CyclicCohomology KummerTheory
-- Mathlib's `Rep ℤ G` currently fixes the acting group to universe zero.
variable {G : IntegralRepGroupType} [Group G] [TopologicalSpace G]
namespace ValuationData
variable {D : DegreeData G} {A : Rep ℤ G}Lean source · statement
theorem normTopology_open_iff_closed_finiteIndex
(v : ValuationData D A) (hcf : SatisfiesClassFieldAxiom A)
[IsTopologicalGroup G] [CompactSpace G] [T2Space G]
[TotallyDisconnectedSpace G]
(K : ClosedSubgroup G)
[hKabsolute : Finite ((baseField G).toSubgroup ⧸
extensionSubgroup (baseField G) K (le_baseField K))]
(H : AddSubgroup (ambientFixedAddSubgroup A K)) :
IsNormOpen A K H ↔
IsNormClosed A K H ∧
Finite (ambientFixedAddSubgroup A K ⧸ H)