The profinite pro-2 group Π and its unramified marking ν₂ (Stage C, work order C3)

This file realises the manuscript's maximal pro-2 quotient Π = ⟨σ, x₀, x₁ ∣ x₀^{σ²} x₀ [x₁,σ] = 1⟩_{pro-2} (reference/q2_manuscript.tex, Proposition 3.10 prop:pro2, lines ~962–995) as the cofiltered inverse limit, in ProfiniteGrp, of all finite marked pro-2 boundary quotients — exactly mirroring the Stage-C construction of the tame group Ttame in Boundary/Ttame.lean, but with the 3-generator pro-2 marking (σ, x₀, x₁) (carrying the 2-group side condition) in place of the 2-generator tame marking (s, t).

The finite index objects PiMarkedFinite, their morphisms PiHom, the index category and PiHom_ext are reused from Boundary/Nielsen.lean (work order C4); this file only adds the cofiltered structure on that category and the inverse-limit construction on top of it.

Main contents:

• IsCofiltered PiMarkedFinite — binary subdirect objects (piSubdirectObj) plus the subsingleton hom-sets (PiHom_ext) make the index category cofiltered.
• piDiagram : PiMarkedFinite ⥤ ProfiniteGrp, PiGrp := Limits.limit piDiagram, the bridge piIso / PiGrp_ext, the universal generators piSigma, piX0, piX1 : PiGrp, their projection-eval lemmas, the coordinatewise boundary relation PiGrp_piRel, and dense generation piGen_topologically_generate.
• nu_2 : PiGrp ⟶ ProfiniteZ2 — the unramified character σ ↦ 1, x₀ ↦ 0, x₁ ↦ 0 (eq:nu2). In a pro-2 group the wild generators x₀, x₁ are killed in the unramified quotient; only the procyclic σ-direction survives. Built as the map into ℤ₂ = lim_n ZMod(2ⁿ) whose n-th layer is the projection of PiGrp through the auxiliary cyclic-2-group boundary quotient cyclicPi n (carrier C2Pow n, σ = additive generator, x₀ = x₁ = 1).

Instance gotcha (inherited from AdmissibleIndex.lean / Nielsen.lean)

Fin n carries the global Fin.instMul, not the transported group structure A.groupFin. We thread A.groupFin explicitly (@, letI, projection access) through every Fin-level construction so Fin.instMul is never synthesized.

Generic transport lemmas (no Fin.instMul)

theorem Q2Presentation.map_rconj {G : Type u_1} {H : Type u_2} [Group G] [Group H] {F : Type u_3} [FunLike F G H] [MonoidHomClass F G H] (f : F) (x g : G) : f (rconj x g) = rconj (f x) (f g)

Right conjugation commutes with any monoid homomorphism.

theorem Q2Presentation.map_commutatorW {G : Type u_1} {H : Type u_2} [Group G] [Group H] {F : Type u_3} [FunLike F G H] [MonoidHomClass F G H] (f : F) (x y : G) : f (commutatorW x y) = commutatorW (f x) (f y)

The commutator word commutes with any monoid homomorphism.

theorem Q2Presentation.pi_generates_transport {G : Type u_1} {H : Type u_2} [Group G] [Group H] (e : G ≃* H) {sigma x0 x1 : G} (hgen : Subgroup.closure {sigma, x0, x1} = ⊤) : Subgroup.closure {e sigma, e x0, e x1} = ⊤

Generation transports along a multiplicative equivalence (3 generators).

theorem Q2Presentation.pi_relation_transport {G : Type u_1} {H : Type u_2} [Group G] [Group H] (e : G ≃* H) {sigma x0 x1 : G} (hrel : rconj x0 (sigma ^ 2) * x0 * commutatorW x1 sigma = 1) : rconj (e x0) (e sigma ^ 2) * e x0 * commutatorW (e x1) (e sigma) = 1

The pro-2 boundary relation transports along a multiplicative equivalence.

