Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Proposition 2.3

Proved
LocalConjugacy.proposition_2_3

by burkh4rt · Sep 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

group-theorylocal-conjugacynonabelian-cohomologyprofinite-groups

For a profinite group JJJ and a finite JJJ-group NNN that is also a ppp-group, suppose NJNJNJ is prosupersolvable. Let π\piπ denote the set of primes not exceeding ppp and let QQQ be a Hall π\piπ-subgroup of JJJ. Then res⁡QJ:H1(J,N)→∼H1(Q,N)\operatorname{res}^{J}_{Q}:H^1(J,N)\xrightarrow{\sim}H^1(Q,N)resQJ​:H1(J,N)∼​H1(Q,N) is an isomorphism.

As stipulated in §1.2, subgroup notation includes closedness, and a discrete JJJ-group has a continuous action by automorphisms.

Preamble
import Definitions.Def_LocalConjugacy_Cohomology

/-
Proposition 2.3: the arXiv version assumes profinite J and prosupersolvable NJ.
There is no additional prosolvability hypothesis. Q is any Hall subgroup for
the primes at most p, and the codomain is all H¹(Q,N), not just stable classes.

This is an open draft target. The deliberate `sorry` is the target proof hole;
all definitions and the structural proofs on which the statement rests compile
without admitted proofs.
-/
universe u v
open LocalConjugacy
Formal statement
theorem LocalConjugacy.proposition_2_3 {J : ProfiniteGrp.{u}} {N : Type v} [Group N]
    [TopologicalSpace N] [MulDistribMulAction J N] [DiscreteTopology N] [Finite N]
    [ContinuousSMul J N] (p : ℕ) (hp : p.Prime) (hN : IsPGroup p N)
    (hG : Prosupersolvable (ActionProduct J N))
    (Q : Subgroup J) (hQ : IsHallPro {r | r ≤ p} Q) :
    Function.Bijective (restrictH1 (N := N) (show Q ≤ ⊤ from le_top)) ∧
      (restrictH1 (N := N) (show Q ≤ ⊤ from le_top)) default = default := by sorry
Source
Michael C. Burkhart, Local conjugacy in prosolvable groups, arXiv:2609.37678v1 (29 September 2026), https://arxiv.org/pdf/2609.37678v1, p. 4, Proposition 2.3; standing conventions in §1.2, pp. 2–3.
Read-back

What the Lean code literally says, in plain math · GPT-6 family (exact model variant not exposed)

For every profinite group JJJ in universe uuu, every finite group NNN in universe vvv with the discrete topology, and every jointly continuous action of JJJ on NNN by group automorphisms, let ppp be a natural prime and assume that every n∈Nn\in Nn∈N satisfies npk=1n^{p^k}=1npk=1 for some k∈Nk\in\mathbb Nk∈N. Suppose that N⋊JN\rtimes JN⋊J, with multiplication (n,j)(n′,j′)=(n(j⋅n′),jj′)(n,j)(n',j')=(n(j\cdot n'),jj')(n,j)(n′,j′)=(n(j⋅n′),jj′) and the product topology, is prosupersolvable. Let Q≤JQ\le JQ≤J be closed, and assume that for every open normal subgroup UUU of JJJ, writing Q‾\overline QQ​ for the image of QQQ under J→J/UJ\to J/UJ→J/U, every prime dividing ∣Q‾∣|\overline Q|∣Q​∣ is at most ppp, and every prime dividing the index [J/U:Q‾][J/U:\overline Q][J/U:Q​] is greater than ppp. For A≤JA\le JA≤J, write H1(A,N)H^1(A,N)H1(A,N) for the set of continuous maps f:A→Nf:A\to Nf:A→N satisfying f(xy)=f(x)(x⋅f(y))f(xy)=f(x)(x\cdot f(y))f(xy)=f(x)(x⋅f(y)), modulo the equivalence relation f∼gf\sim gf∼g if there is one n∈Nn\in Nn∈N such that g(x)=n−1f(x)(x⋅n)g(x)=n^{-1}f(x)(x\cdot n)g(x)=n−1f(x)(x⋅n) for every x∈Ax\in Ax∈A; its distinguished element is the class of the constant map 111. Then the restriction map H1(J,N)→H1(Q,N)H^1(J,N)\to H^1(Q,N)H1(J,N)→H1(Q,N), [f]↦[f∣Q][f]\mapsto[f|_Q][f]↦[f∣Q​], is both injective and surjective, and sends the class of the constant map 111 to that same distinguished class. Its target is the whole cohomology set on QQQ. For a group RRR, the series condition used here means that there exist m∈Nm\in\mathbb Nm∈N and a nondecreasing sequence (Si)i∈N(S_i)_{i\in\mathbb N}(Si​)i∈N​ of normal subgroups of RRR such that S0={1}S_0=\{1\}S0​={1}, Sm=RS_m=RSm​=R, and, for each i<mi<mi<m, some ri∈Rr_i\in Rri​∈R satisfies Si+1=⟨Si,ri⟩S_{i+1}=\langle S_i,r_i\rangleSi+1​=⟨Si​,ri​⟩. Repeated terms are allowed, and m=0m=0m=0 is allowed precisely when RRR is trivial. Saying that RRR is prosupersolvable means that every quotient R/UR/UR/U by an open normal subgroup satisfies this series condition. The quotient groups J/UJ/UJ/U, their subgroup images, and their indices are finite here, so the natural-number cardinal and index conventions do not replace an infinite value by 000. A subgroup image of order 111 or index 111 imposes no prime-divisor condition on that number. Trivial JJJ or NNN are permitted; p=0p=0p=0 and p=1p=1p=1 are excluded by primality.

Human review
  • Endorsed by Shuze Chen · Sep 30, 2026

    Confirmed by the moderator at approval.

  • Endorsed by burkh4rt · Sep 30, 2026

    Confirmed by the mission captain (proposal self-audit).

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me