feat(Archive): dodecahedron, Petersen graph, 3-cube, and antipodal quotients#39650
feat(Archive): dodecahedron, Petersen graph, 3-cube, and antipodal quotients#39650RaggedR wants to merge 16 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.
…otients Defines the dodecahedron (Fin 20), Petersen graph (Fin 10), 3-cube Q₃ (Fin 8), and their antipodal quotient relationships. The Petersen graph is the quotient of the dodecahedron by the antipodal involution. The quotient of the 3-cube by bitwise complement is K₄.
|
Could a maintainer please add the |
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 fa782163d7
|
| Files | Import difference |
|---|---|
Mathlib.Combinatorics.SimpleGraph.Action (new file) |
644 |
Mathlib.Combinatorics.SimpleGraph.CosetGraph (new file) |
837 |
Mathlib.Combinatorics.SimpleGraph.Representation (new file) |
838 |
Mathlib.Combinatorics.SimpleGraph.Symmetric (new file) |
839 |
Mathlib.Combinatorics.SimpleGraph.QuotientGraph (new file) |
962 |
Declarations diff (regex)
+ GraphAction
+ IsArcTransitive
+ IsConnectionSet
+ IsLocallyTransitive
+ IsVertexTransitive
+ SimpleGraph.cosetGraph
+ SimpleGraph.quotientGraph
+ adj_mk
+ adj_smul_iff
+ applyWord'
+ applyWord'_mem
+ cG1
+ cG1F
+ cG1F_s
+ cG1I
+ cG1I_s
+ cG2
+ cG2F
+ cG2F_s
+ cG2I
+ cG2I_s
+ cGens
+ cGroup
+ cWit
+ cWitData
+ cWitData_s
+ cWit_ok
+ closureGraphAction
+ connectionSet
+ connectionSet_eq_doubleCoset
+ cosetQuotientMap
+ cosetQuotientMap_mk
+ cubeAdjBool
+ cubeAntipodalData
+ cubeAntipodalData_length
+ cubeAntipodalMap
+ cubeGraph
+ cubeGraph_edgeCount
+ cubeGraph_regular
+ cubeQuotientGraph
+ cubeQuotientGraph_regular
+ cubeQuotient_eq_top
+ cubeSabidussiIso
+ dG1
+ dG1F_s
+ dG1I_s
+ dG2
+ dG2F_s
+ dG2I_s
+ dGen1Fwd
+ dGen1Inv
+ dGen2Fwd
+ dGen2Inv
+ dGens
+ dGroup
+ dWit
+ dWitData
+ dWitData_s
+ dWit_ok
+ disjoint_stabilizer
+ dodecAdjBool
+ dodecAntipodalData
+ dodecAntipodalData_length
+ dodecAntipodalMap
+ dodecahedronGraph
+ dodecahedronGraph_edgeCount
+ dodecahedronGraph_regular
+ dodecahedronSabidussiIso
+ doubleCoset_isConnectionSet
+ double_coset_stable
+ expandConnectionSet
+ expandConnectionSet_isConnectionSet
+ genOrInv'
+ genOrInv'_mem
+ graphAction
+ instance : DecidableRel cubeGraph.Adj
+ instance : DecidableRel cubeQuotientGraph.Adj := by
+ instance : DecidableRel dodecahedronGraph.Adj
+ instance : DecidableRel petersenGraph.Adj := by
+ instance : GraphAction cGroup (Fin 8) cubeGraph
+ instance : GraphAction dGroup (Fin 20) dodecahedronGraph
+ instance : GraphAction pGroup (Fin 10) petersenGraph
+ instance : MulAction cGroup (Fin 8) := MulAction.compHom _ cGroup.subtype
+ instance : MulAction dGroup (Fin 20) := MulAction.compHom _ dGroup.subtype
+ instance : MulAction pGroup (Fin 10) := MulAction.compHom _ pGroup.subtype
+ instance : MulAction.IsPretransitive cGroup (Fin 8)
+ instance : MulAction.IsPretransitive dGroup (Fin 20)
+ instance : MulAction.IsPretransitive pGroup (Fin 10)
+ inv_eq_self_of_sq_eq_one
+ inv_mem
+ isArcTransitive_of_vertexTransitive_locallyTransitive
+ isConnectionSet
+ locallyTransitive_at_one
+ locallyTransitive_everywhere
+ lorimer_forward
+ lorimer_reverse
+ pG1
+ pG1F
+ pG1F_s
+ pG1I
+ pG1I_s
+ pG2
+ pG2F
+ pG2F_s
+ pG2I
+ pG2I_s
+ pGens
+ pGroup
+ pWD
+ pWD_s
+ pWit
+ pWit_ok
+ petersenGraph
+ petersenGraph_edgeCount
+ petersenGraph_regular
+ petersenSabidussiIso
+ quotient_cosetGraph_iso
+ sabidussiEquiv
+ sabidussiEquiv_smul
+ sabidussiEquiv_symm_mk
+ sabidussiIso
+ sabidussiSymmetricGraph
+ stabilizer_transitive_on_neighbors
+ toIso
+ toIso_apply
+ toIso_mul
+ toIso_symm
++ isVertexTransitive
++ one_not_mem
You can run this locally as follows
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>
## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.
Declarations diff (Lean -- pending)
Computed after the build finishes.
No changes to strong technical debt.
Increase in weak tech debt: (relative, absolute) = (5.00, 0.00)
| Current number | Change | Type (weak) |
|---|---|---|
| 4995 | 5 | exposed public sections |
Current commit fa782163d7
Reference commit 88d006abbc
This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary
- The
relativevalue is the weighted sum of the differences with weight given by the inverse of the current value of the statistic. - The
absolutevalue is therelativevalue divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).
|
Surely if Mathlib is to have graphs for specific polytopes, we should first have those polytopes? |
|
Could a maintainer please add the |
vihdzp
added
the
LLM-generated
Move `import Archive.NamedGraphs` after `MiuLanguage` entries to match the alphabetical ordering expected by `lake exe mk_all`.
|
LLM-generated |
themathqueen
added
the
blocked-by-other-PR
mathlib-dependent-issues
Bot
removed
the
blocked-by-other-PR
Add dodecahedronSabidussiIso and cubeSabidussiIso: both graphs are proved isomorphic to coset graphs via the Sabidussi representation theorem. - Dodecahedron: Sab(A₅, C₃, D), 20 = 60/3 vertices - Cube: Sab(S₄, C₃, D), 8 = 24/3 vertices Generators computed by GAP (GRAPE AutGroupGraph), BFS witness words verify transitivity. GraphAction proved via closure_induction with the finiteness argument for inverses.
Add petersenSabidussiIso: the Petersen graph (defined as the antipodal quotient of the dodecahedron) is isomorphic to a coset graph via the Sabidussi representation theorem. S₅ (order 120) acts vertex-transitively with stabilizer S₂×S₃: petersenGraph ≃g Sab(S₅, S₂×S₃, D) with 10 = 120/12 vertices. Generators computed by GAP (GRAPE AutGroupGraph).
4c520ce to
338b7d8
Compare
|
Please add the |
|
This pull request is now in draft mode. No active bors state needed cleanup. While this PR remains draft, bors will ignore commands on this PR. Mark it ready for review before using commands like |
|
This pull request has conflicts, please merge |
mathlib-merge-conflicts
Bot
added
the
merge-conflict
mathlib-merge-conflicts
Bot
removed
the
merge-conflict
GitHub Actions
Inactive
|
This pull request has conflicts, please merge |
mathlib-merge-conflicts
Bot
added
the
merge-conflict
…-archive # Conflicts: # Mathlib.lean
github-actions
Bot
removed
the
merge-conflict
|
This pull request has conflicts, please merge |
mathlib-merge-conflicts
Bot
added
the
merge-conflict
3 participants
This defines the dodecahedron graph (Fin 20, 3-regular, 30 edges), the Petersen graph (Fin 10, as the antipodal quotient of the dodecahedron), and the 3-cube Q₃ (Fin 8, 3-regular, 12 edges) with its antipodal quotient proved equal to K₄.
The Petersen graph is defined as
dodecahedronGraph.quotientGraph dodecAntipodalMap, using the quotient graph infrastructure from #39551. The antipodal involution on the dodecahedron identifies each vertex with the vertex at distance 5 (diametrically opposite). The 3-cube's antipodal involution (bitwise complement) quotients to K₄ = ⊤.The graph definitions and quotient constructions follow Langer, arXiv:1306.4798.
Depends on #39551 (quotient graphs and Lorimer's theorem).
LLM tools were used to assist with Lean formalization. The mathematical content is the author's own work.