Prove2Me

Local conjugacy inside the subgroup generated by supplements

Proved
LocalConjugacy.Proof.LocalConjugacy.locallyConjugate_generated_profinite

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

group-theorylocal-conjugacylocal-conjugacy-prosolvableprofinite-groupssylow-theory

Let GG be a profinite group, let pp be prime, and let N⊴GN\trianglelefteq G be an algebraic pp-group. Let H,K≤GH,K\le G be closed subgroups with G=NH=NKG=NH=NK, and suppose L=⟨H,K⟩L=\langle H,K\rangle is also closed. Suppose a subgroup P≤GP\le G is simultaneously a Sylow pro-pp subgroup of HH and of KK. Then HH and KK, regarded as subgroups of LL, are locally conjugate:

∀q prime,∃A∈Syl⁡qpro(H), B∈Syl⁡qpro(K), g∈L,gAg−1=B.\forall q\text{ prime},\quad\exists A\in\operatorname{Syl}^{\mathrm{pro}}_q(H),\ B\in\operatorname{Syl}^{\mathrm{pro}}_q(K),\ g\in L,\qquad gAg^{-1}=B.

Here algebraic pp-group means every element has order a power of pp. This places the local conjugators inside the subgroup generated by the two supplements.

Preamble
import Definitions.Def_LocalConjugacy_Groups
import Definitions.Def_LocalConjugacy_Cohomology
import Definitions.Def_LocalConjugacy_Examples
import Definitions.Def_LocalConjugacy_Proof_Definitions
import Definitions.Def_LocalConjugacy_Proof_Bridges
import Definitions.Def_LocalConjugacy_Proof_Counterexamples_Heisenberg
import Definitions.Def_LocalConjugacy_Proof_Counterexamples_HeisenbergStructure
import Definitions.Def_LocalConjugacy_Proof_Counterexamples_HeisenbergSupersolvable
import Definitions.Def_LocalConjugacy_Proof_ConcreteGroups
import Definitions.Def_LocalConjugacy_Targets
import Definitions.Def_LocalConjugacy_Proof_Compactness
import Definitions.Def_LocalConjugacy_Proof_ProfiniteSylow
import Definitions.Def_LocalConjugacy_Proof_StructuralImages
import Definitions.Def_LocalConjugacy_Proof_FiniteAbelianCohomology
import Definitions.Def_LocalConjugacy_Proof_AbelianComplement
import Definitions.Def_LocalConjugacy_Proof_QuotientReduction
import Definitions.Def_LocalConjugacy_Proof_Cohomology
import Definitions.Def_LocalConjugacy_Proof_InvariantRestriction
import Definitions.Def_LocalConjugacy_Proof_CocycleActions
import Definitions.Def_LocalConjugacy_Proof_CoprimeCohomology
import Definitions.Def_LocalConjugacy_Proof_CocycleDescent
import Definitions.Def_LocalConjugacy_Proof_CocycleZorn
import Definitions.Def_LocalConjugacy_Proof_CocycleProducts
import Definitions.Def_LocalConjugacy_Proof_FiniteCoefficientSubgroup
import Definitions.Def_LocalConjugacy_Proof_CocycleInvarianceSubgroup
import Definitions.Def_LocalConjugacy_Proof_CocycleInjectivity
import Definitions.Def_LocalConjugacy_Proof_CocycleRebase
import Definitions.Def_LocalConjugacy_Proof_FiniteHall
import Definitions.Def_LocalConjugacy_Proof_SupersolvableStructure
import Definitions.Def_LocalConjugacy_Proof_ProfiniteHall
import Definitions.Def_LocalConjugacy_Proof_ActionProductTopology
import Definitions.Def_LocalConjugacy_Proof_HallCohomology
import Definitions.Def_LocalConjugacy_Proof_SupersolvableRestriction
import Definitions.Def_LocalConjugacy_Proof_NilpotentCoefficients
import Definitions.Def_LocalConjugacy_Proof_NonabelianComplement
import Definitions.Def_LocalConjugacy_Proof_ComplementSupersolvable
import Definitions.Def_LocalConjugacy_Proof_Counterexamples_Quaternion
import Definitions.Def_LocalConjugacy_Proof_QuaternionCohomology
import Definitions.Def_LocalConjugacy_Proof_QuaternionMatrices
import Definitions.Def_LocalConjugacy_Proof_QuaternionAction
import Definitions.Def_LocalConjugacy_Proof_QuaternionComplements

