The universal marking is admissible in the limit

Γ_A = F₄ ⧸ N_A (paper §2.1, eq. (7); GQ2/GammaA.lean) is the largest quotient of the free profinite group F₄ all of whose finite quotients are admissible. This file proves that the presentation data survives the limit — the three facts Prop 2.3 (Prop. 2.3) needs about Γ_A itself:

• relators die in the limit: tameRelator_mem_NA / wildRelator_mem_NA — the profinite relator words of the universal marking (relations (5)/(6)) lie in N_A, i.e. their images in Γ_A are 1 (quotientMk_tameRelator_eq_one / quotientMk_wildRelator_eq_one);
• the admissible opens are exactly the opens above N_A (isAdmissibleU_iff_NA_le) — the order-theoretic form of "Γ_A's finite quotients are the admissible quotients";
• the wild pair's closed normal closure is pro-2 in the limit (isProP_wildCore): the closed normal subgroup ⟨⟨x₀, x₁⟩⟩ ≤ Γ_A generated by the images of x₀, x₁ is a pro-2 group — the pro-2 condition of eq. (7) holds for Γ_A itself, not just for its finite quotients.

Design note: the limit argument

The engine is the directedness of the admissible family (the subdirect-closure content of paper Lemma 2.1, GQ2/Subdirect.lean), run through the same compactness pattern as GQ2/MaxProP.lean:

1. isAdmissibleU_top: the trivial quotient is admissible (all four conditions are trivial in a subsingleton), so the admissible family is nonempty — no appeal to the Appendix-B S₃ quotient is needed.
2. isAdmissibleU_inf: admissibility is closed under U ⊓ V. Generation holds in every finite quotient of F₄ (generates_univMarking_map — density of the abstract free group in its profinite completion); the relators die in U ⊓ V because they die in U and in V (this is where tameRelator_mem_of_isAdmissibleU recurs); and the 2-core condition passes to U ⊓ V subdirectly: an element of the normal closure in F₄ ⧸ U ⊓ V has a lift whose images in F₄ ⧸ U and F₄ ⧸ V are 2-elements, so it is a 2-element (isPGroup_normalClosure_image_inf, the elementwise form of "Q_A is closed under subdirect products", Lemma 2.1).
3. exists_isAdmissibleU_le: admissible domination — every open normal W ≥ N_A contains an admissible U. Compactness: the family {U ∩ Wᶜ} over admissible U is a directed (by 2) family of closed sets in the compact F₄; were all nonempty, their intersection would meet N_A ∩ Wᶜ = ∅. (Same pattern as isPGroup_quotient_of_proPKernel_le.)
4. isAdmissibleU_of_NA_le: push admissibility from the dominating U up to W along F₄ ⧸ U ↠ F₄ ⧸ W via Lemma 2.2 (Marking.map_admissible). With the trivial converse (N_A is an intersection) this gives the characterization isAdmissibleU_iff_NA_le.
5. isProP_wildCore: for an open normal V ≤ ⟨⟨x₀,x₁⟩⟩ (subspace topology), pick an open normal W ≤ Γ_A with W ∩ ⟨⟨x₀,x₁⟩⟩ ≤ V (Krull-style: V is a neighbourhood of 1); pull W back to an open normal Ŵ ≥ N_A of F₄, which is admissible by 4, so the normal closure of x₀, x₁ in F₄ ⧸ Ŵ is a 2-group; a dense-image argument (the image of ⟨⟨x₀,x₁⟩⟩ = closure M in the finite discrete Γ_A ⧸ W equals the image of the abstract normal closure M) then bounds every element of ⟨⟨x₀,x₁⟩⟩ ⧸ V by a 2-power.

