[Merged by Bors] - feat(combinatorics/quiver/*): More edge reversal constructions by bottine · Pull Request #17665 · leanprover-community/mathlib3

bottine · 2022-11-21T09:56:04Z

Move

quiver.symmetrify,
quiver.has_reverse,
quiver.has_involutive_reverse,
quiver.reverse,
quiver.path.reverse,
quiver.symmetrify.of,
quiver.lift,
associated lemmas,

from combinatorics/quiver/connected_component.lean to combinatorics/quiver/symmetrify.lean.

Add

the class prefunctor.map_reverse witnessing that a prefunctor maps reverses to reverses, and change the lemmas taking this property as an explicit argument.
prefunctor.symmetrify mapping a prefunctor to the prefunctor between symmetrifications,
associated lemmas,

to combinatorics/quiver/symmetrify.lean.

Move quiver.hom.to_pos and quiver.hom.to_neg from category_theory/groupoid/free_groupoid.lean to combinatorics/quiver/symmetrify.lean.

Add map_reverse instance for functors between groupoids.

Co-authored-by: Antoine Labelle antoinelab01@gmail.com

depends on: [Merged by Bors] - feat(quiver/basic): push arrows of a quiver along a map #17618

…actor

src/combinatorics/quiver/basic.lean

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

ghost · 2022-12-03T17:49:16Z

This PR/issue depends on:

~~[Merged by Bors] - feat(quiver/basic): push arrows of a quiver along a map #17618~~
By Dependent Issues (🤖). Happy coding!

YaelDillies · 2022-12-04T11:34:14Z

Can you make clear whether you're adding new material or moving existing one?

bottine · 2022-12-04T12:29:59Z

@YaelDillies Well, since it's a bit of both (moving old stuff because just adding to the original file didn't make sense), can I just explain so in the commit message (which I just did), or are you arguing for further splitting?

YaelDillies · 2022-12-04T13:07:12Z

The splitting I offered before was for you to move everything at once, then add the new material file by file. As I understand, you only moved part of the material in the previous PRs, so yes please split further!

alreadydone · 2022-12-05T05:14:03Z

I had an AI generate a description of the diff and the result is in my fork; can you check if what it said make sense? I haven't look at this PR carefully so I'm not in a position to judge ... (Update: it seems that it didn't get that you're moving a large part of connected_component to symmetrify, and the notation X ⟶ Y isn't changed right? It seems to copy a lot of comments added to the code also. And zigzag doesn't exist as a declaration, so the last bullet point is nonsense (which also includes a link totally conjured up).)

I think the AI must have been trained / fine-tuned on Github PR description/comments, and the mathlib repo probably have been included in the training data.

bottine · 2022-12-05T05:46:00Z

Hahaha, I believe only the first bullet makes sense! Nice try though :)

bottine · 2022-12-05T07:03:26Z

@YaelDillies I expanded the commit message. Does that work?

src/combinatorics/quiver/symmetric.lean

bottine · 2022-12-13T09:32:42Z

I made a mathlib4 PR here In order to get this one in.

YaelDillies · 2022-12-13T14:21:50Z

Is this ready for review? If so, please add the awaiting-review tag 😉

bottine · 2022-12-13T14:23:38Z

oh, does adding labels have any effect beside easing the filtering when looking at the list of PRs?

YaelDillies · 2022-12-13T14:27:58Z

It clearly marks your intention. A PR that's not tagged awaiting-review is very unlikely to get reviewed because it doesn't show up on the queue.

src/combinatorics/quiver/symmetric.lean

src/category_theory/groupoid/free_groupoid.lean

src/combinatorics/quiver/connected_component.lean

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

src/combinatorics/quiver/symmetric.lean

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

kim-em · 2022-12-17T01:52:35Z

bors d+

Please only merge once the mathlib4 PR is in sync.

bors · 2022-12-17T01:52:36Z

✌️ bottine can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

bottine · 2022-12-17T06:21:20Z

@semorrison I've updated the mathlib4 PR (#971). I'll wait for an approval of mathlib4#971 to merge the current one.

bottine · 2022-12-17T06:44:44Z

bors r+

Move * `quiver.symmetrify`, * `quiver.has_reverse`, * `quiver.has_involutive_reverse`, * `quiver.reverse`, * `quiver.path.reverse`, * `quiver.symmetrify.of`, * `quiver.lift`, * associated lemmas, from `combinatorics/quiver/connected_component.lean` to `combinatorics/quiver/symmetrify.lean`. Add * the class `prefunctor.map_reverse` witnessing that a prefunctor maps reverses to reverses, and change the lemmas taking this property as an explicit argument. * `prefunctor.symmetrify` mapping a prefunctor to the prefunctor between symmetrifications, * associated lemmas, to `combinatorics/quiver/symmetrify.lean`. Move `quiver.hom.to_pos` and `quiver.hom.to_neg` from `category_theory/groupoid/free_groupoid.lean` to `combinatorics/quiver/symmetrify.lean`. Add `map_reverse` instance for functors between groupoids. Co-authored-by: Rémi Bottinelli <bottine@users.noreply.github.com>

bors · 2022-12-17T08:28:25Z

Pull request successfully merged into master.

Build succeeded:

… in order to sync with PR 17665 on mathlib3. See leanprover-community/mathlib3#17665 Co-authored-by: Rémi Bottinelli <bottine@users.noreply.github.com>

bottine added 6 commits November 19, 2022 07:20

include changes from bottine/quiver_refactor

c1bf235

only push

4fabd0c

only push'

a3471ec

reorg

6313840

Merge branch 'bottine/quiver_push' into bottine/quiver_symmetrify_ref…

ffe1934

…actor

symmetric stuff for quivers

e61a62a

bottine requested review from a team as code owners November 21, 2022 09:56

bottine mentioned this pull request Nov 21, 2022

refactor(combinatorics/quiver/*): Misc quivers improvements and reorganization #17537

Closed

4 tasks

lint

b69d7bc

ghost added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Nov 21, 2022

instance

9bc1f07

YaelDillies reviewed Nov 21, 2022

View reviewed changes

src/combinatorics/quiver/basic.lean Outdated Show resolved Hide resolved

src/combinatorics/quiver/basic.lean Outdated Show resolved Hide resolved

src/combinatorics/quiver/basic.lean Outdated Show resolved Hide resolved

bottine and others added 3 commits November 22, 2022 06:29

Update src/combinatorics/quiver/basic.lean

6871a56

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

comm->comp

89c258b

lift_spec_x->lift_x

002f1f4

bottine requested a review from YaelDillies November 25, 2022 06:04

ghost removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Dec 3, 2022

bottine added 2 commits December 4, 2022 07:41

Merge branch 'master' into bottine/quiver_symmetrify_refactor

16ebd84

merge master

b2f82ea

map_reverse instance for functors of groupoids

3d07afe

YaelDillies reviewed Dec 5, 2022

View reviewed changes

src/combinatorics/quiver/symmetric.lean Outdated Show resolved Hide resolved

bottine mentioned this pull request Dec 6, 2022

[Merged by Bors] - feat(combinatorics/quiver/covering): Definition of coverings and unique lifting of paths #17828

Closed

1 task

bottine added the awaiting-review The author would like community review of the PR label Dec 13, 2022

YaelDillies reviewed Dec 13, 2022

View reviewed changes

src/combinatorics/quiver/symmetric.lean Outdated Show resolved Hide resolved

src/category_theory/groupoid/free_groupoid.lean Show resolved Hide resolved

Yael suggestion (to match the mathlib4 PR)

ae6fe6e

YaelDillies reviewed Dec 13, 2022

View reviewed changes

src/combinatorics/quiver/connected_component.lean Outdated Show resolved Hide resolved

bottine and others added 3 commits December 13, 2022 14:41

Update src/combinatorics/quiver/connected_component.lean

0112f8c

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

variables

4920b2d

move to variable for consistency

622657d

YaelDillies reviewed Dec 13, 2022

View reviewed changes

bottine and others added 4 commits December 13, 2022 15:36

Update src/combinatorics/quiver/symmetric.lean

a214a68

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Update src/combinatorics/quiver/symmetric.lean

806a91f

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

better universe

52f14fb

Yael's suggestions

d1f2f8b

bottine requested review from YaelDillies and alreadydone December 14, 2022 06:33

github-actions bot added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels Dec 17, 2022

bors bot changed the title ~~feat(combinatorics/quiver/*): More edge reversal constructions~~ [Merged by Bors] - feat(combinatorics/quiver/*): More edge reversal constructions Dec 17, 2022

bors bot closed this Dec 17, 2022

bors bot deleted the bottine/quiver_symmetrify_refactor branch December 17, 2022 08:28

Conversation

bottine commented Nov 21, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

ghost commented Dec 3, 2022

Uh oh!

YaelDillies commented Dec 4, 2022

Uh oh!

bottine commented Dec 4, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

YaelDillies commented Dec 4, 2022

Uh oh!

alreadydone commented Dec 5, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

bottine commented Dec 5, 2022

Uh oh!

bottine commented Dec 5, 2022

Uh oh!

Uh oh!

bottine commented Dec 13, 2022

Uh oh!

YaelDillies commented Dec 13, 2022

Uh oh!

bottine commented Dec 13, 2022

Uh oh!

YaelDillies commented Dec 13, 2022

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

kim-em commented Dec 17, 2022

Uh oh!

bors bot commented Dec 17, 2022

Uh oh!

bottine commented Dec 17, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

bottine commented Dec 17, 2022

Uh oh!

bors bot commented Dec 17, 2022

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

bottine commented Nov 21, 2022 •

edited

Loading

bottine commented Dec 4, 2022 •

edited

Loading

alreadydone commented Dec 5, 2022 •

edited

Loading

bottine commented Dec 17, 2022 •

edited

Loading