Documentation

TauCeti.NumberTheory.LocalField.Generation.AbsoluteGaloisGroup

Topological finite generation and the generator rank of a local absolute Galois group #

Let K be a finite extension of ℚ_p, N = [K : ℚ_p], and P_K the wild inertia subgroup of the absolute Galois group G_K. Every finite quotient of G_K through which ⁅P_K, P_K⁆ dies is generated by an (N + 2)-tuple (TauCeti.exists_generating_tuple_quotient). Since G_K is compact, one (N + 2)-tuple of G_K generates all of these quotients at once, and so it topologically generates G_K modulo ⁅P_K, P_K⁆. As P_K is pro-p, the Frattini argument along P_K removes the commutator, so G_K is topologically finitely generated.

This is the passage from the finite quotients to the profinite group in the proof of NSW (7.4.1). Finite generation is recorded on its own, so that the natural-valued generator rank of G_K is only ever read once its hypothesis is available.

The same tuple bounds the generator rank d(G_K) by N + 2. Together with the lower bound TauCeti.le_topologicalGeneratorRankNat_absoluteGaloisGroup, this computes it exactly:

d(G_K) = N + 2.

The statement of finite generation mentions neither p nor the ℚ_p-algebra structure of K, but it is false without them: the absolute Galois group of 𝔽_q((t)) is not topologically finitely generated. So p is included explicitly, together with the instances depending on it.

Main results #

References #

source
theorem TauCeti.exists_tuple_generating_mod_wildInertiaCommutator (p : ℕ) [Fact (Nat.Prime p)] (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Algebra ℚ_[p] K] [Module.Finite ℚ_[p] K] [ValuativeExtension ℚ_[p] K] :
∃ (x : Fin (Module.finrank ℚ_[p] K + 2) → Field.absoluteGaloisGroup K), (Subgroup.closure (Set.range x) ⊔ ⁅wildInertiaSubgroup K, wildInertiaSubgroup K⁆).topologicalClosure = ⊤

Passage to the profinite group (NSW (7.4.1)). For a finite extension K of ℚ_p, some ([K : ℚ_p] + 2)-tuple of G_K topologically generates G_K together with the commutator subgroup ⁅P_K, P_K⁆ of wild inertia: by compactness, a single tuple generates every finite quotient of G_K through which ⁅P_K, P_K⁆ dies.

source
theorem TauCeti.isTopologicallyFinitelyGenerated_fieldAbsoluteGaloisGroup (p : ℕ) [Fact (Nat.Prime p)] (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Algebra ℚ_[p] K] [Module.Finite ℚ_[p] K] [ValuativeExtension ℚ_[p] K] :
IsTopologicallyFinitelyGenerated (Field.absoluteGaloisGroup K)

The absolute Galois group of a finite extension of ℚ_p is topologically finitely generated, by a ([K : ℚ_p] + 2)-tuple: the tuple of TauCeti.exists_tuple_generating_mod_wildInertiaCommutator already generates G_K by the Frattini argument along wild inertia.

source
theorem TauCeti.isTopologicallyFinitelyGenerated_absoluteGaloisGroup (p : ℕ) [Fact (Nat.Prime p)] (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Algebra ℚ_[p] K] [Module.Finite ℚ_[p] K] [ValuativeExtension ℚ_[p] K] :
IsTopologicallyFinitelyGenerated (AbsoluteGaloisGroup K)

The automorphism group of the separable closure of a finite compatible extension of ℚ_p is topologically finitely generated.

source
theorem TauCeti.topologicalGeneratorRankNat_absoluteGaloisGroup_le (p : ℕ) [Fact (Nat.Prime p)] (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Algebra ℚ_[p] K] [Module.Finite ℚ_[p] K] [ValuativeExtension ℚ_[p] K] (hG : IsTopologicallyFinitelyGenerated (Field.absoluteGaloisGroup K)) :
topologicalGeneratorRankNat (Field.absoluteGaloisGroup K) hG ≤ Module.finrank ℚ_[p] K + 2

The upper bound for the generator rank of a local absolute Galois group (NSW (7.4.1)). For a finite extension K of ℚ_p, the absolute Galois group G_K is topologically generated by [K : ℚ_p] + 2 elements: the tuple of TauCeti.exists_tuple_generating_mod_wildInertiaCommutator generates G_K by the Frattini reduction along wild inertia.

source
theorem TauCeti.topologicalGeneratorRankNat_absoluteGaloisGroup (p : ℕ) [Fact (Nat.Prime p)] (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Algebra ℚ_[p] K] [Module.Finite ℚ_[p] K] [ValuativeExtension ℚ_[p] K] (hG : IsTopologicallyFinitelyGenerated (Field.absoluteGaloisGroup K)) :
topologicalGeneratorRankNat (Field.absoluteGaloisGroup K) hG = Module.finrank ℚ_[p] K + 2

The generator rank of a local absolute Galois group (NSW (7.4.1)). For a finite extension K of ℚ_p, the absolute Galois group G_K needs exactly [K : ℚ_p] + 2 topological generators. A witness of topological finite generation is TauCeti.isTopologicallyFinitelyGenerated_fieldAbsoluteGaloisGroup.

source
theorem TauCeti.exists_finset_card_eq_finrank_add_two_absoluteGaloisGroup (p : ℕ) [Fact (Nat.Prime p)] (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Algebra ℚ_[p] K] [Module.Finite ℚ_[p] K] [ValuativeExtension ℚ_[p] K] :
∃ (s : Finset (Field.absoluteGaloisGroup K)), s.card = Module.finrank ℚ_[p] K + 2 ∧ (Subgroup.closure ↑s).topologicalClosure = ⊤

A minimal topological generating set of a local absolute Galois group. For a finite extension K of ℚ_p, some finite subset of G_K with exactly [K : ℚ_p] + 2 elements generates a dense subgroup; by TauCeti.finrank_add_two_le_card_of_topologicalClosure_closure_eq_top_absoluteGaloisGroup no smaller one does.

source
theorem TauCeti.rank_absoluteGaloisGroup (p : ℕ) [Fact (Nat.Prime p)] (K : Type) [Field K] [ValuativeRel K] [TopologicalSpace K] [IsNonarchimedeanLocalField K] [Algebra ℚ_[p] K] [Module.Finite ℚ_[p] K] [ValuativeExtension ℚ_[p] K] :
IsLeast {m : ℕ | ∃ (s : Finset (Field.absoluteGaloisGroup K)), s.card = m ∧ (Subgroup.closure ↑s).topologicalClosure = ⊤} (Module.finrank ℚ_[p] K + 2)

The generator rank of a local absolute Galois group as a least cardinality (NSW (7.4.1)). For a finite extension K of ℚ_p, the least cardinality of a finite subset of G_K generating a dense subgroup is [K : ℚ_p] + 2.