Everything is deduced from the definition of N_A — no appeal to Γ_A ≅ lim machinery, and no new axioms (#print axioms = the standard three throughout).

Generation in every finite quotient

The four generators topologically generate F₄ (density of the abstract free group in its profinite completion), so their images generate every finite (discrete) quotient. This is the Generates clause of admissibility, for free, for every open normal subgroup.

theorem GQ2.closure_univMarking_eq_range_eta : Subgroup.closure {univMarking.σ, univMarking.τ, univMarking.x₀, univMarking.x₁} = (GrpCat.Hom.hom (ProfiniteGrp.ProfiniteCompletion.eta (GrpCat.of (FreeGroup (Fin 4))))).range

The subgroup generated by the universal marking is the (dense) image of the abstract free group FreeGroup (Fin 4) in its profinite completion.

theorem GQ2.generates_univMarking_map (W : OpenNormalSubgroup ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop) : (Marking.map (QuotientGroup.mk' ↑W.toOpenSubgroup) univMarking).Generates

Generation is automatic: the pushed universal marking generates every finite quotient F₄ ⧸ W (W open normal). Density of the free group in its completion + discreteness of the quotient.

The relator words lie in N_A (result (i))

Each admissible open normal U kills both relator words (the finite-level relations of IsAdmissibleU read back through the profinite⟺finite bridges of GQ2/GammaA.lean), so the words lie in the intersection N_A — i.e. relations (5) and (6) hold in Γ_A.

theorem GQ2.tameRelator_mem_of_isAdmissibleU {U : OpenNormalSubgroup ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop} (hU : IsAdmissibleU U) : univMarking.tameRelator ∈ ↑U.toOpenSubgroup

An admissible open normal subgroup contains the tame relator word (relation (5)).

theorem GQ2.wildRelator_mem_of_isAdmissibleU {U : OpenNormalSubgroup ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop} (hU : IsAdmissibleU U) : univMarking.wildRelator ∈ ↑U.toOpenSubgroup

An admissible open normal subgroup contains the wild relator word (relation (6)).

theorem GQ2.tameRelator_mem_NA : univMarking.tameRelator ∈ NA

The tame relator word lies in N_A — relation (5) holds in Γ_A (paper eq. (7)).

theorem GQ2.wildRelator_mem_NA : univMarking.wildRelator ∈ NA

The wild relator word lies in N_A — relation (6) holds in Γ_A (paper eq. (7)).

@[simp]

theorem GQ2.quotientMk_tameRelator_eq_one : (quotientMk NA) univMarking.tameRelator = 1

Relation (5) in Γ_A: the image of the tame relator word is trivial.

@[simp]

theorem GQ2.quotientMk_wildRelator_eq_one : (quotientMk NA) univMarking.wildRelator = 1

Relation (6) in Γ_A: the image of the wild relator word is trivial.

Directedness of the admissible family (Lemma 2.1 in the limit)

The admissible open normal subgroups form a directed family: the trivial quotient is admissible, and admissibility is closed under ⊓ (the subdirect-closure content of paper Lemma 2.1: F₄ ⧸ U ⊓ V is a subdirect product of F₄ ⧸ U and F₄ ⧸ V). Compactness then gives admissible domination: every open normal subgroup above N_A contains an admissible one, hence is itself admissible (Lemma 2.2 pushforward) — the admissible opens are exactly the opens above N_A.

theorem GQ2.isPGroup_normalClosure_image_inf {G : Type u_1} [Group G] {p : ℕ} (S : Set G) (A B : Subgroup G) [A.Normal] [B.Normal] (hA : IsPGroup p ↥(Subgroup.normalClosure (⇑(QuotientGroup.mk' A) '' S))) (hB : IsPGroup p ↥(Subgroup.normalClosure (⇑(QuotientGroup.mk' B) '' S))) : IsPGroup p ↥(Subgroup.normalClosure (⇑(QuotientGroup.mk' (A ⊓ B)) '' S))

Subdirect 2-core (Lemma 2.1, elementwise). If the normal closures of the image of S in G ⧸ A and in G ⧸ B are p-groups, so is the normal closure of the image of S in G ⧸ (A ⊓ B): any element lifts to n in the abstract normal closure of S, and n ^ p^i ∈ A, n ^ p^j ∈ B give n ^ p^(i+j) ∈ A ⊓ B.

theorem GQ2.isAdmissibleU_top : IsAdmissibleU (topOpenNormalSubgroup ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop)

The trivial quotient is admissible: all four clauses are trivial in a subsingleton. (Nonvacuity of the admissible family, with no appeal to the Appendix-B S₃ quotient.)

@[simp]

theorem GQ2.Marking.map_map {G : Type u_1} {H : Type u_2} {K : Type u_3} [Group G] [Group H] [Group K] (f : G →* H) (g : H →* K) (t : Marking G) : map g (map f t) = map (g.comp f) t

Pushing a marking along a composite is composing the pushes.

theorem GQ2.isAdmissibleU_inf {U V : OpenNormalSubgroup ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop} (hU : IsAdmissibleU U) (hV : IsAdmissibleU V) : IsAdmissibleU (U ⊓ V)

Admissibility is closed under intersections (Lemma 2.1, subdirect closure): the canonical quotient by U ⊓ V is a subdirect product of the quotients by U and by V, and each admissibility clause passes through.

theorem GQ2.exists_isAdmissibleU_le {W : OpenNormalSubgroup ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop} (hle : NA ≤ ↑W.toOpenSubgroup) : ∃ (U : OpenNormalSubgroup ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop), IsAdmissibleU U ∧ ↑U.toOpenSubgroup ≤ ↑W.toOpenSubgroup

Admissible domination. Every open normal subgroup of F₄ containing N_A contains an admissible open normal subgroup. (Compactness: were every admissible U ⊄ W, the directed family {U ∩ Wᶜ} of nonempty closed sets would have a common point, necessarily in N_A ∩ Wᶜ = ∅.)

theorem GQ2.isAdmissibleU_of_NA_le {W : OpenNormalSubgroup ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop} (hle : NA ≤ ↑W.toOpenSubgroup) : IsAdmissibleU W

Every open normal subgroup above N_A is itself admissible: push the marking forward from a dominating admissible U along F₄ ⧸ U ↠ F₄ ⧸ W (Lemma 2.2, Marking.map_admissible).

theorem GQ2.isAdmissibleU_iff_NA_le (U : OpenNormalSubgroup ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop) : IsAdmissibleU U ↔ NA ≤ ↑U.toOpenSubgroup

The admissible opens are exactly the opens above N_A — the order-theoretic form of "Γ_A = F₄ ⧸ N_A is the largest quotient all of whose finite quotients are admissible" (paper §2.1, eq. (7)). This is the interface Prop 2.3 (Prop. 2.3) consumes.

The wild pair's closed normal closure is pro-2 (result (ii))

The pro-2 clause of eq. (7) holds in the limit: the closed normal subgroup of Γ_A generated by the images of x₀, x₁ is a pro-2 group. Every open normal subgroup of it is trapped, via an open normal subgroup of Γ_A, by an admissible finite quotient of F₄, where the 2-core clause of admissibility bounds every element by a 2-power.

noncomputable def GQ2.wildCore : Subgroup (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NA)

The wild core of Γ_A: the closed normal closure ⟨⟨x₀, x₁⟩⟩ ≤ Γ_A of the images of the wild generators — the subgroup that paper eq. (7) requires to be pro-2. (Stated on the underlying quotient F₄ ⧸ N_A, to which GammaA is definitionally equal. The §3 layer's GQ2.SectionThree.wildPart is definitionally this subgroup, so isProP_wildCore etc. transfer verbatim; see GQ2/SectionThree.lean.)

Equations

• GQ2.wildCore = (Subgroup.normalClosure {(GQ2.quotientMk GQ2.NA) GQ2.univMarking.x₀, (GQ2.quotientMk GQ2.NA) GQ2.univMarking.x₁}).topologicalClosure

instance GQ2.wildCore_normal : wildCore.Normal

theorem GQ2.wildCore_isClosed : IsClosed ↑wildCore

theorem GQ2.isProP_wildCore : IsProP 2 ↥wildCore

The wild core is pro-2 (paper §2.1, the pro-2 clause of eq. (7), in the limit): every finite continuous quotient of ⟨⟨x₀, x₁⟩⟩ ≤ Γ_A is a 2-group.

The limit argument (see the module docstring): an open normal V ≤ wildCore contains W ∩ wildCore for some open normal W ≤ Γ_A; the pullback Ŵ ≤ F₄ of W contains N_A, so it is admissible (isAdmissibleU_of_NA_le), and its 2-core clause bounds the relevant elements: any m ∈ wildCore agrees modulo W with an element of the abstract normal closure (discreteness of Γ_A ⧸ W), whose lift to F₄ becomes a 2-element in F₄ ⧸ Ŵ.

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

• eq. (7) = ⟦eq-candidateinverse⟧
• Lemma 2.1 = ⟦lem-subdirect⟧
• Lemma 2.2 = ⟦lem-cofinal⟧
• Prop 2.3 = ⟦prop-epi-semantics⟧