theorem Q2Presentation.isPGroup_two_pi {ι : Type u_1} [Fintype ι] {G : ι → Type u_2} [(i : ι) → Group (G i)] [∀ (i : ι), Finite (G i)] (h : ∀ (i : ι), IsPGroup 2 (G i)) : IsPGroup 2 ((i : ι) → G i)

IsPGroup p transports to a finite product over a Fintype index.

Skeletalization of an arbitrary pro-2 boundary-marked finite group

noncomputable def Q2Presentation.piSkeletalize (G : Type u_1) [Group G] [Finite G] [Nonempty G] (hG2 : IsPGroup 2 G) (sigma x0 x1 : G) (hgen : Subgroup.closure {sigma, x0, x1} = ⊤) (hrel : rconj x0 (sigma ^ 2) * x0 * commutatorW x1 sigma = 1) : PiMarkedFinite

Skeletalization. Any boundary marking (σ, x₀, x₁) of an arbitrary nonempty finite 2-group G is realised by a PiMarkedFinite on Fin (Nat.card G), transporting G's group structure along Finite.equivFin G (mirrors tameSkeletalize).

Equations

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

noncomputable def Q2Presentation.piSkelEquiv (G : Type u_1) [Group G] [Finite G] [Nonempty G] (hG2 : IsPGroup 2 G) (sigma x0 x1 : G) (hgen : Subgroup.closure {sigma, x0, x1} = ⊤) (hrel : rconj x0 (sigma ^ 2) * x0 * commutatorW x1 sigma = 1) : Fin (piSkeletalize G hG2 sigma x0 x1 hgen hrel).n ≃* G

The transport equivalence underlying piSkeletalize, as a MulEquiv Fin (piSkeletalize …).n ≃* G (mirrors tameSkelEquiv).

Equations

• Q2Presentation.piSkelEquiv G hG2 sigma x0 x1 hgen hrel = (Finite.equivFin G).symm.mulEquiv

@[simp]

theorem Q2Presentation.piSkelEquiv_sigma {G : Type u_1} [Group G] [Finite G] [Nonempty G] {hG2 : IsPGroup 2 G} {sigma x0 x1 : G} {hgen : Subgroup.closure {sigma, x0, x1} = ⊤} {hrel : rconj x0 (sigma ^ 2) * x0 * commutatorW x1 sigma = 1} : (piSkelEquiv G hG2 sigma x0 x1 hgen hrel) (piSkeletalize G hG2 sigma x0 x1 hgen hrel).sigma = sigma

@[simp]

theorem Q2Presentation.piSkelEquiv_x0 {G : Type u_1} [Group G] [Finite G] [Nonempty G] {hG2 : IsPGroup 2 G} {sigma x0 x1 : G} {hgen : Subgroup.closure {sigma, x0, x1} = ⊤} {hrel : rconj x0 (sigma ^ 2) * x0 * commutatorW x1 sigma = 1} : (piSkelEquiv G hG2 sigma x0 x1 hgen hrel) (piSkeletalize G hG2 sigma x0 x1 hgen hrel).x0 = x0

@[simp]

theorem Q2Presentation.piSkelEquiv_x1 {G : Type u_1} [Group G] [Finite G] [Nonempty G] {hG2 : IsPGroup 2 G} {sigma x0 x1 : G} {hgen : Subgroup.closure {sigma, x0, x1} = ⊤} {hrel : rconj x0 (sigma ^ 2) * x0 * commutatorW x1 sigma = 1} : (piSkelEquiv G hG2 sigma x0 x1 hgen hrel) (piSkeletalize G hG2 sigma x0 x1 hgen hrel).x1 = x1

The morphism-out and morphism-between constructors

noncomputable def Q2Presentation.piSkeletalizeHomOut {G : Type u_1} [Group G] [Finite G] [Nonempty G] {hG2 : IsPGroup 2 G} {sigma x0 x1 : G} {hgen : Subgroup.closure {sigma, x0, x1} = ⊤} {hrel : rconj x0 (sigma ^ 2) * x0 * commutatorW x1 sigma = 1} {D : PiMarkedFinite} (ψ : G →* Fin D.n) (hψsigma : ψ sigma = D.sigma) (hψx0 : ψ x0 = D.x0) (hψx1 : ψ x1 = D.x1) : PiHom (piSkeletalize G hG2 sigma x0 x1 hgen hrel) D

