Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Proposition 3.1

Proved
LocalConjugacy.proposition_3_1

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

group-theorylocal-conjugacynonabelian-cohomologyprofinite-groups

Given NNN and GGG satisfying the hypotheses of Theorem 1.1 where NNN is finite, two closed complements of NNN are conjugate if and only if they are locally conjugate.

Here Theorem 1.1 requires that GGG be profinite, NNN be a closed normal pronilpotent subgroup, and either GGG be prosupersolvable or G/NG/NG/N be pronilpotent. This proposition additionally requires NNN finite and both subgroups to be closed complements of NNN.

Preamble
import Definitions.Def_LocalConjugacy_Groups

/-
Proposition 3.1: in the arXiv version N is finite. Both H and K are actual
complements, expressed with Mathlib’s standard subgroup complement predicate.

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_3_1 {G : ProfiniteGrp.{u}} (N H K : Subgroup G) [N.Normal] [Finite N]
    (hN : IsClosed (N : Set G)) (hH : IsClosed (H : Set G))
    (hK : IsClosed (K : Set G)) (hpron : Pronilpotent N)
    (hcase : Prosupersolvable G ∨ Pronilpotent (G ⧸ N))
    (hNH : N.IsComplement' H) (hNK : N.IsComplement' K) :
    Conjugate H K ↔ LocallyConjugate H K := by sorry
Source
Michael C. Burkhart, Local conjugacy in prosolvable groups, arXiv:2609.37678v1 (29 September 2026), https://arxiv.org/pdf/2609.37678v1, p. 6, Proposition 3.1; 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 GGG in universe uuu and closed subgroups N,H,K≤GN,H,K\le GN,H,K≤G, assume that NNN is a finite normal subgroup of GGG and pronilpotent, and that either GGG is prosupersolvable or G/NG/NG/N is pronilpotent. Assume that every element of GGG has a unique expression nhnhnh with n∈N,h∈Hn\in N,h\in Hn∈N,h∈H and also a unique expression n′kn'kn′k with n′∈N,k∈Kn'\in N,k\in Kn′∈N,k∈K. Then there exists g∈Gg\in Gg∈G with gHg−1=KgHg^{-1}=KgHg−1=K if and only if, for every natural prime ppp, there exist a Sylow pro-ppp subgroup PPP of HHH, a Sylow pro-ppp subgroup QQQ of KKK, and gp∈Gg_p\in Ggp​∈G with gpPgp−1=Qg_pPg_p^{-1}=Qgp​Pgp−1​=Q. A Sylow pro-ppp subgroup PPP of a subgroup A≤GA\le GA≤G means a subgroup P≤AP\le AP≤A that is closed in GGG, for which every quotient P/UP/UP/U by an open normal subgroup of PPP has the property that every element is killed by some power pkp^kpk with k∈Nk\in\mathbb Nk∈N, and that is maximal under inclusion among the closed subgroups of GGG contained in AAA with this quotient property. Saying that a topological group RRR is pronilpotent means that R/UR/UR/U is nilpotent for every open normal subgroup UUU of RRR, with the subgroup and quotient topologies understood. 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 two unique-product assumptions include N∩H=N∩K={1}N\cap H=N\cap K=\{1\}N∩H=N∩K={1}. The groups G,H,KG,H,KG,H,K need not be finite. Trivial NNN and trivial other groups are permitted, all primes are included even when the relevant Sylow subgroups are trivial, and the local choices may vary with the prime.

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