2. Introduction and main theorem🔗

Proposition2.1

groupuses 0used by 1✓L∃∀N

Proposition 1.1 of the paper (Marked dyadic Demushkin normalization).

Let D_{\mathrm{loc}}=G_{\Qtwo}(2) and let \nu_{\mathrm{ur}}:D_{\mathrm{loc}}\twoheadrightarrow\mathbb{Z}_2 be normalized by sending geometric Frobenius to 1. There exist topological generators a,s,y such that

D_{\mathrm{loc}}\cong \left\langle a,s,y\;\middle|\;a^2s^4[s,y]=1\right\rangle_{\mathrm{pro}-2}, \qquad \nu_{\mathrm{ur}}(a)=-2,\quad \nu_{\mathrm{ur}}(s)=1,\quad \nu_{\mathrm{ur}}(y)=0.

The proof is given in Sections Subsection 3.1–Subsection 3.3.

Lean code for Proposition2.1●1 theorem

theoremdefined in GQ2/PropOneOneAssembly.lean

complete

theorem GQ2.SectionThree.prop_1_1 [CompactSpace GQ2.AbsGalQ2]
  [TotallyDisconnectedSpace GQ2.AbsGalQ2] (R : GQ2.LocalReciprocity) :
  ∃ e,
    (∀ (g : GQ2.AbsGalQ2),
        (GQ2.maxProPMk 2 GQ2.AbsGalQ2) g = e.symm GQ2.d0A →
          R.nu_ur (GQ2.toAb g) = Multiplicative.ofAdd ↑(-2)) ∧
      (∀ (g : GQ2.AbsGalQ2),
          (GQ2.maxProPMk 2 GQ2.AbsGalQ2) g = e.symm GQ2.d0S →
            R.nu_ur (GQ2.toAb g) = Multiplicative.ofAdd ↑1) ∧
        ∀ (g : GQ2.AbsGalQ2),
          (GQ2.maxProPMk 2 GQ2.AbsGalQ2) g = e.symm GQ2.d0Y →
            R.nu_ur (GQ2.toAb g) = Multiplicative.ofAdd ↑0

theorem GQ2.SectionThree.prop_1_1
  [CompactSpace GQ2.AbsGalQ2]
  [TotallyDisconnectedSpace GQ2.AbsGalQ2]
  (R : GQ2.LocalReciprocity) :
  ∃ e,
    (∀ (g : GQ2.AbsGalQ2),
        (GQ2.maxProPMk 2 GQ2.AbsGalQ2) g =
            e.symm GQ2.d0A →
          R.nu_ur (GQ2.toAb g) =
            Multiplicative.ofAdd ↑(-2)) ∧
      (∀ (g : GQ2.AbsGalQ2),
          (GQ2.maxProPMk 2 GQ2.AbsGalQ2)
                g =
              e.symm GQ2.d0S →
            R.nu_ur (GQ2.toAb g) =
              Multiplicative.ofAdd ↑1) ∧
        ∀ (g : GQ2.AbsGalQ2),
          (GQ2.maxProPMk 2 GQ2.AbsGalQ2)
                g =
              e.symm GQ2.d0Y →
            R.nu_ur (GQ2.toAb g) =
              Multiplicative.ofAdd ↑0

**Proposition 1.1.**  A marked isomorphism `e : G_{ℚ₂}(2) ≅ D₀` with unramified
coordinates `ν_ur(a, s, y) = (−2, 1, 0)`.  Assembled from B3c (`orientBundle.equiv`), Lemma 3.5
(`lemma_3_5_marked_abelianization`, using `markedHom_bijective`),
and Prop. 3.8 (`prop_3_8_classification`/`prop_3_8_lift`).  The statement is placed here to
respect the import DAG; see the pointer in `GQ2/SectionThree.lean`.

Proof for Proposition 2.1

Proof uses 3

Proof dependency previews

Preview

Proposition 1.5

Loading preview

Proof dependency preview content is loaded from the rendered-fragment cache.

Proved in §1 of the paper. Ingredients: Proposition 1.5 Lemma 4.4 Lemma 4.7.

Theorem2.2

groupuses 0used by 0✓L∃∀N

Theorem 1.2 of the paper (Presentation theorem).

The absolute Galois group \GQ is isomorphic to the profinite group topologically generated by

\sigma,\tau,x_0,x_1,

for which the closed normal subgroup generated by x_0,x_1 is pro-2, and which is subject to the two relations

\tau^\sigma=\tau^2

and

h_0u_1^{-1}x_1^\sigma c_0=1,

where the auxiliary words are defined in (1)–(3).

Lean code for Theorem2.2●3 theorems

theoremdefined in GQ2/PresentationLiteral.lean

complete

theorem GQ2.main_presentation_literal :
  Nonempty (↑GQ2.GammaA.toProfinite.toTop ≃ₜ* GQ2.AbsGalQ2)

theorem GQ2.main_presentation_literal :
  Nonempty
    (↑GQ2.GammaA.toProfinite.toTop ≃ₜ*
      GQ2.AbsGalQ2)

**Theorem 1.2 (literal presentation form)**: the honest candidate `Γ_A` is continuously
isomorphic to `G_{ℚ₂}`.  Instantiates `main_presentation` at `Γ_A`: `hΓA := prop_2_3` (the `Γ_A`
admissible-marking count), `hcount := SectionTen.main_surjection_count'` (the `G_{ℚ₂}` surjection
count), and the topological finite-generation witnesses of `Γ_A` and `G_{ℚ₂}`.

theoremdefined in GQ2/SectionTenSources.lean

complete

theorem GQ2.SectionTen.main_surjection_count' [CompactSpace GQ2.AbsGalQ2]
  [TotallyDisconnectedSpace GQ2.AbsGalQ2] (G : Type) [Group G]
  [Finite G] [TopologicalSpace G] [DiscreteTopology G] :
  GQ2.contSurjCount G = GQ2.admissibleCount G

theorem GQ2.SectionTen.main_surjection_count'
  [CompactSpace GQ2.AbsGalQ2]
  [TotallyDisconnectedSpace GQ2.AbsGalQ2]
  (G : Type) [Group G] [Finite G]
  [TopologicalSpace G]
  [DiscreteTopology G] :
  GQ2.contSurjCount G =
    GQ2.admissibleCount G

**Theorem 1.2, surjection-count form** (`GQ2.main_surjection_count`), proved from eq. (154) +
Prop 2.3.  The original `Statement.lean` placeholder was resolved by the statement-move pattern
(Statement is upstream of the tower); the moved statement carries the tower-standing
`AbsGalQ2` instance binders.

theoremdefined in GQ2/Statement.lean

complete

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

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

Proof for Theorem 2.2

Proof uses 4

Proof dependency previews

Preview

Proposition 3.1

Loading preview

Proof dependency preview content is loaded from the rendered-fragment cache.

Proved in §1 of the paper. Ingredients: Lemma 3.2 Lemma 11.1 Proposition 3.1 Theorem 5.1.