`Π` is pro-`2`, and the supporting profinite-iso infrastructure (Stage C) #

This file isolates the Γ_A-independent part of Boundary/CandidatePro2.lean: the fact that the profinite pro-2 group Π = PiGrp is pro-2 (isProP2_PiGrp), together with the two reusable profinite tools it rests on:

profiniteGrpIsoOfBijective — a bijective continuous homomorphism of profinite groups is an isomorphism;
isProP2_of_iso — IsProP2 transports along a continuous isomorphism.

These were previously stated inside CandidatePro2.lean; they are factored out here so that the boundary package (Boundary/BoundaryPackage.lean, which is Γ-generic and must not depend on the candidate Γ_A) can consume isProP2_PiGrp without importing the Γ_A machinery. CandidatePro2.lean now imports this file.

The proof of isProP2_PiGrp is unchanged: Π is the inverse limit of the finite 2-groups Fin A.n, so its explicit limit model is pro-2 (isProP2_piModel, mirroring maxPro2_isProP2), and this transports to PiGrp along the bridge piCME.

A bijective continuous homomorphism of profinite groups is an isomorphism #

source

noncomputable def Q2Presentation.profiniteGrpIsoOfBijective {X Y : ProfiniteGrp.{u}} (g : X ⟶ Y) (hg : Function.Bijective ⇑(ProfiniteGrp.Hom.hom g)) :

X ≅ Y

A bijective morphism of profinite groups is an isomorphism: package it as a ContinuousMulEquiv (the inverse is continuous because the source is compact and the target Hausdorff) and apply ContinuousMulEquiv.toProfiniteGrpIso.

Equations

One or more equations did not get rendered due to their size.

Instances For

`IsProP2` transports along an isomorphism #

source

theorem Q2Presentation.isProP2_of_iso {P Q : ProfiniteGrp.{u}} (e : ↑P.toProfinite.toTop ≃ₜ* ↑Q.toProfinite.toTop) (h : IsProP2 Q) :

IsProP2 P

The pro-2 property transports along a continuous isomorphism of profinite groups: pushing an open normal subgroup U ⊴ P forward along e gives an open normal V ⊴ Q with P ⧸ U ≃* Q ⧸ V, and Q ⧸ V is a 2-group.

`Π` is pro-`2` #

source

theorem Q2Presentation.pi_model_exists_eval_ker_le (W : OpenNormalSubgroup ↑(ProfiniteGrp.limit piDiagram).toProfinite.toTop) :

∃ (A : PiMarkedFinite), (piEvalAt A).ker ≤ ↑W.toOpenSubgroup

Coordinate-kernel domination in the explicit limit model. Every open normal subgroup W of ProfiniteGrp.limit piDiagram contains the kernel of some coordinate evaluation piEvalAt A. Mirrors exists_coordProj_ker_le.

source

theorem Q2Presentation.isProP2_piModel :

IsProP2 (ProfiniteGrp.limit piDiagram)

The explicit limit model of Π is pro-2: every finite continuous quotient is a 2-group. Mirrors maxPro2_isProP2.

source

noncomputable def Q2Presentation.piMulEquiv :

↑PiGrp.toProfinite.toTop ≃* ↑(ProfiniteGrp.limit piDiagram).toProfinite.toTop

The bridge PiGrp ≃* (explicit limit model) underlying piIso.

Equations