A marking-preserving hom ψ : G →* Fin D.n out of G induces a Π morphism piSkeletalize G … ⟶ D (mirrors tameSkeletalizeHomOut).

Equations

• Q2Presentation.piSkeletalizeHomOut ψ hψsigma hψx0 hψx1 = { toMonoidHom := ψ.comp (Q2Presentation.piSkelEquiv G hG2 sigma x0 x1 hgen hrel).toMonoidHom, map_sigma := ⋯, map_x0 := ⋯, map_x1 := ⋯ }

noncomputable def Q2Presentation.piSkelHomBetween {G : Type u_1} {H : Type u_2} [Group G] [Finite G] [Nonempty G] [Group H] [Finite H] [Nonempty H] {hG2 : IsPGroup 2 G} {sG x0G x1G : G} {hgG : Subgroup.closure {sG, x0G, x1G} = ⊤} {hrG : rconj x0G (sG ^ 2) * x0G * commutatorW x1G sG = 1} {hH2 : IsPGroup 2 H} {sH x0H x1H : H} {hgH : Subgroup.closure {sH, x0H, x1H} = ⊤} {hrH : rconj x0H (sH ^ 2) * x0H * commutatorW x1H sH = 1} (φ : G →* H) (hs : φ sG = sH) (h0 : φ x0G = x0H) (h1 : φ x1G = x1H) : piSkeletalize G hG2 sG x0G x1G hgG hrG ⟶ piSkeletalize H hH2 sH x0H x1H hgH hrH

A marking-preserving group hom φ : G →* H between two boundary-marked groups induces a Π morphism of their skeletalizations. Stated with both G, H generic so the target skeleton MulOneClass is resolved (to groupFin) once in this generic context, never Fin.instMul (mirrors tameSkelHomBetween).

Equations

• Q2Presentation.piSkelHomBetween φ hs h0 h1 = Q2Presentation.piSkeletalizeHomOut ((Q2Presentation.piSkelEquiv H hH2 sH x0H x1H hgH hrH).symm.toMonoidHom.comp φ) ⋯ ⋯ ⋯

theorem Q2Presentation.piSkelHomBetween_key {G : Type u_1} {H : Type u_2} [Group G] [Finite G] [Nonempty G] [Group H] [Finite H] [Nonempty H] {hG2 : IsPGroup 2 G} {sG x0G x1G : G} {hgG : Subgroup.closure {sG, x0G, x1G} = ⊤} {hrG : rconj x0G (sG ^ 2) * x0G * commutatorW x1G sG = 1} {hH2 : IsPGroup 2 H} {sH x0H x1H : H} {hgH : Subgroup.closure {sH, x0H, x1H} = ⊤} {hrH : rconj x0H (sH ^ 2) * x0H * commutatorW x1H sH = 1} (φ : G →* H) (hs : φ sG = sH) (h0 : φ x0G = x0H) (h1 : φ x1G = x1H) (y : Fin (piSkeletalize G hG2 sG x0G x1G hgG hrG).n) : (piSkelEquiv H hH2 sH x0H x1H hgH hrH) ((piSkelHomBetween φ hs h0 h1).toMonoidHom y) = φ ((piSkelEquiv G hG2 sG x0G x1G hgG hrG) y)

The induced morphism intertwines the transport equivalences with φ.

Nonemptiness: the trivial pro-2 boundary quotient

theorem Q2Presentation.pi_trivial_generates : Subgroup.closure {1, 1, 1} = ⊤

theorem Q2Presentation.pi_trivial_rel : rconj 1 (1 ^ 2) * 1 * commutatorW 1 1 = 1

