The absolute Galois group G_{ℚ₂} of the 2-adic field (Stage: Local) #
This file defines GQ2Profinite : ProfiniteGrp, the absolute Galois group
G_{ℚ₂} = Gal(Q̄₂/ℚ₂) of the field ℚ₂ = ℚ_[2] of 2-adic numbers.
This is the target of the project's final theorem
presentation_correct : Nonempty (GammaA ≅ GQ2Profinite). The object is the one
named in the manuscript (reference/q2_manuscript.tex, l.115–122 and l.149–156):
the absolute Galois group G_{ℚ₂} of ℚ₂, i.e. Gal(Q̄₂/ℚ₂).
Construction #
ℚ₂ has characteristic 0, hence is perfect, so its separable closure coincides
with an algebraic closure Q̄₂. We take
K := SeparableClosure ℚ_[2],
which mathlib defines (Mathlib/FieldTheory/SeparableClosure.lean) as the relative
separable closure of ℚ_[2] inside AlgebraicClosure ℚ_[2]. As an
IntermediateField it carries the Field and Algebra ℚ_[2] _ instances
automatically, and it is Galois over the base via
separableClosure.isGalois : [Normal F E] → IsGalois F (separableClosure F E),
instantiated at E = AlgebraicClosure ℚ_[2]; the hypothesis Normal ℚ_[2] (AlgebraicClosure ℚ_[2]) is supplied by the IsAlgClosure → Normal instance
(Mathlib/FieldTheory/IsAlgClosed/Basic.lean). All four typeclass arguments of
InfiniteGalois.profiniteGalGrp (Field k, Field K, Algebra k K,
IsGalois k K) are therefore found by instance resolution; the Fact (Nat.Prime 2)
needed to form ℚ_[2] = Padic 2 is the global Nat.fact_prime_two.
mathlib's InfiniteGalois.profiniteGalGrp k K
(Mathlib/FieldTheory/Galois/Profinite.lean) then packages the Krull-topologised
Galois group Gal(K/k) as an object of ProfiniteGrp, using that it is a limit of
the finite Galois groups Gal(L/k).
Main definition #
Q2Presentation.GQ2Profinite : ProfiniteGrp— the absolute Galois group ofℚ₂.
The absolute Galois group G_{ℚ₂} = Gal(Q̄₂/ℚ₂) of the 2-adic field
ℚ₂ = ℚ_[2], as a profinite group.
Concretely it is Gal(SeparableClosure ℚ_[2] / ℚ_[2]), packaged as an object of
ProfiniteGrp by InfiniteGalois.profiniteGalGrp. Since ℚ_[2] has
characteristic 0 its separable closure is an algebraic closure, so this is the
absolute Galois group in the usual sense, matching the manuscript's G_{ℚ₂}.