Corollary 1.4

Proved

LocalConjugacy.corollary_1_4

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

group-theorylocal-conjugacynonabelian-cohomologyprofinite-groups

Suppose a profinite semidirect product $G=N\rtimes J$ acts transitively on some nonempty set $\Omega$ with closed point stabilizers $\{G_\alpha\}_{\alpha\in\Omega}$ , where $N$ is pronilpotent and either $G$ is prosupersolvable or $J$ is pronilpotent. If $N_\alpha\trianglelefteq N$ for some $\alpha\in\Omega$ , and for each prime $p$ , a Sylow $p$ -subgroup of $J$ fixes an element of $\Omega$ , then $J$ fixes an element of $\Omega$ .

Preamble

import Definitions.Def_LocalConjugacy_Groups

/-
Corollary 1.4: Ω is nonempty and carries no topology. The action is transitive
and its point stabilizers are closed; the local fixed points may depend on p.

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.corollary_1_4 {G : ProfiniteGrp.{u}} {Ω : Type v} [MulAction G Ω] [Nonempty Ω]
    (N J : Subgroup G) (hN : IsClosed (N : Set G)) (hJ : IsClosed (J : Set G))
    (hsplit : Splits N J) (hpron : Pronilpotent N)
    (hcase : Prosupersolvable G ∨ Pronilpotent J)
    (htrans : MulAction.IsPretransitive G Ω)
    (hclosed : ∀ x : Ω, IsClosed (MulAction.stabilizer G x : Set G))
    (hnormal : ∃ x : Ω, IntersectionNormal N (MulAction.stabilizer G x))
    (hlocal : SylowFixedPoints (Ω := Ω) J) : HasFixedPoint (Ω := Ω) J := by sorry

Source

Michael C. Burkhart, Local conjugacy in prosolvable groups, arXiv:2609.37678v1 (29 September 2026), https://arxiv.org/pdf/2609.37678v1, p. 2, Corollary 1.4; 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 $G$ in universe $u$ , every nonempty set $\Omega$ in universe $v$ with a $G$ -action, and closed subgroups $N,J\le G$ , assume that $N$ is normal in $G$ , every element of $G$ has a unique expression $nj$ with $n\in N,j\in J$ , $N$ is pronilpotent, and either $G$ is prosupersolvable or $J$ is pronilpotent. Assume that the action is transitive, meaning that for any $x,y\in\Omega$ some $g\in G$ satisfies $g\cdot x=y$ ; that the stabilizer $G_x=\{g\in G:g\cdot x=x\}$ is closed in $G$ for every $x\in\Omega$ ; and that there exists at least one $x\in\Omega$ for which $N\cap G_x$ is normal as a subgroup of $N$ . Finally, assume that for every natural prime $p$ there exist a Sylow pro- $p$ subgroup $P_p$ of $J$ and a point $x_p\in\Omega$ fixed by every element of $P_p$ . Then there exists a point $x\in\Omega$ fixed by every element of $J$ . A Sylow pro- $p$ subgroup $P$ of a subgroup $A\le G$ means a subgroup $P\le A$ that is closed in $G$ , for which every quotient $P/U$ by an open normal subgroup of $P$ has the property that every element is killed by some power $p^k$ with $k\in\mathbb N$ , and that is maximal under inclusion among the closed subgroups of $G$ contained in $A$ with this quotient property. Saying that a topological group $R$ is pronilpotent means that $R/U$ is nilpotent for every open normal subgroup $U$ of $R$ , with the subgroup and quotient topologies understood. For a group $R$ , the series condition used here means that there exist $m\in\mathbb N$ and a nondecreasing sequence $(S_i)_{i\in\mathbb N}$ of normal subgroups of $R$ such that $S_0=\{1\}$ , $S_m=R$ , and, for each $i<m$ , some $r_i\in R$ satisfies $S_{i+1}=\langle S_i,r_i\rangle$ . Repeated terms are allowed, and $m=0$ is allowed precisely when $R$ is trivial. Saying that $R$ is prosupersolvable means that every quotient $R/U$ by an open normal subgroup satisfies this series condition. The points $x_p$ and the subgroups $P_p$ may depend on $p$ , and they need not be related to the point witnessing the intersection-normality hypothesis. No topology on $\Omega$ is specified; the topological action hypothesis here is the closedness of every stabilizer. Singleton $\Omega$ and trivial groups are allowed, but empty $\Omega$ is excluded. All natural primes are included, even when their Sylow subgroups are trivial.

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