Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Subgroups of small index in the symmetric group

Lax461425.DixonMortimer · concepts/Lax461425/DixonMortimer.lean · lax-461425

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    Let n≥20n \geq 20 and 1≤r≤n/21 \leq r \leq n/2. If H≤SymnH \leq \mathrm{Sym}_n has index less than min⁡{12(n⌊n/2⌋),(nr)}\min\{\frac12\binom{n}{\lfloor n/2\rfloor}, \binom{n}{r}\}, then Alt(T)≤H\mathbf{Alt}_{(T)} \leq H for some T⊆[n]T \subseteq [n] with ∣T∣<r|T| < r, where Alt(T)\mathbf{Alt}_{(T)} is the pointwise stabiliser of TT in the alternating group.

    This is cf. Dixon and Mortimer, Theorem 5.2B. The paper states it for n≥9n \geq 9; the case n≥20n \geq 20 stated here is the one used in the support theorem, which assumes n≥20n \geq 20.

    Concept map
    1 concept
    100%
    Proven claimThis concept
    Evidence

    Each proof establishes this claim relative to its assumptions.

    Lean source view on GitHub

    1import Mathlib.GroupTheory.SpecificGroups.Alternating
    2import Mathlib.GroupTheory.GroupAction.FixingSubgroup
    3import Mathlib.GroupTheory.Index
    4
    5/-!
    6---
    7title: Subgroups of small index in the symmetric group
    8type: theorem
    9---
    10Let n≥20n \geq 20 and 1≤r≤n/21 \leq r \leq n/2. If H≤SymnH \leq \mathrm{Sym}_n has index less than
    11min⁡{12(n⌊n/2⌋),(nr)}\min\{\frac12\binom{n}{\lfloor n/2\rfloor}, \binom{n}{r}\}, then
    12Alt(T)≤H\mathbf{Alt}_{(T)} \leq H for some T⊆[n]T \subseteq [n] with ∣T∣<r|T| < r, where
    13Alt(T)\mathbf{Alt}_{(T)} is the pointwise stabiliser of TT in the alternating group.
    14
    15This is cf. Dixon and Mortimer, Theorem 5.2B. The paper states it for n≥9n \geq 9; the
    16case n≥20n \geq 20 stated here is the one used in the support theorem, which assumes
    17n≥20n \geq 20.
    18-/
    19
    20namespace Lax461425.DixonMortimer
    21
    22open Equiv
    23
    24/-- A subgroup of `Sym n` of small index contains the pointwise stabiliser, in the
    25alternating group, of fewer than `r` points. -/
    26axiom exists_fixingSubgroup_inf_alternatingGroup_le {n r : ℕ} (hn : 20 ≤ n) (hr : 1 ≤ r)
    27 (hrn : 2 * r ≤ n) (H : Subgroup (Perm (Fin n)))
    28 (hhalf : 2 * H.index < n.choose (n / 2)) (hr' : H.index < n.choose r) :
    29 ∃ T : Set (Fin n), T.ncard < r ∧
    30 fixingSubgroup (Perm (Fin n)) T ⊓ alternatingGroup (Fin n) ≤ H
    31
    32end Lax461425.DixonMortimer
    33
    Show Proof
    Builds on

    none

    Used by

    none

    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…