Documentation

Q2Presentation.Boundary.BoundaryGQ2

The local boundary package on G_{ℚ₂} (Stage C) #

This file assembles the local boundary package boundaryPackage_GQ2 : BoundaryPackage GQ2Profinite — the G_{ℚ₂}-side instance of the uniform Stage-C datum of a tame quotient G_{ℚ₂} ↠ T_A, a maximal pro-2 quotient G_{ℚ₂} ↠ Π, and a common unramified character ν_loc : G_{ℚ₂} ↠ ℤ₂ through which both factor (manuscript reference/q2_manuscript.tex, Prop 3.14 prop:compatiblemarking, l.1085–1110; plan reference/plan_4turns.md Turn 4 §6).

The two markings #

Axiom audit #

boundaryPackage_GQ2 depends on exactly two non-standard axioms:

So #print axioms boundaryPackage_GQ2 = {propext, Classical.choice, Quot.sound, labute_GQ2_maxPro2_marked, gq2_tame_quotient}. (It does not depend on the Goursat core tameMap_ker_pro2Map_ge of Boundary/BoundaryPackage.lean — now proven unconditionally — which is a separate theorem unused here: assembling a BoundaryPackage value requires only its fields.)

A helper: the forward map of a ProfiniteGrp isomorphism is surjective #

source
theorem Q2Presentation.isoHom_surjective {X Y : ProfiniteGrp.{u}} (e : X ≅ Y) :
Function.Surjective ⇑(ProfiniteGrp.Hom.hom e.hom)

The forward map e.hom of an isomorphism of profinite groups is surjective: e.inv y is a preimage of y (ProfiniteGrp.hom_inv_apply).

The maximal pro-2 side from the marked Demushkin normalization #

source
noncomputable def Q2Presentation.pro2Map_loc :
GQ2Profinite ⟶ PiGrp

The local maximal pro-2 quotient map pro2Map_loc : G_{ℚ₂} ↠ Π (manuscript Prop 3.10 / cor:relativeDemushkin). It factors G_{ℚ₂} through its maximal pro-2 quotient G_{ℚ₂}(2) (maxPro2Proj), then across Labute's classification G_{ℚ₂}(2) ≅ D₀ (labute_GQ2_maxPro2_marked.iso) and the profinite Nielsen comparison D₀ ≅ Π (D0_iso_PiGrp).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    noncomputable def Q2Presentation.nu_loc :
    GQ2Profinite ⟶ ProfiniteZ2

    The common unramified character ν_loc : G_{ℚ₂} ↠ ℤ₂: the maximal pro-2 projection followed by the genuine local unramified character ν_ur^{loc} = labute_GQ2_maxPro2_marked.nu_ur_loc (geometric Frobenius ↦ 1). This is the ν_Γ of Prop compatiblemarking for Γ = G_{ℚ₂}.

    Equations
    Instances For
      source
      theorem Q2Presentation.pro2Map_loc_surjective :
      Function.Surjective ⇑(ProfiniteGrp.Hom.hom pro2Map_loc)

      pro2Map_loc is surjective, being the composite of the surjective maxPro2Proj (maxPro2Proj_surjective) and the two surjective isomorphism hom-maps (isoHom_surjective).

      source
      theorem Q2Presentation.pro2Map_loc_nu :
      CategoryTheory.CategoryStruct.comp pro2Map_loc nu_2 = nu_loc

      The pro-2 marking is ν_loc: pro2Map_loc ≫ ν₂ = ν_loc (the pro-2 half of Prop compatiblemarking for G_{ℚ₂}). Chains the marking labute_GQ2_maxPro2_marked.marked (ν_ur^{loc} = iso.hom ≫ ν_ur) with the Nielsen marking nu_ur_eq_hom_comp_nu_2 (ν_ur = D0_iso_PiGrp.hom ≫ ν₂).

      The tame side: one local axiom (Prop 3.2 + the local half of compatiblemarking) #

      Proposition 3.2 (prop:tamequotient, manuscript l.421) gives the canonical local tame quotient G_{ℚ₂}/W_F ≅ T_A; lem:o2tame identifies wild inertia with the local characteristic 2-core; and the local half of Prop compatiblemarking (l.1085–1110, "For the local source, use cor:relativeDemushkin") furnishes the unramified character matching the marked pro-2 quotient. These are local class field theory, irreducible and absent from mathlib v4.28.0; we package them as a single GQ2TameQuotient datum recorded by the axiom gq2_tame_quotient.

      source
      structure Q2Presentation.GQ2TameQuotient :
      Type

      The local tame-quotient datum for G_{ℚ₂} (Prop 3.2 + the local half of Prop compatiblemarking). Bundles the tame quotient map G_{ℚ₂} ↠ T_A, its surjectivity, the compatibility that it realises the same unramified character ν_loc as the marked pro-2 quotient (pro2Map_loc), and the local tame maximality/factorization property from Prop 3.2 plus lem:o2tame: every finite quotient with its 2-core collapsed factors through the tame quotient.

      Instances For
        source
        axiom Q2Presentation.gq2_tame_quotient :
        GQ2TameQuotient

        Prop 3.2 + Prop compatiblemarking (local): the local tame quotient G_{ℚ₂} ↠ T_A, with unramified character matching the marked pro-2 quotient — local class field theory, irreducible.

        The maximal tame quotient of the absolute Galois group G_{ℚ₂} of ℚ₂ is the profinite tame group T_A = ⟨σ,τ ∣ τ^σ = τ²⟩ (manuscript Prop 3.2 prop:tamequotient, l.421: G_{ℚ₂}/W_F ≅ T_A; the tame quotient has pro-prime-to-2 cyclic inertia and procyclic unramified quotient, with geometric Frobenius acting on tame inertia by x ↦ x²), and the quotient map can be chosen so that its composite with the tame unramified character ν_t is the same natural unramified character ν_loc : G_{ℚ₂} ↠ ℤ₂ as the marked pro-2 quotient (the local half of Prop compatiblemarking, l.1085–1110).

        This is genuine local class field theory, absent from mathlib v4.28.0 (no local reciprocity, no ramification filtration, no structure theorem for the tame quotient or wild-inertia characteristic-core theorem). It is the project's single new tame axiom; together with the pro-2 side (reached through labute_GQ2_maxPro2_marked) it furnishes boundaryPackage_GQ2 and the local factorization theorem used by the §10 frame-exhaustion sidecar. #print axioms boundaryPackage_GQ2 exhibits it as gq2_tame_quotient.

        The local boundary package #

        source
        noncomputable def Q2Presentation.boundaryPackage_GQ2 :
        BoundaryPackage GQ2Profinite

        The local boundary package boundaryPackage_GQ2 : BoundaryPackage G_{ℚ₂} (manuscript Prop 3.14 prop:compatiblemarking for Γ = G_{ℚ₂}; plan Turn 4 §6), the G_{ℚ₂}-side instance of the uniform Stage-C boundary datum.

        • tameMap/tame_surj/tame_nu — the local tame quotient G_{ℚ₂} ↠ T_A with unramified marking ν_loc, from the axiom gq2_tame_quotient (Prop 3.2 + the local half of Prop compatiblemarking);
        • pro2Map/pro2_surj/pro2_nu — the local maximal pro-2 quotient G_{ℚ₂} ↠ Π with the same unramified marking ν_loc, proved from the fully marked Labute comparison labute_GQ2_maxPro2_marked (pro2Map_loc, pro2Map_loc_surjective, pro2Map_loc_nu);
        • nu := ν_loc — the common unramified character through which both factor.
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

          Acceptance checks #