Documentation

GQ2.Roe.AdmissibleLimit

The universal marking is R-admissible in the limit (Roe note Definition 1.1 ⟦def:GammaR⟧) #

Γ_R = F₄ ⧸ N_R (GQ2/Roe/GammaR.lean) is the largest quotient of the free profinite group F₄ all of whose finite quotients are R-admissible. This file is the Roe-candidate clone of GQ2/AdmissibleLimit.lean: it proves the three facts the Roe Prop. 2.3 (ticket R4) needs about Γ_R itself:

Design note #

The word-independent engine is reused verbatim from GQ2/AdmissibleLimit.lean (imported): the generation clause generates_univMarking_map, the subdirect 2-core lemma isPGroup_normalClosure_image_inf, and Marking.map_map are shared with Γ_A. Only the wild-relation-carrying and N_R/IsAdmissibleUR-carrying statements are re-derived here with an R suffix — the Roe bridge map_wildRelatorR_eq_one_iff (GQ2/Roe/GammaR.lean) replaces map_wildRelator_eq_one_iff, and map_admissibleR replaces map_admissible in the domination pushforward. No new axioms (#print axioms = the standard three throughout).

The relator words lie in N_R (result (i)) #

Each R-admissible open normal U kills both relator words (the finite-level relations of IsAdmissibleUR read back through the profinite⟺finite bridges — map_tameRelator_eq_one_iff of GQ2/GammaA.lean for the shared tame relation, map_wildRelatorR_eq_one_iff of GQ2/Roe/GammaR.lean for the Roe wild relation), so the words lie in the intersection N_R.

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

An R-admissible open normal subgroup contains the tame relator word.

source
theorem GQ2.wildRelatorR_mem_of_isAdmissibleUR {U : OpenNormalSubgroup ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop} (hU : IsAdmissibleUR U) :
univMarking.wildRelatorR ∈ ↑U.toOpenSubgroup

An R-admissible open normal subgroup contains the Roe wild relator word.

source
theorem GQ2.tameRelator_mem_NR :
univMarking.tameRelator ∈ NR

The tame relator word lies in N_R — the tame relation holds in Γ_R.

source
theorem GQ2.wildRelatorR_mem_NR :
univMarking.wildRelatorR ∈ NR

The Roe wild relator word lies in N_R — the Roe wild relation holds in Γ_R.

source
@[simp]
theorem GQ2.quotientMk_NR_tameRelator_eq_one :
(quotientMk NR) univMarking.tameRelator = 1

The tame relation in Γ_R: the image of the tame relator word is trivial.

source
@[simp]
theorem GQ2.quotientMk_wildRelatorR_eq_one :
(quotientMk NR) univMarking.wildRelatorR = 1

The Roe wild relation in Γ_R: the image of the Roe wild relator word is trivial.

Directedness of the R-admissible family (Roe Lemma 2.1 in the limit) #

The R-admissible open normal subgroups form a directed family: the trivial quotient is R-admissible, and R-admissibility is closed under ⊓. Compactness then gives R-admissible domination: every open normal subgroup above N_R contains an R-admissible one, hence is itself R-admissible — the R-admissible opens are exactly the opens above N_R.

source
theorem GQ2.isAdmissibleUR_top :
IsAdmissibleUR (topOpenNormalSubgroup ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop)

The trivial quotient is R-admissible: all four clauses are trivial in a subsingleton.

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

R-admissibility is closed under intersections (Roe Lemma 2.1, subdirect closure).

source
theorem GQ2.exists_isAdmissibleUR_le {W : OpenNormalSubgroup ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop} (hle : NR ≤ ↑W.toOpenSubgroup) :
∃ (U : OpenNormalSubgroup ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop), IsAdmissibleUR U ∧ ↑U.toOpenSubgroup ≤ ↑W.toOpenSubgroup

R-admissible domination. Every open normal subgroup of F₄ containing N_R contains an R-admissible open normal subgroup.

source
theorem GQ2.isAdmissibleUR_of_NR_le {W : OpenNormalSubgroup ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop} (hle : NR ≤ ↑W.toOpenSubgroup) :
IsAdmissibleUR W

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

source
theorem GQ2.isAdmissibleUR_iff_NR_le (U : OpenNormalSubgroup ↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop) :
IsAdmissibleUR U ↔ NR ≤ ↑U.toOpenSubgroup

The R-admissible opens are exactly the opens above N_R — the order-theoretic form of "Γ_R = F₄ ⧸ N_R is the largest quotient all of whose finite quotients are R-admissible". This is the interface the Roe Prop. 2.3 (ticket R4) consumes.

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

The pro-2 clause holds in the limit for Γ_R: the closed normal subgroup of Γ_R generated by the images of x₀, x₁ is a pro-2 group. Same limit argument as GQ2/AdmissibleLimit.lean, now routed through the R-admissible family.

source
noncomputable def GQ2.wildCoreR :
Subgroup (↑(FreeProfiniteGroup (Fin 4)).toProfinite.toTop ⧸ NR)

The wild core of Γ_R: the closed normal closure ⟨⟨x₀, x₁⟩⟩ ≤ Γ_R of the images of the wild generators — the subgroup that Definition 1.1 requires to be pro-2. Roe counterpart of GQ2.wildCore.

Equations
Instances For
    source
    instance GQ2.wildCoreR_normal :
    wildCoreR.Normal
    source
    theorem GQ2.wildCoreR_isClosed :
    IsClosed ↑wildCoreR
    source
    theorem GQ2.isProP_wildCoreR :
    IsProP 2 ↥wildCoreR

    The wild core is pro-2 (Definition 1.1's pro-2 clause, in the limit): every finite continuous quotient of ⟨⟨x₀, x₁⟩⟩ ≤ Γ_R is a 2-group. Roe counterpart of GQ2.isProP_wildCore; same limit argument (see the GQ2/AdmissibleLimit.lean module docstring), routed through the R-admissible family.

    Paper-tag ledger (Roe note paper/roe-presentation-verification.tex; hand-maintained) #