[Merged by Bors] - feat(category_theory/groupoid/free): free groupoid on a quiver #16666
Conversation
… and then we should be good?
…to define those for the building blocks
bottine
added
the
awaiting-review
|
Pull request successfully merged into master. Build succeeded: |
bors
bot
changed the title
There was a problem hiding this comment.
Hi @bottine, I just had some time to look at this PR more closely, and find it very nice in general, but I do have some suggestions that you may want to include in your subsequent PR, so I temporarily re-opened this PR to add them. The main issue is with the module docstring and name of some declarations, and the rest are just nitpicks.
Not sure if you were aware that @dwarn has defined is_free_groupoid for Nielsen-Schreier, but I don't see an easy connection between that (nonstandard) concept with what you're doing here.
I'll be looking into the subgroupoid PR and two-step quotient groupoid construction next!
| - `free_groupoid V`: a type synonym for `V`. | ||
| - `free_groupoid_groupoid`: the `groupoid` instance on `free_groupoid V`. | ||
| - `lift`: the lifting of a prefunctor from `V` to `V'` where `V'` is a groupoid, to a functor. | ||
| `free_groupoid V ⥤ V'`. | ||
| - `lift_spec` and `lift_unique`: the proofs that, respectively, `lift` indeed is a lifting | ||
| and is the unique one. |
There was a problem hiding this comment.
All these links aren't working now but maybe you don't intend them to link to declarations?
For example you need to write category_theory.groupoid.free.free_groupoid instead of free_groupoid for the first link to work. This name feels quite redundant though. You may want to write def _root_.category_theory.free_groupoid to get a more succinct name.
free_groupoid_groupoid is actually category_theory.groupoid.free.free_groupoid.category_theory.groupoid which is super-redundant; you may consider explicitly naming the instance like I suggested above.
lift_unique appears to be called lift_unique_spec now, and the quotient, path_category, and symmetrify versions have the inconsistent name lift_spec_unique. I think we don't need spec in the name; if you search mathlib there are lots of things named lift_unique but not lift_spec_unique/lift_unique_spec. It's best to uniformize them in your follow-up PR.
There was a problem hiding this comment.
Is it better to write those as links? By looking at a few other files in mathlib, I haven't found many such links for stuff defined in the file at hand.
Co-authored-by: Junyan Xu <junyanxumath@gmail.com>
Co-authored-by: Junyan Xu <junyanxumath@gmail.com>
Co-authored-by: Junyan Xu <junyanxumath@gmail.com>
Co-authored-by: Junyan Xu <junyanxumath@gmail.com>
Co-authored-by: Junyan Xu <junyanxumath@gmail.com>
Co-authored-by: Junyan Xu <junyanxumath@gmail.com>
Co-authored-by: Junyan Xu <junyanxumath@gmail.com>
|
Thanks a lot! I think I've corrected everything. As for Note I'd like to take the opportunity to add functoriality of the free groupoid: working on this now, pushing as soon as possible. |
|
Thanks! |
|
Already running a review |
|
I guess bors can't merge the same PR twice :) It wasn't added to the queue. We should probably close this to avoid confusing people. I think @bottine is meant to open another PR with the new changes in this PR or possibly more. |
|
@alreadydone @jcommelin : Here you go #16907 (I had to make a new useless commit for git(hub?) to accept this new branch as different). |
Define the free groupoid on a quiver and prove its universal property.