Documentation

GQ2.Statement

The main theorem (Theorem 1.2) #

We give the surjection-count form of the theorem, which is:

Let G_{ℚ₂} be the absolute Galois group of ℚ₂ (Mathlib's Field.absoluteGaloisGroup ℚ_[2], which for the char-0 field ℚ₂ is the genuine Gal(ℚ₂^sep/ℚ₂)).

Theorem 1.2 (surjection-count form). For every finite group G, the number of continuous surjections G_{ℚ₂} ↠ G equals the number of admissible marked generating quadruples in G (GQ2.admissibleCount G).

Combined with GQ2.reconstruction (Lemma 2.5) and GQ2.admissibleCount = |Sur(Γ_A, ·)| (Prop. 2.3), this yields the literal statement G_{ℚ₂} ≅ Γ_A, i.e. Theorem 1.2 as printed.

source
@[reducible, inline]
noncomputable abbrev GQ2.AbsGalQ2 :
Type

G_{ℚ₂}, the absolute Galois group of the 2-adic numbers, as a topological group.

Equations
Instances For
    source
    noncomputable def GQ2.contSurjCount (G : Type) [Group G] [TopologicalSpace G] [DiscreteTopology G] :
    ℕ

    The number of continuous surjections G_{ℚ₂} ↠ G onto a finite discrete group G.

    Equations
    Instances For

      Theorem 1.2 (surjection-count form) — for every finite group G, the number of continuous surjections G_{ℚ₂} ↠ G equals admissibleCount G (the admissible marked generating quadruples; paper eq. (154) + Prop. 2.3) — is GQ2.SectionTen.main_surjection_count' (proved in GQ2/SectionTenSources.lean). It cannot live here: Statement.lean sits upstream of the §§4–9 tower (it is imported by GammaA.lean/FoxHeisenberg.lean), so an in-place proof — which needs the whole tower and the concrete boundaryMapsWitness — would cycle. Therefore main_presentation below takes the count as the hypothesis hcount; the downstream theorem main_presentation_literal supplies it from main_surjection_count'. The proof reduces to a minimal list of nine classical literature results (Demushkin classification, G_ℚ₂(2) Demushkin, local reciprocity, local Tate duality, local Euler characteristic, dyadic Hilbert symbol, 2-adic cyclotomic surjectivity, G_ℚ₂ top. f.g., Evens/Stiefel–Whitney), enumerated in docs/literature-axioms.md; its trust base is the standard three axioms plus the nine literature interfaces in GQ2/Foundations/Axioms.lean.

      The literal presentation form (Theorem 1.2 as printed) #

      The honest candidate Γ_A is now constructed in GQ2/GammaA.lean (the paper's marked quotient construction, eq. (7), on GQ2.FreeProfiniteGroup (Fin 4), with the relations readable both profinitely via ℤ̂/ω₂/^ᶻ from GQ2/Zhat.lean and finitely via GQ2/Words.lean — the two readings provably agree). The literal Theorem 1.2 is stated there as GQ2.main_presentation_literal : Nonempty (ContinuousMulEquiv GammaA AbsGalQ2).

      The schematic form below keeps the top-level logic explicit and checked: given Prop. 2.3 for a candidate (hΓA: its continuous surjection counts are the admissible-marking counts) and topological finite generation, reconstruction (Lemma 2.5) + main_surjection_count deliver the isomorphism. GQ2/PresentationLiteral.lean instantiates it at Γ_A, discharging hΓA (paper §2, Prop. 2.3) and hfgΓ.

      source
      theorem GQ2.main_presentation (ΓA : Type) [Group ΓA] [TopologicalSpace ΓA] [IsTopologicalGroup ΓA] [CompactSpace ΓA] [TotallyDisconnectedSpace ΓA] [CompactSpace AbsGalQ2] [TotallyDisconnectedSpace AbsGalQ2] (hfgΓ : ∃ (s : Finset ΓA), (Subgroup.closure ↑s).topologicalClosure = ⊤) (hfgG : ∃ (s : Finset AbsGalQ2), (Subgroup.closure ↑s).topologicalClosure = ⊤) (hΓA : ∀ (G : Type) [inst : Group G] [inst_1 : TopologicalSpace G] [DiscreteTopology G] [Finite G], Nat.card (ContSurj ΓA G) = admissibleCount G) (hcount : ∀ (G : Type) [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : DiscreteTopology G] [Finite G], contSurjCount G = admissibleCount G) :
      Nonempty (ΓA ≃ₜ* AbsGalQ2)

      Theorem 1.2 (literal presentation form), schematic. Any candidate profinite group Γ_A with the surjection-count property of Prop. 2.3 (the honest one is GQ2.GammaA) is continuously isomorphic to G_{ℚ₂}.

      ΓA stands in for the presented profinite group; hΓA is Prop. 2.3 (its finite quotients are the admissible markings); hcount is Theorem 1.2's surjection-count form for G_{ℚ₂} (contSurjCount G = admissibleCount G, = SectionTen.main_surjection_count'; it is a hypothesis here because its proof is downstream of this upstream file); hfgΓ/hfgG are topological finite generation of Γ_A and of G_{ℚ₂} (both true — G_{ℚ₂} is topologically finitely generated, being the absolute Galois group of a local field). The conclusion is Theorem 1.2.

      Paper-tag ledger (auto-generated by paperforge; do not edit) #