Tame-quotient factorization, candidate side, de-axiomatized

(gammaA_tameQuotientFactor_proven)

This file replaces the axiom Q2Presentation.Induction.gammaA_tameQuotientFactor (Induction/FrameExhaustion.lean, manuscript prop:tamequotient for Γ_A) by a theorem gammaA_tameQuotientFactor_proven with the exact same statement: for every continuous epimorphism f : Γ_A ↠ G onto a finite group, the induced quotient map Γ_A ↠ G/O₂(G) factors through the candidate tame quotient gammaTameMap : Γ_A ↠ T_A, i.e. there is α : T_A ⟶ G/O₂(G) with mk ∘ f = α ∘ gammaTameMap.

Method (no kernel characterisation needed)

The factorization is the universal property of the inverse limit T_A = lim tameDiagram, applied to the object that f itself produces — so it does not require the unproved kernel equality ker(gammaTameMap) = W_A. Concretely:

• Put H = G/O₂(G) and mk : G ↠ H the projection (ker mk = O₂(G)).
• The G-marking a ↦ f (gammaGen a) is admissible (GammaA_epi_equiv_admissible, the epimorphism semantics); pushing it along the surjection mk (admissible_map_surjective) gives an admissible H-marking q_H a = mk (f (gammaGen a)). Admissibility hands us exactly the data of a tame index: q_H σ, q_H τ generate H and satisfy the tame relation rconj (q_H τ) (q_H σ) = (q_H τ)². The wild generators die: f x₀, f x₁ ∈ O₂(G) = ker mk, so q_H x₀ = q_H x₁ = 1 (this is the only place the marking's x₀,x₁ ∈ O₂ condition is used).
• Hence (H, q_H σ, q_H τ) is a TameMarkedFinite object A_H (tameSkeletalize), one of the indices defining T_A. The induced frame is the limit projection at A_H, transported back from the skeleton Fin A_H.n to H: α = π_{A_H} ≫ (Fin A_H.n ≃* H).
• α ∘ gammaTameMap = mk ∘ f: precomposing the projection with gammaTameMap is the fixed-stage surjection pSurjTame A_H (gammaTameMap_proj), which sends each gammaGen a to the marked generator tameMarking A_H a = (A_H.s, A_H.t, 1, 1); transporting these back gives (q_H σ, q_H τ, 1, 1) = mk (f (gammaGen a)). The two continuous homs therefore agree on the four topological generators, hence everywhere (gammaTameGen_hom_ext).

The surviving axiom closure is [propext, Classical.choice, Quot.sound] — the proof adds no new axiom; in particular it does not depend on gammaA_tameQuotientFactor.

theorem Q2Presentation.Induction.tameRel_rconj {K : Type u_1} [Group K] [Finite K] {q : Marking K} (h : tameRel q) : rconj (q Gen.tau) (q Gen.sigma) = q Gen.tau ^ 2

The tame relator, in the explicit rconj form: if a marking q of a finite group satisfies tameRel q (the relator evaluates to 1), then rconj (q τ) (q σ) = (q τ)².

theorem Q2Presentation.Induction.gammaA_tameQuotientFactor_proven (G : Type) [Group G] [Finite G] [Nonempty G] (f : Profinite.SurjContHom GammaA (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G))) : ∃ (α : Ttame ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of (G ⧸ twoCore G))), ∀ (γ : ↑GammaA.toProfinite.toTop), (QuotientGroup.mk' (twoCore G)) ((ProfiniteGrp.Hom.hom f.hom) γ) = (ProfiniteGrp.Hom.hom α) ((ProfiniteGrp.Hom.hom boundaryPackage_GammaA.tameMap) γ)

Acceptance checks