Theorem 5.9: B_n/G is rank-symmetric, rank-unimodal, and Sperner #
Formalization of Theorem 5.9 from Stanley's Algebraic Combinatorics.
Copyright (c) 2025. All rights reserved. Released under Apache 2.0 license.
Complement lemmas #
Helper #
The quotient raising operator #
Embed orbit-level functions into level-i functions on B_n.
Given f on level-i orbits, define g : Level n i → ℝ by g(⟨S, hS⟩) = f([S]).
Instances For
The quotient raising operator Û_i, defined by embedding into Level n i → ℝ,
applying BooleanUpDown.up i, and evaluating at an orbit representative.
Instances For
quotientUp i as a linear map.
Instances For
embedOrbits is G-invariant: the value at ⟨S, hS⟩ depends only on the orbit
of S, since f is a function on orbits.
The up operator preserves G-invariance: if v : Level n i → ℝ is constant
on orbits, then up i v : Level n (i+1) → ℝ is also constant on orbits.
Theorem 5.9 (order-raising matchings).
Theorem 5.9 (order-lowering).
Theorem 5.9 (unimodality).
Theorem 5.9 (Sperner).
Nonisomorphic graph counts — unimodality and Sperner property #
The edge set of the complete graph K_m has C(m,2) elements.
The symmetric group S_m acts on this edge set by permuting vertices.
The quotient B_{C(m,2)} / S_m is the poset of isomorphism classes of simple
graphs on m vertices ordered by "is a subgraph of" (up to isomorphism).
(a) The sequence p_0, p_1, ..., p_{C(m,2)} of numbers of
nonisomorphic simple graphs with i edges is symmetric and unimodal.
(b) The poset of isomorphism classes has the Sperner property:
the maximum antichain consists of all graphs with ⌊C(m,2)/2⌋ edges.
Proof: The symmetric group S_m acts on E = C([m],2) by permuting vertices.
The quotient poset B_E / S_m is the poset of isomorphism classes of simple
graphs on m vertices. Apply Theorem 5.9.
The number of edges in the complete graph K_m, i.e., C(m,2).
Instances For
The type of 2-element subsets of Fin m, representing potential edges of
a simple graph on m vertices.
Instances For
Equivalence between 2-element subsets and elements of powersetCard 2.
Instances For
The action of Equiv.Perm (Fin m) on Finset (Fin m) preserves cardinality,
and therefore restricts to an action on 2-element subsets.
The 2-element subsets of Fin m have cardinality m.choose 2.
Bijection between EdgeSubsets m and Fin (edgeCount m).
Instances For
The group homomorphism from S_m to S_{C(m,2)} induced by the action
of S_m on 2-element subsets (edges). This sends a vertex permutation
σ to the induced edge permutation σ̂({i,j}) = {σ(i), σ(j)}.
Instances For
The subgroup of S_{C(m,2)} induced by the action of S_m on edges.
This is the image of S_m under the edge action homomorphism.
Instances For
The quotient poset of graph isomorphism classes on m vertices.
Elements are orbits of S_m acting on subsets of edges (i.e., simple graphs),
ordered by [H] ≤ [G] iff H is isomorphic to a subgraph of G.
Instances For
Theorem 5.10(a), symmetry part. The sequence p_0, p_1, ..., p_{C(m,2)}
is symmetric: p_i = p_{C(m,2) - i} for all 0 ≤ i ≤ C(m,2).
Theorem 5.10(a), unimodality part. The sequence p_0, p_1, ..., p_{C(m,2)}
is unimodal.
Theorem 5.10(b). The poset of isomorphism classes of simple graphs on
m vertices has the Sperner property: the maximum antichain size equals
the maximum level size, which is attained at graphs with ⌊C(m,2)/2⌋ edges.
For a rank-symmetric and rank-unimodal graded poset of rank n,
the maximum rank count is achieved at the middle level ⌊n/2⌋.
This follows because unimodality provides a peak level j, and symmetry
forces the value at ⌊n/2⌋ to equal the peak value.
Theorem 5.10(b), explicit maximizer. The maximum antichain in the graph
isomorphism poset is achieved at level ⌊C(m,2)/2⌋, i.e., the set of all
nonisomorphic graphs with ⌊C(m,2)/2⌋ edges forms a maximum antichain.