Finite factorization of maps out of Γ_A (Stage B, work order B4)

This file proves the finite-factorization theorem, the load-bearing topological API of Stage B (plan §5, manuscript Lemma 2.2 Cofinality): every continuous homomorphism from the candidate profinite group Γ_A to a finite group factors through one of the finite admissible quotients.

GammaA_map_to_finite_factors :
  (φ : Γ_A ⟶ ofFiniteGrp (FiniteGrp.of H)) →
    ∃ A ψ, φ = (limit.π admissibleDiagram A) ≫ ψ

Proof outline (= manuscript Lemma 2.2 compactness argument)

Work in the explicit inverse-limit model L := ProfiniteGrp.limit admissibleDiagram (via the bridge gammaIso), whose points are compatible families m : ∀ A, Fin A.n carrying the subspace topology of the product ∏_A Fin A.n.

• limit_finite_factor: a continuous map f : L → H into any discrete space depends on a single coordinate. Since H is discrete, each fibre f⁻¹{f m} is open; in the product topology it contains a basic-clopen box fixing finitely many coordinates J_m (isOpen_pi_iff), on which f is constant. Compactness of L (IsCompact.elim_finite_subcover) reduces the cover {box_m} to a finite subcover, so f is determined by the finite union of coordinates ⋃ J_{m₀}; cofiltered domination (exists_dominating, folding IsCofiltered.min) collapses that finite set to one coordinate B. This mirrors GammaA.dense_gammaGenFamily.

• piMon_surjective: each limit projection π_A : Γ_A → Fin A.n is surjective (the universal generators map onto the markings A.q, which generate Fin A.n by admissibility — mirrors GammaA.map_evalAt_closure_eq_top).

• GammaA_map_to_finite_factors: transport the single-coordinate factorization to Γ_A, then lift φ over the surjection π_A with MonoidHom.liftOfSurjective (kernel containment ker π_A ≤ ker φ holds because φ is constant on π_A-fibres). The lifted monoid hom is automatically continuous (Fin A.n discrete), giving the factoring morphism ψ.

Surjectivity of the limit projections

noncomputable def Q2Presentation.piMon (A : AdmissibleIndex) : ↑GammaA.toProfinite.toTop →* ↑(admissibleDiagram.obj A).toProfinite.toTop

The underlying monoid homomorphism of the limit projection π_A : Γ_A ⟶ Fin A.n.

Equations

• Q2Presentation.piMon A = (ProfiniteGrp.Hom.hom (CategoryTheory.Limits.limit.π Q2Presentation.admissibleDiagram A)).toMonoidHom

@[simp]

theorem Q2Presentation.piMon_apply (A : AdmissibleIndex) (x : ↑GammaA.toProfinite.toTop) : (piMon A) x = (ProfiniteGrp.Hom.hom (CategoryTheory.Limits.limit.π admissibleDiagram A)) x

theorem Q2Presentation.piMon_surjective (A : AdmissibleIndex) : Function.Surjective ⇑(piMon A)

Each limit projection π_A : Γ_A ⟶ Fin A.n is surjective.

The four universal generators gammaGen project to the markings A.q (gammaGen_eval_projection), which generate Fin A.n because A is admissible (A.admissible.1). Hence the image subgroup of π_A contains the whole group. This mirrors GammaA.map_evalAt_closure_eq_top.

Finite-coordinate factorization of continuous maps to a discrete space

theorem Q2Presentation.limit_finite_factor {H : Type u_1} [TopologicalSpace H] [DiscreteTopology H] (f : ↑(ProfiniteGrp.limit admissibleDiagram).toProfinite.toTop → H) (hf : Continuous f) : ∃ (A : AdmissibleIndex), ∀ (m m' : ↑(ProfiniteGrp.limit admissibleDiagram).toProfinite.toTop), ↑m A = ↑m' A → f m = f m'

A continuous map from the explicit inverse-limit model to a discrete space depends on a single coordinate.

Each fibre f⁻¹{f m} is open (H discrete), hence in the product topology contains a basic box fixing finitely many coordinates J m (isOpen_pi_iff), on which f is constant. These boxes form an open cover; compactness extracts a finite subcover, so f is constant on the (clopen) agreement-locus of the finite union of coordinates; cofiltered domination (exists_dominating) collapses that union to one coordinate B.

Mirrors GammaA.dense_gammaGenFamily.

The finite-factorization theorem

theorem Q2Presentation.GammaA_map_to_finite_factors {H : Type} [Group H] [Finite H] (φ : GammaA ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of H)) : ∃ (A : AdmissibleIndex) (ψ : admissibleDiagram.obj A ⟶ ProfiniteGrp.ofFiniteGrp (FiniteGrp.of H)), φ = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π admissibleDiagram A) ψ

Finite factorization (manuscript Lemma 2.2, plan §5 / work order B4).

Every continuous homomorphism φ : Γ_A ⟶ H to a finite group factors through one of the finite admissible quotients: there is an admissible index A and a (continuous) homomorphism ψ : Fin A.n ⟶ H with φ = π_A ≫ ψ.

The proof transports the single-coordinate factorization limit_finite_factor across the bridge gammaIso, then lifts φ over the surjection π_A (piMon_surjective) using MonoidHom.liftOfSurjective: the kernel containment ker π_A ≤ ker φ holds because φ is constant on π_A-fibres. The lifted monoid hom is continuous for free (Fin A.n is discrete), giving ψ.