theorem Q2Presentation.pi_trivial_isTwoGroup : IsPGroup 2 Unit

noncomputable def Q2Presentation.trivialPi : PiMarkedFinite

The trivial pro-2 boundary index (carrier Fin 1).

Equations

• Q2Presentation.trivialPi = Q2Presentation.piSkeletalize Unit Q2Presentation.pi_trivial_isTwoGroup 1 1 1 Q2Presentation.pi_trivial_generates Q2Presentation.pi_trivial_rel

instance Q2Presentation.instNonemptyPiMarkedFinite : Nonempty PiMarkedFinite

Binary subdirect objects

def Q2Presentation.piFamilySubgroup {ι : Type u_1} {G : ι → Type u_2} [(i : ι) → Group (G i)] (sigma x0 x1 : (i : ι) → G i) : Subgroup ((i : ι) → G i)

The subgroup of ∀ i, G i generated by the diagonal triple (σ, x₀, x₁).

Equations

• Q2Presentation.piFamilySubgroup sigma x0 x1 = Subgroup.closure {sigma, x0, x1}

def Q2Presentation.piFamilyS {ι : Type u_1} {G : ι → Type u_2} [(i : ι) → Group (G i)] (sigma x0 x1 : (i : ι) → G i) : ↥(piFamilySubgroup sigma x0 x1)

The corestricted diagonal σ.

Equations

• Q2Presentation.piFamilyS sigma x0 x1 = ⟨sigma, ⋯⟩

def Q2Presentation.piFamilyX0 {ι : Type u_1} {G : ι → Type u_2} [(i : ι) → Group (G i)] (sigma x0 x1 : (i : ι) → G i) : ↥(piFamilySubgroup sigma x0 x1)

The corestricted diagonal x₀.

Equations

• Q2Presentation.piFamilyX0 sigma x0 x1 = ⟨x0, ⋯⟩

def Q2Presentation.piFamilyX1 {ι : Type u_1} {G : ι → Type u_2} [(i : ι) → Group (G i)] (sigma x0 x1 : (i : ι) → G i) : ↥(piFamilySubgroup sigma x0 x1)

The corestricted diagonal x₁.

Equations

• Q2Presentation.piFamilyX1 sigma x0 x1 = ⟨x1, ⋯⟩

theorem Q2Presentation.piFamily_generates {ι : Type u_1} {G : ι → Type u_2} [(i : ι) → Group (G i)] (sigma x0 x1 : (i : ι) → G i) : Subgroup.closure {piFamilyS sigma x0 x1, piFamilyX0 sigma x0 x1, piFamilyX1 sigma x0 x1} = ⊤

theorem Q2Presentation.piFamily_rel {ι : Type u_1} {G : ι → Type u_2} [(i : ι) → Group (G i)] (sigma x0 x1 : (i : ι) → G i) (h : ∀ (i : ι), rconj (x0 i) (sigma i ^ 2) * x0 i * commutatorW (x1 i) (sigma i) = 1) : rconj (piFamilyX0 sigma x0 x1) (piFamilyS sigma x0 x1 ^ 2) * piFamilyX0 sigma x0 x1 * commutatorW (piFamilyX1 sigma x0 x1) (piFamilyS sigma x0 x1) = 1

def Q2Presentation.piBinSigma (A B : PiMarkedFinite) (i : Fin 2) : Fin (![A, B] i).n

The σ-component of the binary subdirect family of A, B.

Equations

• Q2Presentation.piBinSigma A B i = (![A, B] i).sigma

def Q2Presentation.piBinX0 (A B : PiMarkedFinite) (i : Fin 2) : Fin (![A, B] i).n

The x₀-component of the binary subdirect family of A, B.

Equations

• Q2Presentation.piBinX0 A B i = (![A, B] i).x0

def Q2Presentation.piBinX1 (A B : PiMarkedFinite) (i : Fin 2) : Fin (![A, B] i).n

The x₁-component of the binary subdirect family of A, B.

Equations

• Q2Presentation.piBinX1 A B i = (![A, B] i).x1

