feat(combinatorics/quiver): isomorphisms of quivers #18511

bottine · 2023-02-28T07:56:00Z

Co-authored-by: Adam Topaz [email protected]

The of_bijective part has been kindly provided by @adamtopaz, can I add a co-authored-by line?

src/combinatorics/quiver/cast.lean

src/combinatorics/quiver/iso.lean

alreadydone · 2023-02-28T15:55:37Z

The of_bijective part has been kindly provided by @adamtopaz, can I add a co-authored-by line?

Yeah I think that's common practice.

bottine · 2023-02-28T15:59:25Z

Thanks, I'm sometimes reluctant to do it in instances (like this one) where I asked for help and got a ready-to-use piece of code: the co-authored-by line could signal explicit co-authorship, when I just took the code and the other person didn't have a say in the result. I'm not sure that makes sense?

alreadydone · 2023-02-28T16:37:07Z

I think the main point of the "co-authored-by" lines is that they go into the commit message and are collected into stats like the Authors table here.

src/combinatorics/quiver/iso.lean

Co-authored-by: Yaël Dillies <[email protected]>

YaelDillies

Can you show that an equivalence of categories is an isomorphism of quivers?

bottine · 2023-03-01T08:39:43Z

No, since an equivalence is just "essentially surjective on objects" while an isomorphism of quivers is bijective on objects (afaiu).

src/combinatorics/quiver/iso.lean

bottine · 2023-03-01T08:57:11Z

Can you show that an equivalence of categories is an isomorphism of quivers?

But on that subject, I don't know to what extent I should try and build conversions between all this quiver stuff and categories.
I guess if the quiver stuff had been defined early on, some categorical notions could have been defined on top of that, but since they already exist by now, and the applications for me are mainly "graph-theoretical", there is not necessarily much point to bridge the two?

YaelDillies · 2023-03-17T16:15:29Z

The simple fact that it can be done is enough motivation I think. This might display gaps in the API.

bottine · 2023-03-18T05:16:02Z

But that would be work for another PR in any case, no?

YaelDillies · 2023-03-18T11:15:37Z

Well, no, I want to see whether there are gaps in your API now.

bottine · 2023-03-18T11:36:04Z

I don't follow; what type of gaps would you like to see? Could you give me some signatures or more concrete infos?

src/combinatorics/quiver/iso.lean

urkud · 2023-07-22T18:38:28Z

src/combinatorics/quiver/basic.lean

@@ -61,7 +61,7 @@ lemma ext {V : Type u} [quiver.{v₁} V] {W : Type u₂} [quiver.{v₂} W]
  {F G : prefunctor V W}
  (h_obj : ∀ X, F.obj X = G.obj X)
  (h_map : ∀ (X Y : V) (f : X ⟶ Y),
-           F.map f = eq.rec_on (h_obj Y).symm (eq.rec_on (h_obj X).symm (G.map f))) : F = G :=
+           F.map f = eq.rec_on (h_obj X).symm (eq.rec_on (h_obj Y).symm (G.map f))) : F = G :=


Why swap X and Y here?

Can't say for sure, it's been a long time.

Could you investigate and either revert or add a comment?

I'm kind of out of the loop on all this, but after trying it out in gitpod, it seems swapping X and Y works for the ext lemma itself, but then of_bijective and further lemmas in the iso file get failing proofs, which I couldn't debug.
A comment as to that is what I should do?

( ping @semorrison )

kim-em · 2023-07-30T22:27:48Z

bors d+

bors · 2023-07-30T22:27:49Z

✌️ 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.

init

8f2d379

bottine requested a review from a team as a code owner February 28, 2023 07:56

bottine added awaiting-review The author would like community review of the PR t-combinatorics Combinatorics labels Feb 28, 2023

YaelDillies reviewed Feb 28, 2023

View reviewed changes

Yael's review, easy parts

b9ac8bd

bottine and others added 2 commits February 28, 2023 09:21

to launch the CI again

af46d30

linter ups

3b702a7

YaelDillies reviewed Mar 1, 2023

View reviewed changes

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

Update src/combinatorics/quiver/iso.lean

b57e2e8

Co-authored-by: Yaël Dillies <[email protected]>

YaelDillies reviewed Mar 1, 2023

View reviewed changes

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

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

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

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

Yael's review

6831b3f

kim-em added the modifies-synchronized-file This PR touches a files that has already been ported to mathlib4, and may need a synchronization PR. label Mar 28, 2023

bottine mentioned this pull request Mar 29, 2023

feat(combinatorics.quiver): Schreier and Cayley graphs #18693

Draft

2 tasks

urkud reviewed Jun 21, 2023

View reviewed changes

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

eric-wieser added the not-too-late This PR was ready at the point mathlib3 was frozen: we will try to merge it and port it to mathlib4 label Jul 15, 2023

urkud reviewed Jul 22, 2023

View reviewed changes

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 Jul 30, 2023

bottine added 3 commits July 31, 2023 07:14

Distinct universes for iso

a905ef4

Distinct universes for isomorphic quivers.

3030177

ups

47d86b6

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(combinatorics/quiver): isomorphisms of quivers #18511

feat(combinatorics/quiver): isomorphisms of quivers #18511

bottine commented Feb 28, 2023 •

edited

Loading

alreadydone commented Feb 28, 2023 •

edited

Loading

bottine commented Feb 28, 2023 •

edited

Loading

alreadydone commented Feb 28, 2023

YaelDillies left a comment

bottine commented Mar 1, 2023

bottine commented Mar 1, 2023

YaelDillies commented Mar 17, 2023

bottine commented Mar 18, 2023

YaelDillies commented Mar 18, 2023

bottine commented Mar 18, 2023 •

edited

Loading

urkud Jul 22, 2023

bottine Jul 23, 2023

kim-em Jul 30, 2023

bottine Jul 31, 2023 •

edited

Loading

bottine Aug 5, 2023

kim-em commented Jul 30, 2023

bors bot commented Jul 30, 2023

feat(combinatorics/quiver): isomorphisms of quivers #18511

Are you sure you want to change the base?

feat(combinatorics/quiver): isomorphisms of quivers #18511

Conversation

bottine commented Feb 28, 2023 • edited Loading

alreadydone commented Feb 28, 2023 • edited Loading

bottine commented Feb 28, 2023 • edited Loading

alreadydone commented Feb 28, 2023

YaelDillies left a comment

Choose a reason for hiding this comment

bottine commented Mar 1, 2023

bottine commented Mar 1, 2023

YaelDillies commented Mar 17, 2023

bottine commented Mar 18, 2023

YaelDillies commented Mar 18, 2023

bottine commented Mar 18, 2023 • edited Loading

urkud Jul 22, 2023

Choose a reason for hiding this comment

bottine Jul 23, 2023

Choose a reason for hiding this comment

kim-em Jul 30, 2023

Choose a reason for hiding this comment

bottine Jul 31, 2023 • edited Loading

Choose a reason for hiding this comment

bottine Aug 5, 2023

Choose a reason for hiding this comment

kim-em commented Jul 30, 2023

bors bot commented Jul 30, 2023

bottine commented Feb 28, 2023 •

edited

Loading

alreadydone commented Feb 28, 2023 •

edited

Loading

bottine commented Feb 28, 2023 •

edited

Loading

bottine commented Mar 18, 2023 •

edited

Loading

bottine Jul 31, 2023 •

edited

Loading