Papers With

← All papers
First page of Sylow synchronization in finite groups: the good case

Sylow synchronization in finite groups: the good case

Hong Yi Huang, Francesca Lisi, Aluna Rizzoli, Luca Sabatini

math.GR Sep 23, 2026 · v1
formalization mathlib algebra
Read PDF arXiv abstract Code
TL;DR
All results, including Sylow synchronization for solvable groups and symmetric/alternating groups, are formalized in Lean 4 with mathlib, archived on Zenodo.
Abstract
Let $G$ be a finite solvable group such that, for any prime $p$ and any quotient $Q$ of $G$, there are two Sylow $p$-subgroups of $Q$ intersecting in $O_p(Q)$. Then, for every family $(P_i)_{i=1}^n$ of Sylow subgroups of $G$ for distinct primes $p_1,\ldots,p_n$, there exists $x \in G$ such that $P_i \cap P_i^x = O_{p_i}(G)$ for all $i$. This covers groups of odd order, partially settling a conjecture of the second and fourth authors and unifying old results of Bialostocki and Mann on the intersection of nilpotent subgroups. We also prove a result for all symmetric and alternating groups, completing the proof of the conjecture for simple groups as initiated by Burness and the first author.
Problem

Conjecture A (Kourovka Notebook Question 21.26) asserts that for Sylow subgroups P_i of a finite group for distinct primes, a single conjugating element x makes every intersection P_i ∩ P_i^x inclusion-minimal. Groups of odd order and the alternating groups were the main open cases.

Approach

The authors handle the 'good case': solvable groups in which every quotient has two Sylow p-subgroups meeting in O_p, for every prime p. The argument works with modules and centralizers in solvable groups. For symmetric and alternating groups they use a probabilistic union bound on Sylow intersection probabilities, with explicit combinatorial estimates for n>40 and Magma computations for n≤40. All results are formalized in Lean 4 using mathlib.

Results

Conjecture A holds for finite solvable groups whose quotients all satisfy (*). In particular it holds for groups of odd order, which resolves Conjecture C on nilpotent subgroups lying in F(G). It also holds for all symmetric and alternating groups, which completes the conjecture for simple groups.