feat(Combinatorics): add Schreier graph definition and covering property#36320
feat(Combinatorics): add Schreier graph definition and covering property#36320ZRTMRH wants to merge 8 commits intoleanprover-community:masterfrom
Conversation
PR summary caa79c2e3cImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
github-actions
bot
added
t-combinatorics
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. |
grunweg
added
the
LLM-generated
YaelDillies
added
the
awaiting-author
Add informal mathematical definition to module docstring and change SchreierGraph from a def type alias to a one-field structure per mathlib convention. Co-Authored-By: Claude Opus 4.6 <[email protected]>
YaelDillies
left a comment
YaelDillies
left a comment
There was a problem hiding this comment.
Shouldn't everything past the definition of SchreierGraph be moved to the SchreierGraph namespace?
…space Move definitions and lemmas about `SchreierGraph` into the `SchreierGraph` namespace. Co-Authored-By: Claude Opus 4.6 <[email protected]>
Moved to the SchreierGraph namespace. |
…raph Name the structure constructor `ofVertex`, reword a docstring, and rename `schreierGraphMulAction` to `instMulAction`. Co-Authored-By: Claude Opus 4.6 <[email protected]>
|
All suggestions other than V naming (explained in previous reply) are addressed. Ready for re-review. |
|
in the future, please remove the -awaiting-author |
github-actions
bot
removed
the
awaiting-author
YaelDillies
left a comment
YaelDillies
left a comment
There was a problem hiding this comment.
Unfortunately, I don't know the first thing about Schreier graphs. Could you please contact a more appropriate reviewer? Thanks!
…elling Replace `labelling_star_bijective` and `labelling_costar_bijective` with `labelling_starEquiv` and `labelling_costarEquiv`, providing explicit equivalences. Golf tactic proofs per reviewer suggestions. Co-Authored-By: Claude Opus 4.6 <[email protected]>
|
Thanks a lot for the code review! I'll post on zulip. |
|
|
||
| ## Main definitions | ||
|
|
||
| * `SchreierGraph V ι` - The Schreier graph of an action, with vertices of type `V` and edges |
There was a problem hiding this comment.
Since it is a quiver, maybe let's depart from terminology and call it a SchreierQuiver?
There was a problem hiding this comment.
I prefer to leave as it is. Schreier graph by definition has a labeled directed structure, so it is inherently always a quiver (and should not be formalized in simple graph structure, for instance). Thus I don't think we need to save the name of SchreierGraph and this could make it more discoverable. Happy to change if you feel strongly though.
- Add math literature reference (Vorobets 2012) to module docstring and references.bib - Remove redundant hypotheses from `equiv` (use section variables) - Move `instMulAction` to separate section with `Monoid M` instead of `Group M` - Remove explicit name from `instMulAction` instance - Make `V` implicit in GroupAction section Co-Authored-By: Claude Opus 4.6 <[email protected]>
4 participants
Defines Schreier graphs as quivers with labeled edges.
SchreierGraph V ι: type alias for vertices with quiver structureschreierGraphLabelling: prefunctor extracting edge labelsschreierGraphLabelling_isCovering: the labelling is a covering for group actionsschreierGraph_action_commute: label-preserving maps commute with the actionPorted from Lean 3 PR #18693.
This PR was written with AI assistance (Claude). The code has been reviewed by the author and their advisor.
This is the first in a series of PRs splitting #35467 into smaller pieces, as suggested by reviewers. Upcoming PRs will add word evaluation, paths, connectivity, automorphisms, examples, and Cayley sum graphs.