universe u_1
Formal statement
theorem LocalConjugacy.Proof.LocalConjugacy.locallyConjugate_generated_profinite :
∀ {G : Type u_1} [inst : Group.{u_1} G] [inst_1 : TopologicalSpace.{u_1} G]
  [@LocalConjugacy.Proof.LocalConjugacy.Profinite.{u_1} G inst inst_1] (N H K P : @Subgroup.{u_1} G inst)
  [@Subgroup.Normal.{u_1} G inst N]
  (hH :
    @IsClosed.{u_1} G inst_1
      (@SetLike.coe.{u_1, u_1} (@Subgroup.{u_1} G inst) G (@Subgroup.instSetLike.{u_1} G inst) H))
  (hK :
    @IsClosed.{u_1} G inst_1
      (@SetLike.coe.{u_1, u_1} (@Subgroup.{u_1} G inst) G (@Subgroup.instSetLike.{u_1} G inst) K))
  (hL :
    @IsClosed.{u_1} G inst_1
      (@SetLike.coe.{u_1, u_1} (@Subgroup.{u_1} G inst) G (@Subgroup.instSetLike.{u_1} G inst)
        (@Max.max.{u_1} (@Subgroup.{u_1} G inst)
          (@SemilatticeSup.toMax.{u_1} (@Subgroup.{u_1} G inst)
            (@Lattice.toSemilatticeSup.{u_1} (@Subgroup.{u_1} G inst)
              (@ConditionallyCompleteLattice.toLattice.{u_1} (@Subgroup.{u_1} G inst)
                (@CompleteLattice.toConditionallyCompleteLattice.{u_1} (@Subgroup.{u_1} G inst)
                  (@Subgroup.instCompleteLattice.{u_1} G inst)))))
          H K)))
  {p : Nat} [Fact (Nat.Prime p)]
  (hN :
    @IsPGroup.{u_1} p
      (@Subtype.{u_1 + 1} G fun (x : G) =>
        @Membership.mem.{u_1, u_1} G (@Subgroup.{u_1} G inst)
          (@SetLike.instMembership.{u_1, u_1} (@Subgroup.{u_1} G inst) G (@Subgroup.instSetLike.{u_1} G inst)) N x)
      (@Subgroup.toGroup.{u_1} G inst N))
  (hsH : @LocalConjugacy.Proof.LocalConjugacy.Supplements.{u_1} G inst N H)
  (hsK : @LocalConjugacy.Proof.LocalConjugacy.Supplements.{u_1} G inst N K)
  (hPH : @LocalConjugacy.Proof.LocalConjugacy.IsSylowPro.{u_1} p G inst inst_1 H P)
  (hPK : @LocalConjugacy.Proof.LocalConjugacy.IsSylowPro.{u_1} p G inst inst_1 K P),
  @LocalConjugacy.Proof.LocalConjugacy.LocallyConjugate.{u_1}
    (@Subtype.{u_1 + 1} G fun (x : G) =>
      @Membership.mem.{u_1, u_1} G (@Subgroup.{u_1} G inst)
        (@SetLike.instMembership.{u_1, u_1} (@Subgroup.{u_1} G inst) G (@Subgroup.instSetLike.{u_1} G inst))
        (@Max.max.{u_1} (@Subgroup.{u_1} G inst)
          (@SemilatticeSup.toMax.{u_1} (@Subgroup.{u_1} G inst)
            (@Lattice.toSemilatticeSup.{u_1} (@Subgroup.{u_1} G inst)
              (@ConditionallyCompleteLattice.toLattice.{u_1} (@Subgroup.{u_1} G inst)
                (@CompleteLattice.toConditionallyCompleteLattice.{u_1} (@Subgroup.{u_1} G inst)
                  (@Subgroup.instCompleteLattice.{u_1} G inst)))))
          H K)
        x)
    (@Subgroup.toGroup.{u_1} G inst
      (@Max.max.{u_1} (@Subgroup.{u_1} G inst)
        (@SemilatticeSup.toMax.{u_1} (@Subgroup.{u_1} G inst)
          (@Lattice.toSemilatticeSup.{u_1} (@Subgroup.{u_1} G inst)
            (@ConditionallyCompleteLattice.toLattice.{u_1} (@Subgroup.{u_1} G inst)
              (@CompleteLattice.toConditionallyCompleteLattice.{u_1} (@Subgroup.{u_1} G inst)
                (@Subgroup.instCompleteLattice.{u_1} G inst)))))
        H K))
    (@instTopologicalSpaceSubtype.{u_1} G
      (fun (x : G) =>
        @Membership.mem.{u_1, u_1} G (@Subgroup.{u_1} G inst)
          (@SetLike.instMembership.{u_1, u_1} (@Subgroup.{u_1} G inst) G (@Subgroup.instSetLike.{u_1} G inst))
          (@Max.max.{u_1} (@Subgroup.{u_1} G inst)
            (@SemilatticeSup.toMax.{u_1} (@Subgroup.{u_1} G inst)
              (@Lattice.toSemilatticeSup.{u_1} (@Subgroup.{u_1} G inst)
                (@ConditionallyCompleteLattice.toLattice.{u_1} (@Subgroup.{u_1} G inst)
                  (@CompleteLattice.toConditionallyCompleteLattice.{u_1} (@Subgroup.{u_1} G inst)
                    (@Subgroup.instCompleteLattice.{u_1} G inst)))))
            H K)
          x)
      inst_1)
    (@Subgroup.subgroupOf.{u_1} G inst H
      (@Max.max.{u_1} (@Subgroup.{u_1} G inst)
        (@SemilatticeSup.toMax.{u_1} (@Subgroup.{u_1} G inst)
          (@Lattice.toSemilatticeSup.{u_1} (@Subgroup.{u_1} G inst)
            (@ConditionallyCompleteLattice.toLattice.{u_1} (@Subgroup.{u_1} G inst)
              (@CompleteLattice.toConditionallyCompleteLattice.{u_1} (@Subgroup.{u_1} G inst)
                (@Subgroup.instCompleteLattice.{u_1} G inst)))))
        H K))
    (@Subgroup.subgroupOf.{u_1} G inst K
      (@Max.max.{u_1} (@Subgroup.{u_1} G inst)
        (@SemilatticeSup.toMax.{u_1} (@Subgroup.{u_1} G inst)
          (@Lattice.toSemilatticeSup.{u_1} (@Subgroup.{u_1} G inst)
            (@ConditionallyCompleteLattice.toLattice.{u_1} (@Subgroup.{u_1} G inst)
              (@CompleteLattice.toConditionallyCompleteLattice.{u_1} (@Subgroup.{u_1} G inst)
                (@Subgroup.instCompleteLattice.{u_1} G inst)))))
        H K)) := by sorry
Source
Michael C. Burkhart, Local conjugacy in prosolvable groups, https://arxiv.org/abs/2609.37678; supporting formalization lemma, LocalConjugacy/FiniteKernelSylow.lean, lines 81–109; source SHA-256 4cc6aa4c9f883bff52303e9074afbc77e4bc971fe7011f4acd9a1dbc91af24b7.

View graph