IsDemushkin: Demushkin pro-p groups

A profinite pro-p group G is Demushkin (Serre, Galois Cohomology I §4.5; NSW Def. 3.9.9; Labute, Classification of Demushkin groups, Canad. J. Math. 19 (1967)) if, for 𝔽_p-coefficients with the trivial action,

1. H¹(G, 𝔽_p) is finite (equivalently G is topologically finitely generated — Burnside basis, NSW 3.9.1; we do not carry the redundant generation clause),
2. dim_{𝔽_p} H²(G, 𝔽_p) = 1, and
3. the cup product H¹ × H¹ → H² is a non-degenerate bilinear form.

This is the definition behind the paper's B3/B4 leaves: G_{ℚ₂}(2) = maxProPQuotient 2 AbsGalQ2 is Demushkin of rank 3 with q = 2 (NSW Thm 7.5.11(ii)), encoded by the dyadic presentation and orientation interfaces.

Encoding

• Cohomology is GQ2.ContCoh (the continuous-cohomology API) with coefficients the literal ZMod p; following the the continuous-cohomology API note, dimension conditions are phrased via Nat.card — H¹/H² are p-torsion, so finiteness forces Nat.card = p ^ dim (IsDemushkin.card_H1_eq_pow), and clause 2 becomes Nat.card (H2 G (ZMod p)) = p. The rank is recovered as demushkinRank p G := padicValNat p (Nat.card (H1 G (ZMod p))).
• The cup form is the cup-product API's cup11 relative to the multiplication pairing AddMonoidHom.mul : ZMod p →+ ZMod p →+ ZMod p (trivialCupPairing); non-degeneracy is stated two-sidedly (nondegen_left/nondegen_right) since graded-commutativity of cup11 is not formalized — for p = 2 the form is symmetric and the clauses coincide, and in the literature each implies the other by finite-dimensional linear algebra.
• The trivial action enters as in the continuous-cohomology API/the Kummer-class API: the ambient [DistribMulAction G (ZMod p)] instance is constrained by the structure field smul_trivial. (For p = 2 every action is trivial — Aut(ℤ/2) = 1 — so this is no restriction there.) By proof irrelevance, trivialCupPairing p G h₁ and trivialCupPairing p G h₂ are definitionally equal, so the non-degeneracy clauses can be consumed with any proof of triviality (IsDemushkin.nondegen_left').
• isProP is the maximal pro-p quotient API's predicate; profiniteness of G is ambient, entering only through the instances a caller supplies.

Stress tests

• Positive (isDemushkin_cyclicTwo): ℤ/2 is Demushkin of rank 1 — the unique finite Demushkin group (Serre GC I §4.5). H¹ and H² are computed explicitly (both ≃+ ZMod 2), and the generator's cup square is the class of the 4-point cocycle (g,h) ↦ c₀(g)·c₀(h) — the extension class of ℤ/4 — detected non-zero by the evaluation functional f ↦ f(1,1) + f(σ,σ). This exercises every field of the structure. ℤ/2 is realized as DihedralGroup 1 (as in the App. B tests), not Multiplicative (ZMod 2): Mathlib's Multiplicative.smul transfer instance would make g • m mean multiplication in ZMod 2, clashing with the trivial coefficient action.
• Negative (not_isDemushkin_punit): the trivial group — the rank-0 free pro-p group — has H² = 0, so clause 2 fails (Nat.card H² = 1 ≠ p); free pro-p groups are the archetypal non-Demushkin groups (plan B3a: "H² = 0, pick cheap ones").
• The plan's H¹(G,𝔽₂) ≃ ContinuousMonoidHom G 𝔽₂ sanity check is delivered wrapper-free, as in the continuous-cohomology API: ContCoh.H1equivZ1OfTrivial composed with the explicit evaluation equivalence z1CyclicTwoEquiv (avoiding Multiplicative-wrapped hom-types).

Consumers: the dyadic-presentation interface (IsDemushkin (maxProPQuotient 2 AbsGalQ2) strengthening), the Demushkin classification (rank-3 q = 2 classification; use demushkinRank_eq_of_card), the orientation interface (the orientation character pairs against trivialCupPairing).

The cup form and the definition

noncomputable def GQ2.trivialCupPairing (p : ℕ) (G : Type u_1) [Group G] [TopologicalSpace G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (htriv : ∀ (g : G) (m : ZMod p), g • m = m) : ContCoh.H1 G (ZMod p) →+ ContCoh.H1 G (ZMod p) →+ ContCoh.H2 G (ZMod p)

The cup-product form H¹(G,𝔽_p) × H¹(G,𝔽_p) → H²(G,𝔽_p) relative to the multiplication pairing on ZMod p, available once the coefficient action is trivial. By proof irrelevance the value does not depend on the proof htriv.

Equations

• GQ2.trivialCupPairing p G htriv = GQ2.ContCoh.cup11 AddMonoidHom.mul ⋯

structure GQ2.IsDemushkin (p : ℕ) (G : Type u_1) [Group G] [TopologicalSpace G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] : Prop

Demushkin pro-p group (Serre GC I §4.5, NSW Def. 3.9.9), with the dimension clauses in Nat.card form (see module docstring). The ambient action on ZMod p is constrained to be trivial by the field smul_trivial.

• smul_trivial (g : G) (m : ZMod p) : g • m = m

  The coefficient action is the trivial one (the literature's 𝔽_p).

• isProP : IsProP p G

  G is pro-p (the maximal pro-p quotient API's IsProP).

• finiteH1 : Finite (ContCoh.H1 G (ZMod p))

  Clause 1: dim H¹ < ∞.

• cardH2 : Nat.card (ContCoh.H2 G (ZMod p)) = p

  Clause 2: dim H² = 1, i.e. #H² = p.

• nondegen_left (x : ContCoh.H1 G (ZMod p)) : x ≠ 0 → ∃ (y : ContCoh.H1 G (ZMod p)), ((trivialCupPairing p G ⋯) x) y ≠ 0

  Clause 3, left: every non-zero H¹-class cups non-trivially with something.

• nondegen_right (y : ContCoh.H1 G (ZMod p)) : y ≠ 0 → ∃ (x : ContCoh.H1 G (ZMod p)), ((trivialCupPairing p G ⋯) x) y ≠ 0

  Clause 3, right: the symmetric clause (graded-commutativity is not formalized).

noncomputable def GQ2.demushkinRank (p : ℕ) (G : Type u_1) [Group G] [TopologicalSpace G] [DistribMulAction G (ZMod p)] : ℕ

The rank of a Demushkin group: n = dim_{𝔽_p} H¹(G,𝔽_p), recovered from the cardinality (see IsDemushkin.card_H1_eq_pow). Junk value when G is not Demushkin.

Equations

• GQ2.demushkinRank p G = padicValNat p (Nat.card (GQ2.ContCoh.H1 G (ZMod p)))

Basic API

theorem GQ2.IsDemushkin.nondegen_left' {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (hD : IsDemushkin p G) (htriv : ∀ (g : G) (m : ZMod p), g • m = m) (x : ContCoh.H1 G (ZMod p)) (hx : x ≠ 0) : ∃ (y : ContCoh.H1 G (ZMod p)), ((trivialCupPairing p G htriv) x) y ≠ 0

The left non-degeneracy clause, consumable with any proof of action-triviality (the pairing does not depend on the proof).

theorem GQ2.IsDemushkin.nondegen_right' {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] (hD : IsDemushkin p G) (htriv : ∀ (g : G) (m : ZMod p), g • m = m) (y : ContCoh.H1 G (ZMod p)) (hy : y ≠ 0) : ∃ (x : ContCoh.H1 G (ZMod p)), ((trivialCupPairing p G htriv) x) y ≠ 0

Right-slot variant of IsDemushkin.nondegen_left'.

theorem GQ2.nsmul_H1_eq_zero {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [DistribMulAction G (ZMod p)] (x : ContCoh.H1 G (ZMod p)) : p • x = 0

H¹(G, 𝔽_p) is p-torsion (the coefficients are).

theorem GQ2.IsDemushkin.card_H1_eq_pow {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [DistribMulAction G (ZMod p)] [ContinuousSMul G (ZMod p)] [Fact (Nat.Prime p)] (hD : IsDemushkin p G) : Nat.card (ContCoh.H1 G (ZMod p)) = p ^ demushkinRank p G

For a Demushkin group, #H¹ = p ^ rank — the Nat.card clause really encodes an 𝔽_p-dimension.

theorem GQ2.demushkinRank_eq_of_card {p : ℕ} {G : Type u_1} [Group G] [TopologicalSpace G] [DistribMulAction G (ZMod p)] [Fact (Nat.Prime p)] {n : ℕ} (h : Nat.card (ContCoh.H1 G (ZMod p)) = p ^ n) : demushkinRank p G = n

Computation rule for the rank: exhibit the cardinality as a p-power.

The q-invariant

Labute's second invariant: for a Demushkin group, G^{ab} ≅ ℤ_p^{n−1} × ℤ/q with q = p^s (or q = 0, torsion-free), and the classification (his Théorème 8) is by (n, q) — plus, in the exceptional q = 2 case, the image of the canonical orientation character. We take G^{ab} to be the topological abelianization (quotient by the closed commutator — the right notion for profinite G) and read q off as the number of torsion elements (#(ℤ/q) = q when the torsion is finite cyclic; junk value otherwise, in particular the sensible reading of "q = 0" is not encoded — documented deviation).

B3b is deliberately not an axiom (docs/orchestration/formalization-plan.md §B3): stating the abstract rank-3 q = 2 classification honestly requires Labute's canonical character (his Prop. 6 dualizing characterization — route (i) of the orientation interface, deferred); quantifying over an arbitrary continuous character with the right image would be a different (and possibly false) statement. At the field level the classification instance the paper uses is axiom B4 (G_{ℚ₂}(2) ≅ D₀), whose orientation normalization is axiom B3c (dyadicOrientation, route (ii)). This section supplies the invariant so that the classification data (rank, q) = (3, 2) is at least expressible; demushkinQ D₀ = 2 itself is Labute-content and is not attempted.

def GQ2.topAbelianization (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Type u_1

The topological abelianization G^{ab} = G ⧸ closure ⁅G,G⁆ (for profinite G this is the profinite abelianization; cf. AbsGalQ2ab in GQ2/Reciprocity.lean).

Equations

• GQ2.topAbelianization G = (G ⧸ (commutator G).topologicalClosure)

@[implicit_reducible]

noncomputable instance GQ2.instGroupTopAbelianization (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : Group (topAbelianization G)

Equations

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

noncomputable def GQ2.demushkinQ (G : Type u_1) [Group G] [TopologicalSpace G] [IsTopologicalGroup G] : ℕ

The q-invariant (Labute): the number of torsion elements of the topological abelianization — = q when G^{ab} ≅ ℤ_p^{n−1} × ℤ/q with q ≠ 0. Junk value otherwise (see the section docstring).

Equations

• GQ2.demushkinQ G = Nat.card { x : GQ2.topAbelianization G // IsOfFinOrder x }

Positive stress test: ℤ/2 is Demushkin of rank 1

ℤ/2 (as DihedralGroup 1, discrete) is the unique finite Demushkin group. We compute H¹ ≃+ ZMod 2 (evaluation at the generator σ), H² ≃+ ZMod 2 (the functional f ↦ f(1,1) + f(σ,σ), which kills coboundaries), and the cup square of the generator — the class of (g,h) ↦ c₀(g)·c₀(h), the extension class of ℤ/4 — evaluates to 1 ≠ 0.

@[implicit_reducible]

instance GQ2.instDistribMulActionDihedralGroupOfNatNatZMod_gQ2 : DistribMulAction (DihedralGroup 1) (ZMod 2)

The trivial action of ℤ/2 = DihedralGroup 1 on 𝔽₂. Safe to register globally: Aut(ℤ/2) = 1, so every distributive action on ZMod 2 is trivial (same convention as GQ2/Kummer.lean).

Equations

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

@[implicit_reducible]

def GQ2.instTopologicalSpaceD1 : TopologicalSpace (DihedralGroup 1)

Equations

• GQ2.instTopologicalSpaceD1 = ⊥

theorem GQ2.instDiscreteTopologyD1 : DiscreteTopology (DihedralGroup 1)

theorem GQ2.instContinuousSMulD1 : ContinuousSMul (DihedralGroup 1) (ZMod 2)

def GQ2.cCyclicTwo : ↥(ContCoh.Z1 (DihedralGroup 1) (ZMod 2))

The generating 1-cocycle c₀ (the nontrivial character ℤ/2 → 𝔽₂).

Equations

• GQ2.cCyclicTwo = ⟨fun (g : DihedralGroup 1) => if g = 1 then 0 else 1, GQ2.cCyclicTwo._proof_1⟩

noncomputable def GQ2.z1CyclicTwoEquiv : ↥(ContCoh.Z1 (DihedralGroup 1) (ZMod 2)) ≃+ ZMod 2

Evaluation at the generator: Z¹(ℤ/2, 𝔽₂) ≃+ 𝔽₂ (1-cocycles are homs, determined by the value at σ).

Equations

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

noncomputable def GQ2.h1CyclicTwoEquiv : ContCoh.H1 (DihedralGroup 1) (ZMod 2) ≃+ ZMod 2

H¹(ℤ/2, 𝔽₂) ≃+ 𝔽₂ (the plan's "H¹ ≃ continuous homs" check, in the wrapper-free the continuous-cohomology API form).

Equations

• GQ2.h1CyclicTwoEquiv = (GQ2.ContCoh.H1equivZ1OfTrivial GQ2.htrivC2✝).trans GQ2.z1CyclicTwoEquiv

def GQ2.z2CyclicTwoEval : ↥(ContCoh.Z2 (DihedralGroup 1) (ZMod 2)) →+ ZMod 2

The evaluation functional f ↦ f(1,1) + f(σ,σ) on 2-cocycles.

Equations

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

noncomputable def GQ2.h2CyclicTwoEval : ContCoh.H2 (DihedralGroup 1) (ZMod 2) →+ ZMod 2

The induced functional on H².

Equations

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

def GQ2.wCyclicTwo : ↥(ContCoh.Z2 (DihedralGroup 1) (ZMod 2))

The 4-point product cocycle w(g,h) = c₀(g)·c₀(h) — the generator of H² (the extension class of ℤ/4, and the cup square of the generator of H¹).

Equations

• GQ2.wCyclicTwo = ⟨fun (q : DihedralGroup 1 × DihedralGroup 1) => (if q.1 = 1 then 0 else 1) * if q.2 = 1 then 0 else 1, GQ2.wCyclicTwo._proof_1⟩

noncomputable def GQ2.h2CyclicTwoEquiv : ContCoh.H2 (DihedralGroup 1) (ZMod 2) ≃+ ZMod 2

H²(ℤ/2, 𝔽₂) ≃+ 𝔽₂.

Equations

• GQ2.h2CyclicTwoEquiv = AddEquiv.ofBijective GQ2.h2CyclicTwoEval GQ2.h2CyclicTwoEquiv._proof_2

theorem GQ2.isDemushkin_cyclicTwo : IsDemushkin 2 (DihedralGroup 1)

ℤ/2 is a Demushkin group — the unique finite one (Serre GC I §4.5).

theorem GQ2.demushkinRank_cyclicTwo : demushkinRank 2 (DihedralGroup 1) = 1

ℤ/2 has Demushkin rank 1.

theorem GQ2.demushkinQ_cyclicTwo : demushkinQ (DihedralGroup 1) = 2

ℤ/2 has q-invariant 2 (the Demushkin classification stress): it is abelian and finite, so G^{ab} = G = ℤ/2 and every element is torsion — matching Labute's q(⟨x | x²⟩) = 2.

Negative stress test: the trivial group is not Demushkin

PUnit is the free pro-p group of rank 0: H²(1, 𝔽_p) = 0, so clause 2 fails. (Free pro-p groups all have H² = 0 — Serre GC I §4.2 — and are the basic non-examples.)

@[implicit_reducible]

instance GQ2.instDistribMulActionPUnitZMod_gQ2 (p : ℕ) : DistribMulAction PUnit.{u_1 + 1} (ZMod p)

The (unique) action of the trivial group. Global for the same reason as the ℤ/2 instance: one_smul forces any action of PUnit to be trivial.

Equations

• GQ2.instDistribMulActionPUnitZMod_gQ2 p = { smul := fun (x : PUnit.{?u.1 + 1}) (m : ZMod p) => m, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯ }

instance GQ2.instContinuousSMulPUnitZMod_gQ2 (p : ℕ) : ContinuousSMul PUnit.{u_1 + 1} (ZMod p)

theorem GQ2.not_isDemushkin_punit (p : ℕ) [Fact (Nat.Prime p)] : ¬IsDemushkin p PUnit.{u_1 + 1}

The trivial group is not Demushkin: H² = 0 (it is free pro-p of rank 0), violating #H² = p.