The Nielsen transform, finite part (Stage C, work order C4)

This file is the finite-quotient-category form of the manuscript's Nielsen transform to the pro-2 boundary (reference/q2_manuscript.tex, Proposition 3.11 prop:abstractDemushkin, lines ~998–1025). It is pure finite group theory: independent of Stage B (GammaA) and of all profinite machinery.

The substitution (manuscript Prop 3.11)

The standard rank-three dyadic Demushkin group D₀ has the single defining relation (manuscript l.208, l.489, l.575) a² s⁴ [s,y] = 1 (here [s,y] = commutatorW s y). The Nielsen change of generators (manuscript eq. nielsenrelative, l.1005) σ = s, x₁ = y, x₀ = s⁻² a⁻¹ carries the closed normal closure of that relator to that of the pro-2 boundary relator (manuscript eq. relativeDemrelation, l.1010) x₀^{σ²} x₀ [x₁,σ] ( = rconj x₀ (σ²) * x₀ * commutatorW x₁ σ, the EXACT relation form of Boundary/PiFinite.lean's admissible_twoGroup_iff_piMarked ).

Why nielsen_rel_equiv is not a single group call

The manuscript proof (l.1016–1025) is explicit that the two relator words are cyclic conjugates, not equal: writing P = x₀^{σ²} x₀ and Q = [x₁,σ], the inverse of the standard relator is Q P, while the boundary relator is P Q, and QP, PQ have the same closed normal closure only because they are cyclic conjugates. Concretely (c := s⁻⁴ a⁻²) one has the pure group identity rconj x₀ (σ²) * x₀ * commutatorW x₁ σ = c · (a² s⁴ [s,y])⁻¹ · c⁻¹ , so the boundary relator is a conjugate of the inverse of the Demushkin relator. Hence R = 1 ↔ W = 1 holds (the content of nielsen_rel_equiv) but a bare group cannot close the Iff — group proves equalities, and the two "… = 1" sides are genuinely different elements. We discharge each direction by rewriting along the conjugation identity (itself closed by group), mirroring the manuscript's cyclic-conjugacy argument. The plan's / Prop 3.11's substitution is correct as written; no correction was needed.

Category equivalence

D0MarkedFinite ≌ PiMarkedFinite is the induced equivalence of the two finite 2-group quotient categories. Objects correspond via the (mutually inverse) markings; morphisms are the marking-preserving homomorphisms of the skeletal carriers, and nielsen_rel_equiv is what makes the defining relation transfer. Both round trips are the identity on markings up to a group-provable rewrite, so the unit and counit are built from identity homomorphisms.

The profinite isomorphism D₀ ≅ Π is deferred: it needs the inverse-limit machinery (not yet built). See the note at the end of the file.

The Fin n group-instance threading mirrors Candidate/AdmissibleIndex.lean and Candidate/AdmissibleCat.lean: the bundled groupFin is made an instance and letI := …groupFin is used whenever a fresh Group (Fin n) is required, so the global Fin.instMul is never synthesized.

The Nielsen substitution on triples (manuscript eq. nielsenrelative)

structure Q2Presentation.D0Triple (G : Type u_1) [Group G] : Type u_1

A D₀-marking: the three Demushkin generators a, s, y.

• a : G

  The generator a (with ν_ur(a) = -2).

• s : G

  The generator s (geometric Frobenius lift, ν_ur(s) = 1).

• y : G

  The generator y (with ν_ur(y) = 0).

structure Q2Presentation.PiTriple (G : Type u_1) [Group G] : Type u_1

A Π-marking: the three pro-2 boundary generators σ, x₀, x₁.

• sigma : G

  The generator σ.

• x0 : G

  The generator x₀.

• x1 : G

  The generator x₁.

def Q2Presentation.D0_to_Pi_marking {G : Type u_1} [Group G] (a s y : G) : PiTriple G

The Nielsen transform D₀ → Π (manuscript eq. nielsenrelative): σ = s, x₁ = y, x₀ = s⁻² a⁻¹.

Equations

• Q2Presentation.D0_to_Pi_marking a s y = { sigma := s, x0 := (s ^ 2)⁻¹ * a⁻¹, x1 := y }

def Q2Presentation.Pi_to_D0_marking {G : Type u_1} [Group G] (sigma x0 x1 : G) : D0Triple G

The inverse Nielsen transform Π → D₀ (manuscript l.1018, a = x₀⁻¹σ⁻²): a = x₀⁻¹ σ⁻², s = σ, y = x₁.

Equations

• Q2Presentation.Pi_to_D0_marking sigma x0 x1 = { a := x0⁻¹ * (sigma ^ 2)⁻¹, s := sigma, y := x1 }

The relation equivalence (manuscript Proposition 3.11)

theorem Q2Presentation.nielsen_rel_equiv {G : Type u_1} [Group G] (a s y : G) : a ^ 2 * s ^ 4 * commutatorW s y = 1 ↔ rconj ((s ^ 2)⁻¹ * a⁻¹) (s ^ 2) * ((s ^ 2)⁻¹ * a⁻¹) * commutatorW y s = 1

Proposition 3.11 (pure group form). Under the Nielsen substitution σ = s, x₀ = s⁻² a⁻¹, x₁ = y, the standard Demushkin relator a² s⁴ [s,y] vanishes iff the pro-2 boundary relator x₀^{σ²} x₀ [x₁,σ] (the EXACT relation form of PiFinite.admissible_twoGroup_iff_piMarked) vanishes.

This is not an equality of the two relator words: as in the manuscript (l.1022–1024) they are cyclic conjugates. The proof rewrites each direction along the conjugation identity W = c · R⁻¹ · c⁻¹ with c = s⁻⁴ a⁻², which group verifies.

theorem Q2Presentation.nielsen_rel_equiv' {G : Type u_1} [Group G] (sigma x0 x1 : G) : rconj x0 (sigma ^ 2) * x0 * commutatorW x1 sigma = 1 ↔ (x0⁻¹ * (sigma ^ 2)⁻¹) ^ 2 * sigma ^ 4 * commutatorW sigma x1 = 1

The inverse-direction relation equivalence (used to transfer the relation along Pi_to_D0): the pro-2 boundary relator at (σ, x₀, x₁) vanishes iff the standard Demushkin relator at (x₀⁻¹ σ⁻², σ, x₁) vanishes. Derived from nielsen_rel_equiv by rewriting σ⁻²(x₀⁻¹σ⁻²)⁻¹ = x₀.

Generation transfer

The two markings generate the same subgroup because each generator of one is a word in the generators of the other.

theorem Q2Presentation.closure_nielsen_to {G : Type u_1} [Group G] (a s y : G) (h : Subgroup.closure {a, s, y} = ⊤) : Subgroup.closure {s, (s ^ 2)⁻¹ * a⁻¹, y} = ⊤

If {a, s, y} generates, so does the Nielsen image {s, s⁻²a⁻¹, y}. (Worked at the proof-term level: a occurs inside the target generating set, so rw on the goal is unavailable; we rewrite the membership proof instead.)

theorem Q2Presentation.closure_nielsen_from {G : Type u_1} [Group G] (sigma x0 x1 : G) (h : Subgroup.closure {sigma, x0, x1} = ⊤) : Subgroup.closure {x0⁻¹ * (sigma ^ 2)⁻¹, sigma, x1} = ⊤

If {σ, x₀, x₁} generates, so does the inverse Nielsen image {x₀⁻¹σ⁻², σ, x₁}.

The two finite marked-quotient categories

The defining predicates are packaged as standalone definitions that thread the group instance through a [Group G] argument (exactly as Foundation.Admissible does). This is essential: writing the relations inline in the structure field types would let the elaborator synthesise the global Fin.instMul for the bare */^, baking the wrong instance into the field types.

def Q2Presentation.Gen3 {G : Type u_1} [Group G] (p q r : G) : Prop

A triple generates G.

Equations

• Q2Presentation.Gen3 p q r = (Subgroup.closure {p, q, r} = ⊤)

def Q2Presentation.D0Relator {G : Type u_1} [Group G] (a s y : G) : Prop

The standard Demushkin relator a² s⁴ [s,y] = 1.

Equations

• Q2Presentation.D0Relator a s y = (a ^ 2 * s ^ 4 * Q2Presentation.commutatorW s y = 1)

def Q2Presentation.PiRelator {G : Type u_1} [Group G] (sigma x0 x1 : G) : Prop

The pro-2 boundary relator x₀^{σ²} x₀ [x₁,σ] = 1 (the relation form of PiFinite.admissible_twoGroup_iff_piMarked).

Equations

• Q2Presentation.PiRelator sigma x0 x1 = (Q2Presentation.rconj x0 (sigma ^ 2) * x0 * Q2Presentation.commutatorW x1 sigma = 1)

structure Q2Presentation.D0MarkedFinite : Type

A finite 2-group with a generating Demushkin marking a, s, y satisfying a² s⁴ [s,y] = 1. Carrier pinned to the skeleton Fin n (cf. AdmissibleIndex).

• n : ℕ

  Cardinality of the skeletal carrier.

• hn : Fact (0 < self.n)

  The carrier is nonempty (Fin n carries a group).

• groupFin : Group (Fin self.n)

  The group structure on Fin n.

• isTwoGroup : IsPGroup 2 (Fin self.n)

  The carrier is a 2-group.

• a : Fin self.n

  Demushkin generator a.

• s : Fin self.n

  Demushkin generator s.

• y : Fin self.n

  Demushkin generator y.

• generates : Gen3 self.a self.s self.y

  {a, s, y} generates.

• rel : D0Relator self.a self.s self.y

  The standard Demushkin relation a² s⁴ [s,y] = 1.

structure Q2Presentation.PiMarkedFinite : Type

A finite 2-group with a generating pro-2 boundary marking σ, x₀, x₁ satisfying the boundary relation x₀^{σ²} x₀ [x₁,σ] = 1 (the relation form of PiFinite.admissible_twoGroup_iff_piMarked).

• n : ℕ

  Cardinality of the skeletal carrier.

• hn : Fact (0 < self.n)

  The carrier is nonempty.

• groupFin : Group (Fin self.n)

  The group structure on Fin n.

• isTwoGroup : IsPGroup 2 (Fin self.n)

  The carrier is a 2-group.

• sigma : Fin self.n

  Boundary generator σ.

• x0 : Fin self.n

  Boundary generator x₀.

• x1 : Fin self.n

  Boundary generator x₁.

• generates : Gen3 self.sigma self.x0 self.x1

  {σ, x₀, x₁} generates.

• rel : PiRelator self.sigma self.x0 self.x1

  The pro-2 boundary relation x₀^{σ²} x₀ [x₁,σ] = 1.

D₀ morphisms and category

structure Q2Presentation.D0Hom (X Y : D0MarkedFinite) : Type

A marking-preserving homomorphism of D0MarkedFinite carriers.

• toMonoidHom : Fin X.n →* Fin Y.n

  The underlying homomorphism of skeletal carriers.

• map_a : self.toMonoidHom X.a = Y.a

  Preserves a.

• map_s : self.toMonoidHom X.s = Y.s

  Preserves s.

• map_y : self.toMonoidHom X.y = Y.y

  Preserves y.

theorem Q2Presentation.D0Hom.ext' {X Y : D0MarkedFinite} {f g : D0Hom X Y} (h : f.toMonoidHom = g.toMonoidHom) : f = g

theorem Q2Presentation.D0Hom.ext'_iff {X Y : D0MarkedFinite} {f g : D0Hom X Y} : f = g ↔ f.toMonoidHom = g.toMonoidHom

def Q2Presentation.D0Hom.id (X : D0MarkedFinite) : D0Hom X X

The identity D₀ morphism.

Equations

• Q2Presentation.D0Hom.id X = { toMonoidHom := MonoidHom.id (Fin X.n), map_a := ⋯, map_s := ⋯, map_y := ⋯ }

def Q2Presentation.D0Hom.comp {X Y Z : D0MarkedFinite} (f : D0Hom X Y) (g : D0Hom Y Z) : D0Hom X Z

Composition of D₀ morphisms.

Equations

• f.comp g = { toMonoidHom := g.toMonoidHom.comp f.toMonoidHom, map_a := ⋯, map_s := ⋯, map_y := ⋯ }

instance Q2Presentation.instCategoryD0 : CategoryTheory.Category.{0, 0} D0MarkedFinite

Equations

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

theorem Q2Presentation.D0Hom_ext {X Y : D0MarkedFinite} (f g : X ⟶ Y) : f = g

Any two parallel D₀ morphisms coincide (they agree on the generating marking {a, s, y}, which is dense).

def Q2Presentation.D0Iso {X Y : D0MarkedFinite} (f : X ⟶ Y) (g : Y ⟶ X) : X ≅ Y

Build a D₀ isomorphism from a pair of morphisms (the two identities are automatic by D0Hom_ext).

Equations

• Q2Presentation.D0Iso f g = { hom := f, inv := g, hom_inv_id := ⋯, inv_hom_id := ⋯ }

Π morphisms and category

structure Q2Presentation.PiHom (X Y : PiMarkedFinite) : Type

A marking-preserving homomorphism of PiMarkedFinite carriers.

• toMonoidHom : Fin X.n →* Fin Y.n

  The underlying homomorphism of skeletal carriers.

• map_sigma : self.toMonoidHom X.sigma = Y.sigma

  Preserves σ.

• map_x0 : self.toMonoidHom X.x0 = Y.x0

  Preserves x₀.

• map_x1 : self.toMonoidHom X.x1 = Y.x1

  Preserves x₁.

theorem Q2Presentation.PiHom.ext' {X Y : PiMarkedFinite} {f g : PiHom X Y} (h : f.toMonoidHom = g.toMonoidHom) : f = g

theorem Q2Presentation.PiHom.ext'_iff {X Y : PiMarkedFinite} {f g : PiHom X Y} : f = g ↔ f.toMonoidHom = g.toMonoidHom

def Q2Presentation.PiHom.id (X : PiMarkedFinite) : PiHom X X

The identity Π morphism.

Equations

• Q2Presentation.PiHom.id X = { toMonoidHom := MonoidHom.id (Fin X.n), map_sigma := ⋯, map_x0 := ⋯, map_x1 := ⋯ }

def Q2Presentation.PiHom.comp {X Y Z : PiMarkedFinite} (f : PiHom X Y) (g : PiHom Y Z) : PiHom X Z

Composition of Π morphisms.

Equations

• f.comp g = { toMonoidHom := g.toMonoidHom.comp f.toMonoidHom, map_sigma := ⋯, map_x0 := ⋯, map_x1 := ⋯ }

instance Q2Presentation.instCategoryPi : CategoryTheory.Category.{0, 0} PiMarkedFinite

Equations

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

theorem Q2Presentation.PiHom_ext {X Y : PiMarkedFinite} (f g : X ⟶ Y) : f = g

Any two parallel Π morphisms coincide.

def Q2Presentation.PiIso {X Y : PiMarkedFinite} (f : X ⟶ Y) (g : Y ⟶ X) : X ≅ Y

Build a Π isomorphism from a pair of morphisms.

Equations

• Q2Presentation.PiIso f g = { hom := f, inv := g, hom_inv_id := ⋯, inv_hom_id := ⋯ }

The Nielsen functor D₀ ⥤ Π

def Q2Presentation.D0_to_Pi_obj (D : D0MarkedFinite) : PiMarkedFinite

Object map of the Nielsen functor: relabel the marking by D0_to_Pi_marking, transfer generates via closure_nielsen_to and rel via nielsen_rel_equiv.

Equations

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

def Q2Presentation.D0_to_Pi_map {X Y : D0MarkedFinite} (f : X ⟶ Y) : D0_to_Pi_obj X ⟶ D0_to_Pi_obj Y

Morphism map of the Nielsen functor: the same underlying homomorphism.

Equations

• Q2Presentation.D0_to_Pi_map f = { toMonoidHom := f.toMonoidHom, map_sigma := ⋯, map_x0 := ⋯, map_x1 := ⋯ }

def Q2Presentation.D0_to_Pi : CategoryTheory.Functor D0MarkedFinite PiMarkedFinite

The Nielsen transform as a functor D₀ ⥤ Π.

Equations

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

The inverse functor Π ⥤ D₀

def Q2Presentation.Pi_to_D0_obj (P : PiMarkedFinite) : D0MarkedFinite

Object map of the inverse Nielsen functor.

Equations

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

def Q2Presentation.Pi_to_D0_map {X Y : PiMarkedFinite} (f : X ⟶ Y) : Pi_to_D0_obj X ⟶ Pi_to_D0_obj Y

Morphism map of the inverse Nielsen functor.

Equations

• Q2Presentation.Pi_to_D0_map f = { toMonoidHom := f.toMonoidHom, map_a := ⋯, map_s := ⋯, map_y := ⋯ }

def Q2Presentation.Pi_to_D0 : CategoryTheory.Functor PiMarkedFinite D0MarkedFinite

The inverse Nielsen transform as a functor Π ⥤ D₀.

Equations

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

Unit and counit

Both round trips are the identity on the carrier; the markings agree up to a group-provable rewrite, so each component is an identity-homomorphism iso.

def Q2Presentation.unitHomComp (X : D0MarkedFinite) : X ⟶ (D0_to_Pi.comp Pi_to_D0).obj X

Unit component X ⟶ (D0_to_Pi ⋙ Pi_to_D0).obj X.

Equations

• Q2Presentation.unitHomComp X = { toMonoidHom := MonoidHom.id (Fin X.n), map_a := ⋯, map_s := ⋯, map_y := ⋯ }

def Q2Presentation.unitInvComp (X : D0MarkedFinite) : (D0_to_Pi.comp Pi_to_D0).obj X ⟶ X

Inverse unit component (D0_to_Pi ⋙ Pi_to_D0).obj X ⟶ X.

Equations

• Q2Presentation.unitInvComp X = { toMonoidHom := MonoidHom.id (Fin X.n), map_a := ⋯, map_s := ⋯, map_y := ⋯ }

def Q2Presentation.unitIso : CategoryTheory.Functor.id D0MarkedFinite ≅ D0_to_Pi.comp Pi_to_D0

The unit isomorphism 𝟭 D₀ ≅ D0_to_Pi ⋙ Pi_to_D0.

Equations

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

def Q2Presentation.counitHomComp (P : PiMarkedFinite) : (Pi_to_D0.comp D0_to_Pi).obj P ⟶ P

Counit component (Pi_to_D0 ⋙ D0_to_Pi).obj P ⟶ P.

Equations

• Q2Presentation.counitHomComp P = { toMonoidHom := MonoidHom.id (Fin P.n), map_sigma := ⋯, map_x0 := ⋯, map_x1 := ⋯ }

def Q2Presentation.counitInvComp (P : PiMarkedFinite) : P ⟶ (Pi_to_D0.comp D0_to_Pi).obj P

Inverse counit component P ⟶ (Pi_to_D0 ⋙ D0_to_Pi).obj P.

Equations

• Q2Presentation.counitInvComp P = { toMonoidHom := MonoidHom.id (Fin P.n), map_sigma := ⋯, map_x0 := ⋯, map_x1 := ⋯ }

def Q2Presentation.counitIso : Pi_to_D0.comp D0_to_Pi ≅ CategoryTheory.Functor.id PiMarkedFinite

The counit isomorphism Pi_to_D0 ⋙ D0_to_Pi ≅ 𝟭 Π.

Equations

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

The category equivalence

def Q2Presentation.D0_Pi_index_equiv : D0MarkedFinite ≌ PiMarkedFinite

The Nielsen transform induces an equivalence of the two finite marked-quotient categories D0MarkedFinite ≌ PiMarkedFinite (manuscript Proposition 3.11). Objects correspond via the markings D0_to_Pi_marking / Pi_to_D0_marking; nielsen_rel_equiv makes the defining relation transfer; the triangle identity is automatic since every hom-set is a subsingleton.

Equations

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

Deferred: the profinite isomorphism D₀ ≅ Π

The genuine profinite statement D₀ ≅ Π (manuscript Cor. 3.12, cor:relativeDemushkin) is deferred: it requires the inverse-limit machinery over these index categories (the ProfiniteGrp cofiltered-limit construction), which is not yet built in this development. The categorical equivalence D0_Pi_index_equiv above is the finite-quotient avatar that this profinite isomorphism will be reconstructed from.

Acceptance checks