The local Weil group

Let K be a nonarchimedean local field, G_K = Field.absoluteGaloisGroup K its absolute Galois group, I_K = TauCeti.inertiaSubgroup K the inertia subgroup and K^{ur} the maximal unramified extension, so that 1 → I_K → G_K → Gal(K^{ur}/K) → 1 is exact and Gal(K^{ur}/K) ≃ ℤ̂ carries arithmetic Frobenius to the canonical generator. The local Weil group

TauCeti.ClassFieldTheory.localWeilGroup K ≤ G_K

consists of the elements acting on K^{ur} as an integral power of arithmetic Frobenius: it is the preimage of ℤ ⊆ ℤ̂. It contains inertia, it is normal, and it is generated by inertia together with any single arithmetic Frobenius lift. Since ℤ is dense in ℤ̂ but not all of it, W_K is a dense proper subgroup of G_K.

The degree weilDegree K : WeilGroup K →* Multiplicative ℤ records which power of Frobenius an element induces on K^{ur}; it is normalized arithmetically, so that the arithmetic Frobenius lifts are exactly the elements of degree 1. It is surjective with kernel inertia, giving the exact sequence 1 → I_K → W_K → ℤ → 1, and its image in ℤ̂ is the unramified coordinate.

The Weil group is wanted as a locally compact group in which I_K, with its profinite topology, is open. That is not the subspace topology of G_K: inertia is not open in G_K (TauCeti.not_isOpen_inertiaSubgroup), because its image {1} in ℤ̂ is not open. The degree map is therefore stated on the type synonym WeilGroup K of localWeilGroup K, which does not inherit the subspace topology of the subtype; weilGroupEquivLocalWeilGroup K identifies the two as groups.

Main definitions

• TauCeti.ClassFieldTheory.localWeilGroup K: the local Weil group, as a subgroup of G_K.
• TauCeti.ClassFieldTheory.WeilGroup K: a type synonym for localWeilGroup K, with its inclusion weilToAbsolute K : WeilGroup K →* G_K and the group isomorphism weilGroupEquivLocalWeilGroup K : WeilGroup K ≃* localWeilGroup K.
• TauCeti.ClassFieldTheory.weilDegree K : WeilGroup K →* Multiplicative ℤ: the degree.
• TauCeti.ClassFieldTheory.inertiaToWeil K : I_K →* W_K: the inclusion of inertia.

Main results

• TauCeti.ClassFieldTheory.mem_localWeilGroup_iff, TauCeti.ClassFieldTheory.mem_localWeilGroup_iff_unramifiedCoordinate: σ ∈ W_K exactly when σ acts on K^{ur} as an integral power of Frobenius, exactly when its unramified coordinate lies in ℤ ⊆ ℤ̂.
• TauCeti.ClassFieldTheory.inertiaSubgroup_le_localWeilGroup, TauCeti.ClassFieldTheory.localWeilGroup_normal: I_K ≤ W_K, and W_K is normal in G_K.
• TauCeti.IsArithFrobeniusLift.zpowers_sup_inertiaSubgroup: W_K = ⟨σ⟩ I_K for every arithmetic Frobenius lift σ.
• TauCeti.ClassFieldTheory.dense_localWeilGroup, TauCeti.ClassFieldTheory.localWeilGroup_ne_top: W_K is dense and proper in G_K.
• TauCeti.ClassFieldTheory.surjective_weilDegree, TauCeti.ClassFieldTheory.ker_weilDegree: the exact sequence 1 → I_K → W_K → ℤ → 1.
• TauCeti.ClassFieldTheory.range_inertiaToWeil: the image of inertia in W_K is the kernel of the degree.
• TauCeti.ClassFieldTheory.unramifiedCoordinate_weilDegree, TauCeti.ClassFieldTheory.weilDegree_eq_ofAdd_one_iff: the degree is the unramified coordinate, and the elements of degree 1 are the arithmetic Frobenius lifts.

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 carrier