theorem Q2Presentation.piSubdirect_isTwoGroup (A B : PiMarkedFinite) : IsPGroup 2 ↥(piFamilySubgroup (piBinSigma A B) (piBinX0 A B) (piBinX1 A B))

The 2-group certificate for the binary subdirect subgroup of A, B.

noncomputable def Q2Presentation.piSubdirectObj (A B : PiMarkedFinite) : PiMarkedFinite

The binary subdirect object of A, B: skeletalize the subgroup of ∏ Fin (![A,B] i).n generated by the diagonal (σ, x₀, x₁), which is a 2-group and satisfies the boundary relation coordinatewise.

Equations

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

noncomputable def Q2Presentation.piSubdirectFst (A B : PiMarkedFinite) : piSubdirectObj A B ⟶ A

First projection of the binary subdirect object.

Equations

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

noncomputable def Q2Presentation.piSubdirectSnd (A B : PiMarkedFinite) : piSubdirectObj A B ⟶ B

Second projection of the binary subdirect object.

Equations

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

instance Q2Presentation.piMarkedFinite_isCofiltered : CategoryTheory.IsCofiltered PiMarkedFinite

The pro-2 boundary index category is cofiltered.

The pro-2 inverse system and its limit PiGrp

noncomputable def Q2Presentation.piDiagram : CategoryTheory.Functor PiMarkedFinite ProfiniteGrp.{0}

The inverse system of finite marked pro-2 boundary quotients, as a functor into ProfiniteGrp (mirrors tameDiagram).

Equations

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

@[simp]

theorem Q2Presentation.piDiagram_map_apply {A B : PiMarkedFinite} (f : A ⟶ B) (x : Fin A.n) : (ProfiniteGrp.Hom.hom (piDiagram.map f)) x = f.toMonoidHom x

instance Q2Presentation.instFinitePiObj (A : PiMarkedFinite) : Finite ↑(piDiagram.obj A).toProfinite.toTop

noncomputable def Q2Presentation.PiGrp : ProfiniteGrp.{0}

The profinite pro-2 group Π, the cofiltered inverse limit (in ProfiniteGrp) of all finite marked pro-2 boundary quotients (manuscript Π, eq:Pi). Named PiGrp to avoid clashing with Lean's Pi dependent-function type.

Equations

• Q2Presentation.PiGrp = CategoryTheory.Limits.limit Q2Presentation.piDiagram

noncomputable def Q2Presentation.piIso : PiGrp ≅ ProfiniteGrp.limit piDiagram

Bridge from the opaque categorical limit to mathlib's explicit subtype model.

Equations

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

theorem Q2Presentation.pi_limit_pi_apply (A : PiMarkedFinite) (x : ↑PiGrp.toProfinite.toTop) : (ProfiniteGrp.Hom.hom (CategoryTheory.Limits.limit.π piDiagram A)) x = ↑((ProfiniteGrp.Hom.hom piIso.hom) x) A

The categorical projection PiGrp ⟶ Fin A.n, via piIso.

theorem Q2Presentation.PiGrp_ext {x y : ↑PiGrp.toProfinite.toTop} (h : ∀ (A : PiMarkedFinite), (ProfiniteGrp.Hom.hom (CategoryTheory.Limits.limit.π piDiagram A)) x = (ProfiniteGrp.Hom.hom (CategoryTheory.Limits.limit.π piDiagram A)) y) : x = y

Two points of PiGrp agree once all coordinate projections agree.

The universal generators σ, x₀, x₁

def Q2Presentation.piGenSigmaFamily : ↑(ProfiniteGrp.limit piDiagram).toProfinite.toTop

The compatible family underlying σ: coordinate A.sigma at every A.

Equations

• Q2Presentation.piGenSigmaFamily = ⟨fun (A : Q2Presentation.PiMarkedFinite) => A.sigma, ⋯⟩

def Q2Presentation.piGenX0Family : ↑(ProfiniteGrp.limit piDiagram).toProfinite.toTop

