The profinite Demushkin group D0 (Stage C, work order C4)

This file realises the manuscript's standard rank-three dyadic Demushkin group D₀ = ⟨a, s, y ∣ a² s⁴ [s,y] = 1⟩_{pro-2} (reference/q2_manuscript.tex, l.208, Proposition prop:markedDem; equivalently the HNN form Y⁻¹SY = T = S⁻³A⁻², l.814, eq:D0HNN) as the cofiltered inverse limit, in ProfiniteGrp, of all finite marked Demushkin 2-group quotients — exactly mirroring the Stage-C construction of Ttame in Boundary/Ttame.lean, but with the 3-generator Demushkin marking (a, s, y) and the defining relation a² s⁴ [s,y] = 1 in place of the 2-generator tame marking (s, t) with τ^σ = τ².

The finite index objects D0MarkedFinite, their morphisms D0Hom, the category, D0Hom_ext, and D0Iso are reused from Boundary/Nielsen.lean (work order C4, the Nielsen-transform file). This file adds the limit-theoretic content:

• skeletalization of an arbitrary Demushkin-marked finite 2-group (d0Skeletalize, d0SkelEquiv, d0SkeletalizeHomOut, d0SkelHomBetween);
• the trivial object and binary subdirect objects, giving IsCofiltered D0MarkedFinite;
• d0Diagram : D0MarkedFinite ⥤ ProfiniteGrp, D0 := Limits.limit d0Diagram, the bridge d0Iso to mathlib's explicit subtype model and D0_ext;
• the universal generators d0A, d0S, d0Y : D0, their projection-eval lemmas, the coordinatewise Demushkin relation D0_rel, and dense generation d0Gen_topologically_generate.

Deferred: D0 ≅ PiGrp

The profinite Nielsen comparison D0 ≅ PiGrp (manuscript Cor. 3.12, cor:relativeDemushkin) is deferred to a follow-up file: it will follow from Nielsen's categorical equivalence D0_Pi_index_equiv : D0MarkedFinite ≌ PiMarkedFinite together with limit functoriality, once the parallel Boundary/PiGroup.lean (PiGrp := Limits.limit piDiagram) is available. We do not import PiGroup.lean here.

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

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

Generic transport lemmas (no Fin.instMul)

