Proposition 2.3: |Sur(Γ_A, G)| = N(G)

The paper's Prop. 2.3 (§2.2): for every finite group G, continuous surjections Γ_A ↠ G correspond bijectively to admissible marked generating quadruples in G, so Nat.card (ContSurj Γ_A G) = admissibleCount G. This is the Γ_A half of the surjection-count Theorem 1.2 (the G_{ℚ₂} half is main_surjection_count, Track B); together with Lemma 2.5 (reconstruction, the reconstruction proof) and t.f.g. (the finite-generation proof) it yields the literal presentation form in the literal-presentation proof.

The bijection

contSurjEquivAdmissible : ContSurj (F₄ ⧸ N_A) G ≃ {t : Marking G // t.Admissible}

• forward: push the universal marking through φ ∘ π (π : F₄ → F₄ ⧸ N_A the projection). Admissibility is admissible_of_NA_le_ker — the converse of NA_le_ker (the literal Γ_A construction): for a continuous f : F₄ → G into a finite discrete group, surjective with N_A ≤ ker f, the pushed marking is admissible. Proof: ker f is an admissible open normal subgroup (isAdmissibleU_of_NA_le, the admissible-limit proof), and admissibility transfers along the induced isomorphism F₄ ⧸ ker f ≃* G (Lemma 2.2, Marking.map_admissible). Together NA_le_ker and admissible_of_NA_le_ker say: for surjective continuous f, the pushed marking is admissible iff N_A ≤ ker f — the paper's "quotients of Γ_A = admissible quotients".
• backward (Marking.descend): an admissible t classifies t.toHom : F₄ ⟶ G (universal property of F₄), which kills N_A by NA_le_ker, hence descends along quotientLift; surjectivity from t.Generates (surjective_of_map_generates).
• round-trips: univMarking_map_toHom (the literal Γ_A construction) in one direction; in the other, the uniqueness half of the universal property (Marking.toHom_univMarking_map: any morphism out of F₄ is toHom of its own pushed marking) plus surjectivity of π. Encoding note: topological finite generation is not needed — homEquiv-injectivity replaces the density argument for "agreeing on generators ⇒ equal".

The count Nat.card (ContSurj GammaA G) = admissibleCount G (prop_2_3) is stated in exactly the hΓA shape consumed by main_presentation (GQ2/Statement.lean). Everything is at the standard three axioms (Ax = ∅).

The universal property, uniqueness half

theorem GQ2.Marking.toHom_hom_univMarking_map {G : Type} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] (c : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop →ₜ* G) : ProfiniteGrp.Hom.hom (map c.toMonoidHom univMarking).toHom = c

ContinuousMonoidHom-level form of the uniqueness half: classifying the pushforward of the universal marking along c recovers c.

The converse of NA_le_ker

theorem GQ2.admissible_of_NA_le_ker {G : Type} [Group G] [TopologicalSpace G] [DiscreteTopology G] [Finite G] (f : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop →ₜ* G) (hsurj : Function.Surjective ⇑f) (hker : NA ≤ f.ker) : (Marking.map f.toMonoidHom univMarking).Admissible

Converse of NA_le_ker (with it: the paper's characterization of the admissible finite quotients of F₄ as exactly the surjections killing N_A, §2.1–2.2). If a continuous homomorphism f : F₄ → G into a finite discrete group is surjective and kills N_A, then the pushed universal marking of G is admissible: ker f is then an open normal subgroup above N_A, hence admissible (isAdmissibleU_of_NA_le, the admissible-limit proof), and admissibility transfers to G along F₄ ⧸ ker f ≃* G (Lemma 2.2).

The two directions of the bijection, as named constructions

noncomputable def GQ2.Marking.push {G : Type} [Group G] [TopologicalSpace G] (φ : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA →ₜ* G) : Marking G

The marking of G pushed forward from the universal marking along φ : F₄ ⧸ N_A → G.

Equations

• GQ2.Marking.push φ = GQ2.Marking.map (φ.comp (GQ2.quotientMk GQ2.NA)).toMonoidHom GQ2.univMarking

theorem GQ2.Marking.push_admissible {G : Type} [Group G] [TopologicalSpace G] [DiscreteTopology G] [Finite G] (φ : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA →ₜ* G) (hφ : Function.Surjective ⇑φ) : (push φ).Admissible

The pushed marking of a continuous surjection is admissible (forward direction of Prop 2.3).

noncomputable def GQ2.Marking.classify {G : Type} [Group G] [TopologicalSpace G] [DiscreteTopology G] [Finite G] (t : Marking G) : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop →ₜ* G

The classified hom of an admissible marking, as a continuous homomorphism out of F₄ (the gammaA_surjective_s3 ascription pattern).

Equations

• t.classify = ProfiniteGrp.Hom.hom t.toHom

noncomputable def GQ2.Marking.descend {G : Type} [Group G] [TopologicalSpace G] [DiscreteTopology G] [Finite G] (t : Marking G) (ht : t.Admissible) : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA →ₜ* G

The descended hom Γ_A → G of an admissible marking (backward direction of Prop 2.3).

Equations

• t.descend ht = GQ2.quotientLift GQ2.NA t.classify ⋯

theorem GQ2.Marking.descend_surjective {G : Type} [Group G] [TopologicalSpace G] [DiscreteTopology G] [Finite G] (t : Marking G) (ht : t.Admissible) : Function.Surjective ⇑(t.descend ht)

theorem GQ2.Marking.push_descend {G : Type} [Group G] [TopologicalSpace G] [DiscreteTopology G] [Finite G] (t : Marking G) (ht : t.Admissible) : push (t.descend ht) = t

Pushing the descended hom recovers the marking (round-trip 1).

theorem GQ2.Marking.descend_push {G : Type} [Group G] [TopologicalSpace G] [DiscreteTopology G] [Finite G] (φ : ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA →ₜ* G) (hφ : Function.Surjective ⇑φ) : (push φ).descend ⋯ = φ

Descending the pushed marking recovers the surjection (round-trip 2, via the uniqueness half of the universal property).

Prop 2.3

noncomputable def GQ2.contSurjEquivAdmissible (G : Type) [Group G] [TopologicalSpace G] [DiscreteTopology G] [Finite G] : ContSurj (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA) G ≃ { t : Marking G // t.Admissible }

Prop. 2.3, bijection form (paper §2.2): continuous surjections Γ_A ↠ G correspond to admissible markings of G. (Stated on the underlying quotient F₄ ⧸ N_A, to which GammaA is definitionally equal.)

Equations

• One or more equations did not get rendered due to their size.

theorem GQ2.prop_2_3 (G : Type) [Group G] [TopologicalSpace G] [DiscreteTopology G] [Finite G] : Nat.card (ContSurj (↑GammaA.toProfinite.toTop) G) = admissibleCount G

Proposition 2.3 (paper §2.2): the number of continuous surjections Γ_A ↠ G onto a finite discrete group equals the number of admissible marked generating quadruples in G — in exactly the hΓA shape that main_presentation (GQ2/Statement.lean) consumes.

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

• Lemma 2.2 = ⟦lem-cofinal⟧
• Lemma 2.5 = ⟦lem-reconstruction⟧
• Proposition 2.3 = ⟦prop-epi-semantics⟧
• Theorem 1.2 = ⟦thm-main⟧