The compatible family underlying x₀: coordinate A.x0 at every A.

Equations

• Q2Presentation.piGenX0Family = ⟨fun (A : Q2Presentation.PiMarkedFinite) => A.x0, ⋯⟩

def Q2Presentation.piGenX1Family : ↑(ProfiniteGrp.limit piDiagram).toProfinite.toTop

The compatible family underlying x₁: coordinate A.x1 at every A.

Equations

• Q2Presentation.piGenX1Family = ⟨fun (A : Q2Presentation.PiMarkedFinite) => A.x1, ⋯⟩

noncomputable def Q2Presentation.piSigma : ↑PiGrp.toProfinite.toTop

The universal generator σ of PiGrp.

Equations

• Q2Presentation.piSigma = (ProfiniteGrp.Hom.hom Q2Presentation.piIso.inv) Q2Presentation.piGenSigmaFamily

noncomputable def Q2Presentation.piX0 : ↑PiGrp.toProfinite.toTop

The universal generator x₀ of PiGrp.

Equations

• Q2Presentation.piX0 = (ProfiniteGrp.Hom.hom Q2Presentation.piIso.inv) Q2Presentation.piGenX0Family

noncomputable def Q2Presentation.piX1 : ↑PiGrp.toProfinite.toTop

The universal generator x₁ of PiGrp.

Equations

• Q2Presentation.piX1 = (ProfiniteGrp.Hom.hom Q2Presentation.piIso.inv) Q2Presentation.piGenX1Family

theorem Q2Presentation.piSigma_eval (A : PiMarkedFinite) : (ProfiniteGrp.Hom.hom (CategoryTheory.Limits.limit.π piDiagram A)) piSigma = A.sigma

Projecting σ to a coordinate returns A.sigma.

theorem Q2Presentation.piX0_eval (A : PiMarkedFinite) : (ProfiniteGrp.Hom.hom (CategoryTheory.Limits.limit.π piDiagram A)) piX0 = A.x0

Projecting x₀ to a coordinate returns A.x0.

theorem Q2Presentation.piX1_eval (A : PiMarkedFinite) : (ProfiniteGrp.Hom.hom (CategoryTheory.Limits.limit.π piDiagram A)) piX1 = A.x1

Projecting x₁ to a coordinate returns A.x1.

theorem Q2Presentation.PiGrp_piRel (A : PiMarkedFinite) : rconj ((ProfiniteGrp.Hom.hom (CategoryTheory.Limits.limit.π piDiagram A)) piX0) ((ProfiniteGrp.Hom.hom (CategoryTheory.Limits.limit.π piDiagram A)) piSigma ^ 2) * (ProfiniteGrp.Hom.hom (CategoryTheory.Limits.limit.π piDiagram A)) piX0 * commutatorW ((ProfiniteGrp.Hom.hom (CategoryTheory.Limits.limit.π piDiagram A)) piX1) ((ProfiniteGrp.Hom.hom (CategoryTheory.Limits.limit.π piDiagram A)) piSigma) = 1

The pro-2 boundary relation holds in PiGrp (manuscript x₀^{σ²} x₀ [x₁,σ] = 1, eq:Pi), in the inverse-limit sense: projecting the universal generators to any finite boundary quotient A satisfies the relation there (because A does).

Topological generation

noncomputable def Q2Presentation.piHomeo : ↑PiGrp.toProfinite.toTop ≃ₜ ↑(ProfiniteGrp.limit piDiagram).toProfinite.toTop

PiGrp is homeomorphic to the explicit limit model via piIso.

Equations

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

noncomputable def Q2Presentation.piEvalAt (B : PiMarkedFinite) : ↑(ProfiniteGrp.limit piDiagram).toProfinite.toTop →* ↑(piDiagram.obj B).toProfinite.toTop

Evaluation at coordinate B, as a monoid hom out of the explicit limit.

Equations

