Proposition 3.1
ProvedLocalConjugacy.proposition_3_1Given and satisfying the hypotheses of Theorem 1.1 where is finite, two closed complements of are conjugate if and only if they are locally conjugate.
Here Theorem 1.1 requires that be profinite, be a closed normal pronilpotent subgroup, and either be prosupersolvable or be pronilpotent. This proposition additionally requires finite and both subgroups to be closed complements of .
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
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 sorryRead-back
What the Lean code literally says, in plain math · GPT-6 family (exact model variant not exposed)
For every profinite group in universe and closed subgroups , assume that is a finite normal subgroup of and pronilpotent, and that either is prosupersolvable or is pronilpotent. Assume that every element of has a unique expression with and also a unique expression with . Then there exists with if and only if, for every natural prime , there exist a Sylow pro- subgroup of , a Sylow pro- subgroup of , and with . A Sylow pro- subgroup of a subgroup means a subgroup that is closed in , for which every quotient by an open normal subgroup of has the property that every element is killed by some power with , and that is maximal under inclusion among the closed subgroups of contained in with this quotient property. Saying that a topological group is pronilpotent means that is nilpotent for every open normal subgroup of , with the subgroup and quotient topologies understood. For a group , the series condition used here means that there exist and a nondecreasing sequence of normal subgroups of such that , , and, for each , some satisfies . Repeated terms are allowed, and is allowed precisely when is trivial. Saying that is prosupersolvable means that every quotient by an open normal subgroup satisfies this series condition. The two unique-product assumptions include . The groups need not be finite. Trivial 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.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.