theorem Q2Presentation.commutatorW_map {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.d0_gen3_transport {G : Type u_1} {H : Type u_2} [Group G] [Group H] (e : G ≃* H) {a s y : G} (hgen : Gen3 a s y) : Gen3 (e a) (e s) (e y)

A three-generator generation transports along a multiplicative equivalence.

theorem Q2Presentation.d0_rel_transport {G : Type u_1} {H : Type u_2} [Group G] [Group H] (e : G ≃* H) {a s y : G} (hrel : D0Relator a s y) : D0Relator (e a) (e s) (e y)

The standard Demushkin relator a² s⁴ [s,y] = 1 transports along a multiplicative equivalence.

Skeletalization of an arbitrary Demushkin-marked finite 2-group

noncomputable def Q2Presentation.d0Skeletalize (G : Type u_1) [Group G] [Finite G] [Nonempty G] (a s y : G) (hgen : Gen3 a s y) (hrel : D0Relator a s y) (hp : IsPGroup 2 G) : D0MarkedFinite

Skeletalization. Any Demushkin marking (a, s, y) of an arbitrary nonempty finite 2-group G is realised by a D0MarkedFinite on Fin (Nat.card G), transporting G's group structure along Finite.equivFin G (mirrors tameSkeletalize, with the extra IsPGroup 2 field).

Equations

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

noncomputable def Q2Presentation.d0SkelEquiv (G : Type u_1) [Group G] [Finite G] [Nonempty G] (a s y : G) (hgen : Gen3 a s y) (hrel : D0Relator a s y) (hp : IsPGroup 2 G) : Fin (d0Skeletalize G a s y hgen hrel hp).n ≃* G

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

Equations

• Q2Presentation.d0SkelEquiv G a s y hgen hrel hp = (Finite.equivFin G).symm.mulEquiv

@[simp]

theorem Q2Presentation.d0SkelEquiv_a {G : Type u_1} [Group G] [Finite G] [Nonempty G] {a s y : G} {hgen : Gen3 a s y} {hrel : D0Relator a s y} {hp : IsPGroup 2 G} : (d0SkelEquiv G a s y hgen hrel hp) (d0Skeletalize G a s y hgen hrel hp).a = a

@[simp]

theorem Q2Presentation.d0SkelEquiv_s {G : Type u_1} [Group G] [Finite G] [Nonempty G] {a s y : G} {hgen : Gen3 a s y} {hrel : D0Relator a s y} {hp : IsPGroup 2 G} : (d0SkelEquiv G a s y hgen hrel hp) (d0Skeletalize G a s y hgen hrel hp).s = s

@[simp]

theorem Q2Presentation.d0SkelEquiv_y {G : Type u_1} [Group G] [Finite G] [Nonempty G] {a s y : G} {hgen : Gen3 a s y} {hrel : D0Relator a s y} {hp : IsPGroup 2 G} : (d0SkelEquiv G a s y hgen hrel hp) (d0Skeletalize G a s y hgen hrel hp).y = y

noncomputable def Q2Presentation.d0SkeletalizeHomOut {G : Type u_1} [Group G] [Finite G] [Nonempty G] {a s y : G} {hgen : Gen3 a s y} {hrel : D0Relator a s y} {hp : IsPGroup 2 G} {D : D0MarkedFinite} (ψ : G →* Fin D.n) (hψa : ψ a = D.a) (hψs : ψ s = D.s) (hψy : ψ y = D.y) : D0Hom (d0Skeletalize G a s y hgen hrel hp) D

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

Equations

• Q2Presentation.d0SkeletalizeHomOut ψ hψa hψs hψy = { toMonoidHom := ψ.comp (Q2Presentation.d0SkelEquiv G a s y hgen hrel hp).toMonoidHom, map_a := ⋯, map_s := ⋯, map_y := ⋯ }

noncomputable def Q2Presentation.d0SkelHomBetween {G : Type u_1} {H : Type u_2} [Group G] [Finite G] [Nonempty G] [Group H] [Finite H] [Nonempty H] {aG sG yG : G} {hgG : Gen3 aG sG yG} {hrG : D0Relator aG sG yG} {hpG : IsPGroup 2 G} {aH sH yH : H} {hgH : Gen3 aH sH yH} {hrH : D0Relator aH sH yH} {hpH : IsPGroup 2 H} (φ : G →* H) (ha : φ aG = aH) (hs : φ sG = sH) (hy : φ yG = yH) : d0Skeletalize G aG sG yG hgG hrG hpG ⟶ d0Skeletalize H aH sH yH hgH hrH hpH

A marking-preserving group hom φ : G →* H between two Demushkin-marked 2-groups induces a D₀ 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.d0SkelHomBetween φ ha hs hy = Q2Presentation.d0SkeletalizeHomOut ((Q2Presentation.d0SkelEquiv H aH sH yH hgH hrH hpH).symm.toMonoidHom.comp φ) ⋯ ⋯ ⋯

Nonemptiness: the trivial Demushkin quotient

theorem Q2Presentation.d0_trivial_generates : Gen3 1 1 1

theorem Q2Presentation.d0_trivial_rel : D0Relator 1 1 1

theorem Q2Presentation.d0_trivial_isTwoGroup : IsPGroup 2 Unit

noncomputable def Q2Presentation.trivialD0 : D0MarkedFinite

The trivial Demushkin index (carrier Fin 1).

Equations

• Q2Presentation.trivialD0 = Q2Presentation.d0Skeletalize Unit 1 1 1 Q2Presentation.d0_trivial_generates Q2Presentation.d0_trivial_rel Q2Presentation.d0_trivial_isTwoGroup

instance Q2Presentation.instNonemptyD0MarkedFinite : Nonempty D0MarkedFinite

Binary subdirect objects

def Q2Presentation.d0FamilySubgroup {ι : Type u_1} {G : ι → Type u_2} [(i : ι) → Group (G i)] (a s y : (i : ι) → G i) : Subgroup ((i : ι) → G i)

The subgroup of ∀ i, G i generated by the diagonal triple (a, s, y).

Equations

• Q2Presentation.d0FamilySubgroup a s y = Subgroup.closure {a, s, y}

def Q2Presentation.d0FamilyA {ι : Type u_1} {G : ι → Type u_2} [(i : ι) → Group (G i)] (a s y : (i : ι) → G i) : ↥(d0FamilySubgroup a s y)

The corestricted diagonal a.

Equations

• Q2Presentation.d0FamilyA a s y = ⟨a, ⋯⟩

def Q2Presentation.d0FamilyS {ι : Type u_1} {G : ι → Type u_2} [(i : ι) → Group (G i)] (a s y : (i : ι) → G i) : ↥(d0FamilySubgroup a s y)

The corestricted diagonal s.

Equations

• Q2Presentation.d0FamilyS a s y = ⟨s, ⋯⟩

def Q2Presentation.d0FamilyY {ι : Type u_1} {G : ι → Type u_2} [(i : ι) → Group (G i)] (a s y : (i : ι) → G i) : ↥(d0FamilySubgroup a s y)

The corestricted diagonal y.

Equations

• Q2Presentation.d0FamilyY a s y = ⟨y, ⋯⟩

theorem Q2Presentation.d0Family_generates {ι : Type u_1} {G : ι → Type u_2} [(i : ι) → Group (G i)] (a s y : (i : ι) → G i) : Gen3 (d0FamilyA a s y) (d0FamilyS a s y) (d0FamilyY a s y)

theorem Q2Presentation.d0Family_rel {ι : Type u_1} {G : ι → Type u_2} [(i : ι) → Group (G i)] (a s y : (i : ι) → G i) (h : ∀ (i : ι), D0Relator (a i) (s i) (y i)) : D0Relator (d0FamilyA a s y) (d0FamilyS a s y) (d0FamilyY a s y)

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

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

Equations

• Q2Presentation.d0BinA A B i = (![A, B] i).a

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

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

Equations

• Q2Presentation.d0BinS A B i = (![A, B] i).s

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

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

Equations

• Q2Presentation.d0BinY A B i = (![A, B] i).y

theorem Q2Presentation.d0Bin_prod_isTwoGroup (A B : D0MarkedFinite) : IsPGroup 2 ((i : Fin 2) → Fin (![A, B] i).n)

The ambient binary product ∀ i : Fin 2, Fin (![A, B] i).n of two Demushkin 2-groups is again a 2-group (its cardinality is a power of 2).

theorem Q2Presentation.d0Bin_subgroup_isTwoGroup (A B : D0MarkedFinite) : IsPGroup 2 ↥(d0FamilySubgroup (d0BinA A B) (d0BinS A B) (d0BinY A B))

The binary subdirect carrier (subgroup of the product generated by the diagonal triple) is a 2-group.

noncomputable def Q2Presentation.d0SubdirectObj (A B : D0MarkedFinite) : D0MarkedFinite

The binary subdirect object of A, B: skeletalize the subgroup of Fin A.n × Fin B.n (as a Fin 2-product) generated by the diagonal (a, s, y), which is a 2-group, generates, and satisfies the Demushkin relation coordinatewise.

Equations

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

noncomputable def Q2Presentation.d0SubdirectFst (A B : D0MarkedFinite) : d0SubdirectObj 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.d0SubdirectSnd (A B : D0MarkedFinite) : d0SubdirectObj 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.d0MarkedFinite_isCofiltered : CategoryTheory.IsCofiltered D0MarkedFinite

The Demushkin index category is cofiltered.

The Demushkin inverse system and its limit D0

noncomputable def Q2Presentation.d0Diagram : CategoryTheory.Functor D0MarkedFinite ProfiniteGrp.{0}

The inverse system of finite marked Demushkin quotients, as a functor into ProfiniteGrp (mirrors tameDiagram).

Equations

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

@[simp]

theorem Q2Presentation.d0Diagram_map_apply {X Y : D0MarkedFinite} (f : X ⟶ Y) (x : Fin X.n) : (ProfiniteGrp.Hom.hom (d0Diagram.map f)) x = f.toMonoidHom x

instance Q2Presentation.instFiniteD0Obj (X : D0MarkedFinite) : Finite ↑(d0Diagram.obj X).toProfinite.toTop

noncomputable def Q2Presentation.D0 : ProfiniteGrp.{0}

The profinite Demushkin group D₀, the cofiltered inverse limit (in ProfiniteGrp) of all finite marked Demushkin 2-group quotients (manuscript D₀, l.208 eq:markedstandardhyp).

Equations

• Q2Presentation.D0 = CategoryTheory.Limits.limit Q2Presentation.d0Diagram

noncomputable def Q2Presentation.d0Iso : D0 ≅ ProfiniteGrp.limit d0Diagram

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.d0_limit_pi_apply (X : D0MarkedFinite) (x : ↑D0.toProfinite.toTop) : (ProfiniteGrp.Hom.hom (CategoryTheory.Limits.limit.π d0Diagram X)) x = ↑((ProfiniteGrp.Hom.hom d0Iso.hom) x) X

The categorical projection D₀ ⟶ Fin X.n, via d0Iso.

theorem Q2Presentation.D0_ext {x y : ↑D0.toProfinite.toTop} (h : ∀ (X : D0MarkedFinite), (ProfiniteGrp.Hom.hom (CategoryTheory.Limits.limit.π d0Diagram X)) x = (ProfiniteGrp.Hom.hom (CategoryTheory.Limits.limit.π d0Diagram X)) y) : x = y

Two points of D₀ agree once all coordinate projections agree.

The universal generators a, s, y

def Q2Presentation.d0GenAFamily : ↑(ProfiniteGrp.limit d0Diagram).toProfinite.toTop

The compatible family underlying a: coordinate X.a at every X.

Equations

• Q2Presentation.d0GenAFamily = ⟨fun (X : Q2Presentation.D0MarkedFinite) => X.a, ⋯⟩

def Q2Presentation.d0GenSFamily : ↑(ProfiniteGrp.limit d0Diagram).toProfinite.toTop

The compatible family underlying s: coordinate X.s at every X.

Equations

• Q2Presentation.d0GenSFamily = ⟨fun (X : Q2Presentation.D0MarkedFinite) => X.s, ⋯⟩

def Q2Presentation.d0GenYFamily : ↑(ProfiniteGrp.limit d0Diagram).toProfinite.toTop

The compatible family underlying y: coordinate X.y at every X.

Equations

• Q2Presentation.d0GenYFamily = ⟨fun (X : Q2Presentation.D0MarkedFinite) => X.y, ⋯⟩

noncomputable def Q2Presentation.d0A : ↑D0.toProfinite.toTop

The universal generator a of D₀.

Equations

• Q2Presentation.d0A = (ProfiniteGrp.Hom.hom Q2Presentation.d0Iso.inv) Q2Presentation.d0GenAFamily

noncomputable def Q2Presentation.d0S : ↑D0.toProfinite.toTop

The universal generator s of D₀.

Equations

• Q2Presentation.d0S = (ProfiniteGrp.Hom.hom Q2Presentation.d0Iso.inv) Q2Presentation.d0GenSFamily

noncomputable def Q2Presentation.d0Y : ↑D0.toProfinite.toTop

The universal generator y of D₀.

Equations

• Q2Presentation.d0Y = (ProfiniteGrp.Hom.hom Q2Presentation.d0Iso.inv) Q2Presentation.d0GenYFamily

theorem Q2Presentation.d0A_eval (X : D0MarkedFinite) : (ProfiniteGrp.Hom.hom (CategoryTheory.Limits.limit.π d0Diagram X)) d0A = X.a

Projecting a to a coordinate returns X.a.

theorem Q2Presentation.d0S_eval (X : D0MarkedFinite) : (ProfiniteGrp.Hom.hom (CategoryTheory.Limits.limit.π d0Diagram X)) d0S = X.s

Projecting s to a coordinate returns X.s.

theorem Q2Presentation.d0Y_eval (X : D0MarkedFinite) : (ProfiniteGrp.Hom.hom (CategoryTheory.Limits.limit.π d0Diagram X)) d0Y = X.y

Projecting y to a coordinate returns X.y.

theorem Q2Presentation.D0_rel (X : D0MarkedFinite) : (ProfiniteGrp.Hom.hom (CategoryTheory.Limits.limit.π d0Diagram X)) d0A ^ 2 * (ProfiniteGrp.Hom.hom (CategoryTheory.Limits.limit.π d0Diagram X)) d0S ^ 4 * commutatorW ((ProfiniteGrp.Hom.hom (CategoryTheory.Limits.limit.π d0Diagram X)) d0S) ((ProfiniteGrp.Hom.hom (CategoryTheory.Limits.limit.π d0Diagram X)) d0Y) = 1

The Demushkin relation holds in D₀ (manuscript a² s⁴ [s,y] = 1, l.208), in the inverse-limit sense: projecting the universal generators to any finite Demushkin quotient X satisfies a² s⁴ [s,y] = 1 there (because X satisfies the defining relation).

Topological generation

noncomputable def Q2Presentation.d0Homeo : ↑D0.toProfinite.toTop ≃ₜ ↑(ProfiniteGrp.limit d0Diagram).toProfinite.toTop

D₀ is homeomorphic to the explicit limit model via d0Iso.

Equations

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

noncomputable def Q2Presentation.d0EvalAt (X : D0MarkedFinite) : ↑(ProfiniteGrp.limit d0Diagram).toProfinite.toTop →* ↑(d0Diagram.obj X).toProfinite.toTop

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

Equations

• Q2Presentation.d0EvalAt X = { toFun := fun (m : ↑(ProfiniteGrp.limit Q2Presentation.d0Diagram).toProfinite.toTop) => ↑m X, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem Q2Presentation.d0EvalAt_apply (X : D0MarkedFinite) (m : ↑(ProfiniteGrp.limit d0Diagram).toProfinite.toTop) : (d0EvalAt X) m = ↑m X

theorem Q2Presentation.map_d0EvalAt_closure_eq_top (X : D0MarkedFinite) : Subgroup.map (d0EvalAt X) (Subgroup.closure {d0GenAFamily, d0GenSFamily, d0GenYFamily}) = ⊤

The coordinate-X evaluation maps the subgroup generated by a, s, y onto Fin X.n (its image is closure {X.a, X.s, X.y} = ⊤, by X.generates).

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

Finite cofiltered domination.

theorem Q2Presentation.dense_d0GenFamily : Dense ↑(Subgroup.closure {d0GenAFamily, d0GenSFamily, d0GenYFamily})

The subgroup generated by a, s, y is dense in the explicit limit model.

theorem Q2Presentation.d0Gen_topologically_generate : (Subgroup.closure {d0A, d0S, d0Y}).topologicalClosure = ⊤

The universal generators a, s, y topologically generate D₀.

Deferred: the profinite Nielsen comparison D0 ≅ PiGrp

The genuine profinite Nielsen comparison D₀ ≅ Π (manuscript Cor. 3.12, cor:relativeDemushkin) is deferred to a follow-up file. It will follow from Nielsen's categorical equivalence D0_Pi_index_equiv : D0MarkedFinite ≌ PiMarkedFinite (Boundary/Nielsen.lean) together with limit functoriality, once the parallel Boundary/PiGroup.lean (PiGrp := Limits.limit piDiagram) is built. That file should import both this file and PiGroup.lean and assemble D0_iso_PiGrp : D0 ≅ PiGrp as (limit-preimage equivalence) ≪≫ …; we do not import PiGroup.lean here to keep the two parallel constructions decoupled.