Exact-image and epimorphism semantics (Stage B, work order B5)

This file closes Stage B. It proves the exact-image finite-quotient semantics of the candidate profinite group Γ_A, and derives the manuscript's epimorphism semantics (Proposition 2.3) as a corollary.

The exact-image refinement (manuscript Prop 2.3 + the Remark after it)

The manuscript warns (Remark following Prop 2.3) that the naive statement "a homomorphism Γ_A → G into a fixed ambient finite group induces an admissible marking of G" is false for non-surjective maps: the image of the wild subgroup W_A is only normal-of-2-power inside the image subgroup, and need not land in the 2-core O₂(G) of the ambient G. The correct, true statement tracks the exact image:

• exactImageSubgroup φ — the range subgroup MonoidHom.range φ ≤ H of a continuous hom φ : Γ_A ⟶ H;
• exactImageMarking φ — the induced marking of that range subgroup;
• GammaA_hom_exactImage_admissible — this marking is always Admissible.

The proof factors φ = π_A ≫ ψ through an admissible finite stage A (GammaA_map_to_finite_factors). Because π_A is surjective (piMon_surjective), range φ = range ψ, so ψ corestricts to a surjection Fin A.n ↠ exactImageSubgroup φ. Admissibility of A.q then transports along that surjection (admissible_map_surjective) to exactImageMarking φ.

Epimorphism semantics (Proposition 2.3)

GammaA_epi_equiv_admissible packages the bijection

SurjContHom Γ_A G  ≃  { q : Marking G // Admissible q }.

• Forward: a surjection f has exactImageSubgroup f = ⊤, so the exact-image marking is, via the (now surjective) top-subgroup inclusion, an admissible marking of G itself.
• Backward: an admissible (q, hq) skeletalizes to an index A = skeletalize G q hq; the limit projection π_A is surjective (piMon_surjective), and the transport iso skelEquiv carries Fin A.n onto G, giving an epimorphism Γ_A ↠ G.
• The two are mutually inverse: a continuous hom out of Γ_A into a finite (Hausdorff) group is pinned by its values on the topological generators gammaGen (gammaGen_topologically_generate + hom_ext_of_dense).

Two implementation notes. (i) ProfiniteGrp.ofFiniteGrp (FiniteGrp.of H) already requires [Finite H], so all four declarations carry [Finite H]/[Finite G] even where the plan sketch omitted it; and GammaA_epi_equiv_admissible is an Equiv (data), hence a noncomputable def, not a theorem. (ii) The transport skelMor pins the source MulOneClass of MulEquiv.toMonoidHom to the transported groupFin structure with an explicit @, so it cannot grab the global Fin.instMul (the documented Fin.instMul-vs-groupFin gotcha).

instance Q2Presentation.instFiniteOfFiniteGrp {X : FiniteGrp.{u_1}} : Finite ↑(ProfiniteGrp.ofFiniteGrp X).toProfinite.toTop

The underlying space of ofFiniteGrp X is finite (it is the carrier ↥X of the finite group X). Mathlib does not register this through the ProfiniteGrp coercion layers, but every Subgroup/Finite/MonoidHom.range argument over a finite target of G needs it; without it the class search loops in whnf. Mirrors instFiniteAdmissibleObj in Candidate/GammaA.lean.

Exact-image subgroup and induced marking

noncomputable def Q2Presentation.exactImageSubgroup {H : Type} [Group H] [Finite H] (φ : GammaA ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of H)) : Subgroup H

The exact image of a continuous homomorphism φ : Γ_A ⟶ H into a finite group: the range subgroup MonoidHom.range φ of H.

Equations

• Q2Presentation.exactImageSubgroup φ = (ProfiniteGrp.Hom.hom φ).range

noncomputable def Q2Presentation.exactImageMarking {H : Type} [Group H] [Finite H] (φ : GammaA ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of H)) : Marking ↥(exactImageSubgroup φ)

The marking of the exact image induced by φ: each universal generator gammaGen a maps to its image φ (gammaGen a), viewed inside the range subgroup exactImageSubgroup φ.

Equations

• Q2Presentation.exactImageMarking φ a = ⟨(ProfiniteGrp.Hom.hom φ).toMonoidHom (Q2Presentation.gammaGen a), ⋯⟩

Exact-image admissibility

theorem Q2Presentation.GammaA_hom_exactImage_admissible {H : Type} [Group H] [Finite H] (φ : GammaA ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of H)) : Admissible (exactImageMarking φ)

Exact-image semantics (manuscript Prop 2.3, exact-image form). For every continuous homomorphism φ : Γ_A ⟶ H into a finite group H, the induced marking of the exact image exactImageSubgroup φ is admissible.

This is the true statement the manuscript Remark insists on: it tracks the exact image, sidestepping the false ambient claim. The proof factors φ = π_A ≫ ψ through an admissible stage A (GammaA_map_to_finite_factors); surjectivity of π_A (piMon_surjective) lets ψ corestrict to a surjection Fin A.n ↠ exactImageSubgroup φ, and admissibility of A.q transports along it (admissible_map_surjective).

Epimorphism semantics (Proposition 2.3)

noncomputable def Q2Presentation.GammaA_epi_equiv_admissible (G : Type) [Group G] [Finite G] [Nonempty G] : Profinite.SurjContHom GammaA (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G)) ≃ { q : Marking G // Admissible q }

Epimorphic finite-quotient semantics (manuscript Proposition 2.3). For every finite group G, the surjective continuous homomorphisms Γ_A ↠ G are in natural bijection with the admissible markings of G.

Forward: a surjection induces an admissible marking of G via the exact-image theorem with image ⊤ (admissible_of_surj). Backward: an admissible marking skeletalizes to an admissible stage whose limit projection, transported by skelEquiv, is an epimorphism (epiOfMarking). The two are mutually inverse because a hom out of Γ_A is determined by its values on gammaGen (epiHom_ext).

Equations

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

Acceptance checks