The Weil topology on the local Weil group

Let K be a nonarchimedean local field, G_K its absolute Galois group, I_K ≤ G_K the inertia subgroup and W_K = TauCeti.ClassFieldTheory.WeilGroup K the local Weil group, with its degree weilDegree K : W_K →* ℤ and kernel I_K. The Weil topology on W_K is the unique group topology in which I_K, with the profinite topology it carries as a closed subgroup of G_K, is an open subgroup. It is not the topology induced from G_K, in which inertia is not open (TauCeti.not_isOpen_inertiaSubgroup).

We define it without choosing a Frobenius lift, as the topology induced by the injective homomorphism

W_K → G_K × ℤ, w ↦ (w, deg w),

with ℤ discrete (isEmbedding_weilToAbsolute_prod_weilDegree). A neighbourhood basis of 1 is then {w | deg w = 0, w ∈ U} = I_K ∩ U for U open in G_K, so inertia is open with its own profinite topology. Weil's description of the same topology goes through a choice of arithmetic Frobenius lift, writing W_K as I_K ⋊ ℤ with the product of the profinite and the discrete topologies; the description used here needs no choice.

Main definitions

• TauCeti.ClassFieldTheory.instTopologicalSpaceWeilGroup: the Weil topology on WeilGroup K.

Main results

• TauCeti.ClassFieldTheory.isOpenEmbedding_inertiaToWeil: I_K, with its profinite topology, is an open topological subgroup of W_K via the inclusion inertiaToWeil K : I_K →* W_K.
• TauCeti.ClassFieldTheory.weilTopology_unique: the Weil topology is the only group topology on W_K with this property.
• TauCeti.ClassFieldTheory.continuous_weilToAbsolute, TauCeti.ClassFieldTheory.denseRange_weilToAbsolute: the inclusion W_K → G_K is a continuous injection with dense image.
• TauCeti.ClassFieldTheory.continuous_weilDegree: the degree W_K → ℤ is continuous, so the exact sequence 1 → I_K → W_K → ℤ → 1 is one of topological groups.
• W_K is a locally compact, totally disconnected Hausdorff group (TauCeti.ClassFieldTheory.instLocallyCompactSpaceWeilGroup, TauCeti.ClassFieldTheory.instTotallyDisconnectedSpaceWeilGroup), and it is not compact (TauCeti.ClassFieldTheory.not_compactSpace_weilGroup).

References

• A. Weil, Sur la théorie du corps de classes, J. Math. Soc. Japan 3 (1951).
• J. Tate, Number theoretic background, in Automorphic forms, representations and L-functions, Proc. Sympos. Pure Math. 33, Part 2 (1979), §1.4.

The topology

@[instance_reducible]

noncomputable instance TauCeti.ClassFieldTheory.instTopologicalSpaceWeilGroup (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : TopologicalSpace (WeilGroup K)

The Weil topology on the local Weil group: the topology induced by w ↦ (w, deg w) : W_K → G_K × ℤ, with ℤ discrete. It is the unique group topology in which inertia, with its profinite topology, is an open subgroup (isOpenEmbedding_inertiaToWeil, weilTopology_unique), and it is finer than the topology induced from G_K (continuous_weilToAbsolute).

theorem TauCeti.ClassFieldTheory.isEmbedding_weilToAbsolute_prod_weilDegree (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : Topology.IsEmbedding ⇑((weilToAbsolute K).prod (weilDegree K))

The characterization of the Weil topology: w ↦ (w, deg w) is a topological embedding of W_K into G_K × ℤ, with ℤ discrete.

instance TauCeti.ClassFieldTheory.instIsTopologicalGroupWeilGroup (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : IsTopologicalGroup (WeilGroup K)

The Weil topology makes W_K a topological group.

theorem TauCeti.ClassFieldTheory.continuous_weilToAbsolute (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : Continuous ⇑(weilToAbsolute K)

The inclusion W_K → G_K is continuous: the Weil topology is finer than the topology induced from G_K.

theorem TauCeti.ClassFieldTheory.continuous_weilDegree (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : Continuous ⇑(weilDegree K)

The degree W_K → ℤ is continuous for the discrete topology on ℤ.

theorem TauCeti.ClassFieldTheory.denseRange_weilToAbsolute (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : DenseRange ⇑(weilToAbsolute K)

The inclusion W_K → G_K has dense image, since W_K is dense in G_K.

instance TauCeti.ClassFieldTheory.instT2SpaceWeilGroup (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : T2Space (WeilGroup K)

The Weil topology is Hausdorff.

Inertia is open, with its own topology

theorem TauCeti.ClassFieldTheory.isOpen_inertia_weil (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : IsOpen ↑(Subgroup.comap (weilToAbsolute K) (inertiaSubgroup K))

Inertia is open in the Weil group, being the kernel of the continuous degree map to the discrete group ℤ.

theorem TauCeti.ClassFieldTheory.isOpenEmbedding_inertiaToWeil (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : Topology.IsOpenEmbedding ⇑(inertiaToWeil K)

The characterization of the Weil topology, first half. The inclusion of I_K, with its profinite topology as a closed subgroup of G_K, into W_K is an open topological embedding.

theorem TauCeti.ClassFieldTheory.weilTopology_unique (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (t : TopologicalSpace (WeilGroup K)) (ht : IsTopologicalGroup (WeilGroup K)) (hopen : Topology.IsOpenEmbedding ⇑(inertiaToWeil K)) : t = instTopologicalSpaceWeilGroup K

The characterization of the Weil topology, second half: uniqueness. Any group topology on W_K in which I_K, with its profinite topology, includes as an open embedding is the Weil topology.

Local compactness and noncompactness

instance TauCeti.ClassFieldTheory.instLocallyCompactSpaceWeilGroup (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : LocallyCompactSpace (WeilGroup K)

The Weil group is locally compact: inertia is a compact open neighbourhood of 1.

instance TauCeti.ClassFieldTheory.instTotallyDisconnectedSpaceWeilGroup (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : TotallyDisconnectedSpace (WeilGroup K)

The Weil group is totally disconnected, as it embeds into the totally disconnected group G_K × ℤ.

theorem TauCeti.ClassFieldTheory.not_compactSpace_weilGroup (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : ¬CompactSpace (WeilGroup K)

The Weil group is not compact, although G_K is compact and W_K is dense in it: the degree is a continuous surjection onto the infinite discrete group ℤ.