• Q2Presentation.piEvalAt B = { toFun := fun (m : ↑(ProfiniteGrp.limit Q2Presentation.piDiagram).toProfinite.toTop) => ↑m B, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem Q2Presentation.piEvalAt_apply (B : PiMarkedFinite) (m : ↑(ProfiniteGrp.limit piDiagram).toProfinite.toTop) : (piEvalAt B) m = ↑m B

theorem Q2Presentation.map_piEvalAt_closure_eq_top (B : PiMarkedFinite) : Subgroup.map (piEvalAt B) (Subgroup.closure {piGenSigmaFamily, piGenX0Family, piGenX1Family}) = ⊤

The coordinate-B evaluation maps the subgroup generated by σ, x₀, x₁ onto Fin B.n (its image is closure {B.sigma, B.x0, B.x1} = ⊤, by B.generates).

theorem Q2Presentation.pi_exists_dominating (J : Finset PiMarkedFinite) : ∃ (B : PiMarkedFinite), ∀ A ∈ J, Nonempty (B ⟶ A)

Finite cofiltered domination.

theorem Q2Presentation.dense_piGenFamily : Dense ↑(Subgroup.closure {piGenSigmaFamily, piGenX0Family, piGenX1Family})

The subgroup generated by σ, x₀, x₁ is dense in the explicit limit model.

theorem Q2Presentation.piGen_topologically_generate : (Subgroup.closure {piSigma, piX0, piX1}).topologicalClosure = ⊤

The universal generators σ, x₀, x₁ topologically generate PiGrp.

The unramified character nu_2 : PiGrp ⟶ ℤ₂

The unramified character sends σ to the topological generator 1 ∈ ℤ₂ and the wild generators x₀, x₁ to 0 (in a pro-2 group the wild inertia is killed in the unramified quotient — Prop 3.10 eq:nu2). It is built as the map into ℤ₂ = lim_n ZMod(2ⁿ) whose n-th layer is the projection of PiGrp through the auxiliary cyclic-2-group boundary quotient cyclicPi n (carrier C2Pow n, σ = additive generator, x₀ = x₁ = 1).

theorem Q2Presentation.cyclicPi_gen (n : ℕ) : Subgroup.closure {Multiplicative.ofAdd 1, 1, 1} = ⊤

The additive generator ofAdd 1 (together with 1, 1) generates the cyclic 2-group C2Pow n.

theorem Q2Presentation.cyclicPi_rel (n : ℕ) : rconj 1 (Multiplicative.ofAdd 1 ^ 2) * 1 * commutatorW 1 (Multiplicative.ofAdd 1) = 1

The boundary relation holds trivially in C2Pow n (x₀ = x₁ = 1).

theorem Q2Presentation.cyclicPi_isTwoGroup (n : ℕ) : IsPGroup 2 (C2Pow n)

C2Pow n is a 2-group.

noncomputable def Q2Presentation.cyclicPi (n : ℕ) : PiMarkedFinite

The auxiliary cyclic 2-group boundary quotient at layer n: carrier C2Pow n, σ = additive generator, x₀ = x₁ = 1.

Equations

• Q2Presentation.cyclicPi n = Q2Presentation.piSkeletalize (Q2Presentation.C2Pow n) ⋯ (Multiplicative.ofAdd 1) 1 1 ⋯ ⋯

noncomputable def Q2Presentation.cyclicPiEquiv (n : ℕ) : Fin (cyclicPi n).n ≃* C2Pow n

The transport equivalence Fin (cyclicPi n).n ≃* C2Pow n.

Equations

• Q2Presentation.cyclicPiEquiv n = Q2Presentation.piSkelEquiv (Q2Presentation.C2Pow n) ⋯ (Multiplicative.ofAdd 1) 1 1 ⋯ ⋯

@[simp]

theorem Q2Presentation.cyclicPiEquiv_sigma (n : ℕ) : (cyclicPiEquiv n) (cyclicPi n).sigma = Multiplicative.ofAdd 1

@[simp]

theorem Q2Presentation.cyclicPiEquiv_x0 (n : ℕ) : (cyclicPiEquiv n) (cyclicPi n).x0 = 1

@[simp]

theorem Q2Presentation.cyclicPiEquiv_x1 (n : ℕ) : (cyclicPiEquiv n) (cyclicPi n).x1 = 1

theorem Q2Presentation.castCMH_ofAddOne {a b : ℕ} (h : 2 ^ a ∣ 2 ^ b) : (castCMH h) (Multiplicative.ofAdd 1) = Multiplicative.ofAdd 1

Reduction maps fix the additive generator ofAdd 1.

noncomputable def Q2Presentation.piLayerHom (n : ℕ) : ↑PiGrp.toProfinite.toTop →* C2Pow n

The n-th unramified layer hom PiGrp →* C2Pow n: project to the auxiliary cyclic quotient cyclicPi n and read off the additive coordinate.

Equations

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

theorem Q2Presentation.piLayer_continuous (n : ℕ) : Continuous ⇑(piLayerHom n)

noncomputable def Q2Presentation.redHomPi (n m : ℕ) (hmn : m ≤ n) : cyclicPi n ⟶ cyclicPi m

The reduction Π morphism cyclicPi n ⟶ cyclicPi m for m ≤ n, underlying the ℤ₂-layer maps ZMod(2ⁿ) → ZMod(2ᵐ).

Equations

• Q2Presentation.redHomPi n m hmn = Q2Presentation.piSkelHomBetween (Q2Presentation.castCMH ⋯).toMonoidHom ⋯ ⋯ ⋯

theorem Q2Presentation.redHomPi_key (n m : ℕ) (hmn : m ≤ n) (y : Fin (cyclicPi n).n) : (cyclicPiEquiv m) ((redHomPi n m hmn).toMonoidHom y) = (castCMH ⋯) ((cyclicPiEquiv n) y)

The reduction morphism intertwines the transport equivalences with the ℤ₂-layer reduction.

theorem Q2Presentation.piLayer_compat (n m : ℕ) (hmn : m ≤ n) (x : ↑PiGrp.toProfinite.toTop) : (castCMH ⋯) ((piLayerHom n) x) = (piLayerHom m) x

Layer compatibility: reducing the n-th layer to the m-th agrees with the m-th layer (m ≤ n). Uses the inverse-limit compatibility of PiGrp through redHomPi.

noncomputable def Q2Presentation.nu_2 : PiGrp ⟶ ProfiniteZ2

The unramified character ν₂ : PiGrp ⟶ ℤ₂, σ ↦ 1, x₀ ↦ 0, x₁ ↦ 0. Built as the map into ℤ₂ = lim_n ZMod(2ⁿ) whose n-th coordinate is piLayerHom n.

Equations

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

nu_2 is the unramified character: σ ↦ 1, x₀ ↦ 0, x₁ ↦ 0

theorem Q2Presentation.piLayerHom_piSigma (n : ℕ) : (piLayerHom n) piSigma = Multiplicative.ofAdd 1

theorem Q2Presentation.piLayerHom_piX0 (n : ℕ) : (piLayerHom n) piX0 = 1

theorem Q2Presentation.piLayerHom_piX1 (n : ℕ) : (piLayerHom n) piX1 = 1

theorem Q2Presentation.nu_2_piSigma : (ProfiniteGrp.Hom.hom nu_2) piSigma = z2One

ν₂ sends σ to the topological generator 1 ∈ ℤ₂ (the unramified Frobenius coordinate).

theorem Q2Presentation.nu_2_piX0 : (ProfiniteGrp.Hom.hom nu_2) piX0 = z2Zero

ν₂ sends x₀ to 0 ∈ ℤ₂ (the wild generator is killed in the unramified pro-2 quotient — Prop 3.10).

theorem Q2Presentation.nu_2_piX1 : (ProfiniteGrp.Hom.hom nu_2) piX1 = z2Zero

ν₂ sends x₁ to 0 ∈ ℤ₂ (the wild generator is killed in the unramified pro-2 quotient — Prop 3.10).