Topological finite generation, and Γ_A

main_presentation (GQ2/Statement.lean) consumes topological finite generation of its candidate group Γ_A in the shape ∃ s : Finset _, (Subgroup.closure ↑s).topologicalClosure = ⊤. This file discharges it for GQ2.GammaA, via two reusable facts:

• GQ2.isTopologicallyFinGen_freeProfiniteGroup — the free profinite group on a finite set is topologically finitely generated (its free generators' images topologically generate: the free group is dense in its profinite completion, ProfiniteGrp.ProfiniteCompletion.denseRange);
• GQ2.IsTopologicallyFinGen.of_surjective — topological finite generation passes along a continuous surjection (the image of a topological generating set topologically generates — DenseRange.topologicalClosure_map_subgroup), in particular to any profiniteQuotient.

Instantiating the second at the quotient projection F₄ ↠ F₄ ⧸ N_A = Γ_A gives GQ2.gammaA_topologicallyFinitelyGenerated, in exactly the form needed by main_presentation and main_presentation_literal.

No axioms: every result here is at the standard three (#print axioms).

def GQ2.IsTopologicallyFinGen (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Prop

A topological group is topologically finitely generated when some finite subset topologically generates it — i.e. the (algebraic) subgroup it generates is dense. This is the predicate main_presentation needs of Γ_A.

Equations

• GQ2.IsTopologicallyFinGen G = ∃ (s : Finset G), (Subgroup.closure ↑s).topologicalClosure = ⊤

theorem GQ2.IsTopologicallyFinGen.of_surjective {G : Type u_1} {Q : Type u_2} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [Group Q] [TopologicalSpace Q] [IsTopologicalGroup Q] (f : G →* Q) (hf : Continuous ⇑f) (hfs : Function.Surjective ⇑f) (hG : IsTopologicallyFinGen G) : IsTopologicallyFinGen Q

Topological finite generation passes along a continuous surjection. If f : G →* Q is continuous and surjective and G is topologically finitely generated, then so is Q (the images of a topological generating set topologically generate Q). In particular it passes to every profiniteQuotient.

theorem GQ2.isTopologicallyFinGen_freeProfiniteGroup {X : Type u} [Finite X] : IsTopologicallyFinGen ↑(FreeProfiniteGroup X).toProfinite.toTop

The free profinite group on a finite set is topologically finitely generated. The finite generating set is the image of the free generators under FreeProfiniteGroup.of; they topologically generate because the free group is dense in its profinite completion (ProfiniteGrp.ProfiniteCompletion.denseRange).

theorem GQ2.gammaA_isTopologicallyFinGen : IsTopologicallyFinGen ↑GammaA.toProfinite.toTop

Γ_A is topologically finitely generated (the predicate form).

theorem GQ2.gammaA_topologicallyFinitelyGenerated : ∃ (s : Finset ↑GammaA.toProfinite.toTop), (Subgroup.closure ↑s).topologicalClosure = ⊤

Γ_A is topologically finitely generated, in exactly the ∃ s : Finset _, … shape that GQ2.main_presentation consumes (used by the step-2 assembly main_presentation_literal, the literal-presentation proof).