noncomputable def TauCeti.ClassFieldTheory.localWeilGroup (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : Subgroup (Field.absoluteGaloisGroup K)

The local Weil group W_K ≤ G_K of a nonarchimedean local field K: the elements of the absolute Galois group acting on the maximal unramified extension K^{ur} as an integral power of arithmetic Frobenius. Through Gal(K^{ur}/K) ≃ ℤ̂ it is the preimage of ℤ ⊆ ℤ̂ (mem_localWeilGroup_iff_unramifiedCoordinate).

theorem TauCeti.ClassFieldTheory.localWeilGroup_def (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : localWeilGroup K = Subgroup.comap (restrictMaximalUnramifiedHom K) (Subgroup.zpowers (maximalUnramifiedFrobenius K (AlgebraicClosure K)))

The local Weil group is the preimage of the powers of arithmetic Frobenius under restriction to the maximal unramified extension.

theorem TauCeti.ClassFieldTheory.mem_localWeilGroup_iff {K : Type u} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {σ : Field.absoluteGaloisGroup K} : σ ∈ localWeilGroup K ↔ ∃ (n : ℤ), (restrictMaximalUnramifiedHom K) σ = maximalUnramifiedFrobenius K (AlgebraicClosure K) ^ n

σ lies in the local Weil group exactly when it acts on the maximal unramified extension as an integral power of arithmetic Frobenius.

theorem TauCeti.ClassFieldTheory.mem_localWeilGroup_iff_unramifiedCoordinate {K : Type u} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {σ : Field.absoluteGaloisGroup K} : σ ∈ localWeilGroup K ↔ (unramifiedCoordinate K) ↑σ ∈ zHat.ofInt.range

The Weil group is the preimage of ℤ ⊆ ℤ̂: σ lies in the local Weil group exactly when the unramified coordinate of its class in G_K^{ab} is an integer.

theorem TauCeti.ClassFieldTheory.inertiaSubgroup_le_localWeilGroup (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : inertiaSubgroup K ≤ localWeilGroup K

Inertia lies in the Weil group, as the elements acting trivially on K^{ur}.

theorem TauCeti.IsArithFrobeniusLift.mem_localWeilGroup {K : Type u} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {σ : Field.absoluteGaloisGroup K} (hσ : IsArithFrobeniusLift K σ) : σ ∈ ClassFieldTheory.localWeilGroup K

An arithmetic Frobenius lift lies in the Weil group.

theorem TauCeti.IsArithFrobeniusLift.zpowers_sup_inertiaSubgroup {K : Type u} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {σ : Field.absoluteGaloisGroup K} (hσ : IsArithFrobeniusLift K σ) : Subgroup.zpowers σ ⊔ inertiaSubgroup K = ClassFieldTheory.localWeilGroup K

The Weil group is generated by a Frobenius lift and inertia: for every arithmetic Frobenius lift σ, the subgroup generated by σ and I_K is W_K.

instance TauCeti.ClassFieldTheory.localWeilGroup_normal (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : (localWeilGroup K).Normal

The Weil group is normal in G_K, being the preimage of a subgroup of the abelian group Gal(K^{ur}/K).

theorem TauCeti.ClassFieldTheory.dense_localWeilGroup (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : Dense ↑(localWeilGroup K)

The Weil group is dense in G_K: its closure contains every Frobenius lift and inertia, and these generate G_K topologically.

theorem TauCeti.ClassFieldTheory.localWeilGroup_ne_top (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : localWeilGroup K ≠ ⊤

The Weil group is a proper subgroup of G_K, since ℤ ≠ ℤ̂.

The Weil group as a type, and its degree

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

The local Weil group as a type: a type synonym for localWeilGroup K. It carries the group structure of the subgroup, but deliberately not the subspace topology of G_K, in which inertia is not open (not_isOpen_inertiaSubgroup).

@[instance_reducible]

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

noncomputable def TauCeti.ClassFieldTheory.weilToAbsolute (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : WeilGroup K →* Field.absoluteGaloisGroup K

The inclusion W_K → G_K of the Weil group into the absolute Galois group.

noncomputable def TauCeti.ClassFieldTheory.weilGroupEquivLocalWeilGroup (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : WeilGroup K ≃* ↥(localWeilGroup K)

The Weil group as a type is the local Weil group: the group isomorphism WeilGroup K ≃* localWeilGroup K, under which the inclusion weilToAbsolute K is the subgroup inclusion (coe_weilGroupEquivLocalWeilGroup).

@[simp]

theorem TauCeti.ClassFieldTheory.coe_weilGroupEquivLocalWeilGroup (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (w : WeilGroup K) : ↑((weilGroupEquivLocalWeilGroup K) w) = (weilToAbsolute K) w

The isomorphism WeilGroup K ≃* localWeilGroup K is compatible with the inclusions into G_K.

@[simp]

theorem TauCeti.ClassFieldTheory.weilToAbsolute_weilGroupEquivLocalWeilGroup_symm (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (σ : ↥(localWeilGroup K)) : (weilToAbsolute K) ((weilGroupEquivLocalWeilGroup K).symm σ) = ↑σ

The element of the Weil group corresponding to σ ∈ localWeilGroup K maps to σ in G_K.

theorem TauCeti.ClassFieldTheory.injective_weilToAbsolute (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : Function.Injective ⇑(weilToAbsolute K)

The inclusion of the Weil group into G_K is injective.

@[simp]

theorem TauCeti.ClassFieldTheory.range_weilToAbsolute (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : (weilToAbsolute K).range = localWeilGroup K

The image of the inclusion W_K → G_K is the local Weil group.

@[simp]

theorem TauCeti.ClassFieldTheory.weilToAbsolute_mem_localWeilGroup {K : Type u} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (w : WeilGroup K) : (weilToAbsolute K) w ∈ localWeilGroup K

An element of the Weil group lies in the local Weil group of G_K.

noncomputable def TauCeti.ClassFieldTheory.weilDegree (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : WeilGroup K →* Multiplicative ℤ

The degree of the Weil group: w ∈ W_K has degree n when it acts on the maximal unramified extension as the n-th power of arithmetic Frobenius (restrictMaximalUnramifiedHom_weilToAbsolute).

theorem TauCeti.ClassFieldTheory.restrictMaximalUnramifiedHom_weilToAbsolute {K : Type u} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (w : WeilGroup K) : (restrictMaximalUnramifiedHom K) ((weilToAbsolute K) w) = maximalUnramifiedFrobenius K (AlgebraicClosure K) ^ Multiplicative.toAdd ((weilDegree K) w)

The characterization of the degree: an element of degree n acts on the maximal unramified extension as the n-th power of arithmetic Frobenius.

theorem TauCeti.ClassFieldTheory.weilDegree_eq_iff {K : Type u} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {w : WeilGroup K} {n : Multiplicative ℤ} : (weilDegree K) w = n ↔ (restrictMaximalUnramifiedHom K) ((weilToAbsolute K) w) = maximalUnramifiedFrobenius K (AlgebraicClosure K) ^ Multiplicative.toAdd n

The degree of w is n exactly when w acts on the maximal unramified extension as the n-th power of arithmetic Frobenius.

theorem TauCeti.ClassFieldTheory.weilDegree_eq_ofAdd_one_iff {K : Type u} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] {w : WeilGroup K} : (weilDegree K) w = Multiplicative.ofAdd 1 ↔ IsArithFrobeniusLift K ((weilToAbsolute K) w)

Arithmetic normalization of the degree: the elements of degree 1 are exactly the arithmetic Frobenius lifts.

theorem TauCeti.ClassFieldTheory.unramifiedCoordinate_weilDegree {K : Type u} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (w : WeilGroup K) : (unramifiedCoordinate K) ↑((weilToAbsolute K) w) = zHat.ofInt ((weilDegree K) w)

The degree is the unramified coordinate: the unramified coordinate of the class of w in G_K^{ab} is the image in ℤ̂ of the degree of w.

theorem TauCeti.ClassFieldTheory.surjective_weilDegree (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : Function.Surjective ⇑(weilDegree K)

Exactness on the right: every integer is the degree of an element of the Weil group, for instance of a power of an arithmetic Frobenius lift.

theorem TauCeti.ClassFieldTheory.ker_weilDegree (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : (weilDegree K).ker = Subgroup.comap (weilToAbsolute K) (inertiaSubgroup K)

Exactness in the middle: the kernel of the degree is inertia. With surjective_weilDegree and injective_weilToAbsolute, this is the exact sequence 1 → I_K → W_K → ℤ → 1.

Inertia in the Weil group

noncomputable def TauCeti.ClassFieldTheory.inertiaToWeil (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : ↥(inertiaSubgroup K) →* WeilGroup K

The inclusion of inertia into the Weil group.

@[simp]

theorem TauCeti.ClassFieldTheory.weilToAbsolute_inertiaToWeil {K : Type u} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (σ : ↥(inertiaSubgroup K)) : (weilToAbsolute K) ((inertiaToWeil K) σ) = ↑σ

An element of inertia maps to itself under I_K → W_K → G_K.

@[simp]

theorem TauCeti.ClassFieldTheory.weilDegree_inertiaToWeil {K : Type u} [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] (σ : ↥(inertiaSubgroup K)) : (weilDegree K) ((inertiaToWeil K) σ) = 1

An element of inertia has trivial degree in the Weil group.

theorem TauCeti.ClassFieldTheory.range_inertiaToWeil (K : Type u) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] : (inertiaToWeil K).range = Subgroup.comap (weilToAbsolute K) (inertiaSubgroup K)

The image of inertia in the Weil group is the preimage of I_K under W_K → G_K, that is, the kernel of the degree (ker_weilDegree).