feat(Combinatorics/SimpleGraph): Sabidussi representation theorem#39550
feat(Combinatorics/SimpleGraph): Sabidussi representation theorem#39550RaggedR wants to merge 5 commits into
Conversation
This adds the first connection between Mathlib's `MulAction` and `SimpleGraph` libraries, defining what it means for a group action to preserve adjacency and providing the standard transitivity predicates used in algebraic graph theory. The `GraphAction` class asserts that `g • u` is adjacent to `g • v` whenever `u` is adjacent to `v`. For group actions this is automatically an iff (`adj_smul_iff`), and each group element induces a graph isomorphism (`toIso`). On top of this, `IsVertexTransitive` combines `GraphAction` with `IsPretransitive`, and `IsArcTransitive` requires transitivity on ordered adjacent pairs. The main result is the characterization theorem: a vertex-transitive graph that is locally transitive (the stabilizer of each vertex acts transitively on its neighbors) is arc-transitive, and conversely an arc-transitive graph with no isolated vertices is vertex-transitive. This is the standard equivalence between arc-transitivity and the combination of vertex-transitivity with local transitivity, used throughout the theory of symmetric graphs.
github-actions
Bot
added
the
new-contributor
Welcome new contributor!Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests. We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR. Thank you again for joining our community. |
PR summary f81a6d70f0Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
SnirBroshi
added
the
LLM-generated
2 participants
This proves Sabidussi's representation theorem: every vertex-transitive graph is isomorphic to a coset graph. The proof constructs, for any basepoint
vin a graph with a transitive graph action, an explicit graph isomorphismΓ ≃g Sab(G, Gᵥ, D)whereGᵥis the stabilizer ofvandD = {g ∈ G : Γ.Adj v (g • v)}is the connection set.The connection set
Dis shown to satisfy theIsConnectionSetaxioms for the stabilizer subgroup: it is stable under left and right multiplication by stabilizer elements (since the stabilizer fixesvand the action preserves adjacency), closed under inversion (since the graph is undirected), and disjoint from the stabilizer (since the graph has no loops). The orbit-stabilizer equivalenceV ≃ G ⧸ Gᵥis then shown to preserve adjacency in both directions, completing the isomorphism.Together with the coset graph construction from #39548, this gives a complete classification of vertex-transitive graphs up to isomorphism.
Depends on
#39548
AI disclosure
The definitions and proofs are from my honours thesis (Symmetric Graphs and their Quotients, arXiv:1306.4798). The Lean formalization was developed collaboratively with Claude Code (Anthropic's coding assistant), which helped with tactic selection, Mathlib API navigation, and porting the mathematical content into idiomatic Lean 4. All mathematical content was verified by me and the proofs compile without sorry.