mathlib3
feat(combinatorics.quiver): Schreier and Cayley graphs
#18693
Open
Overview
Commits
80
Changes
View On GitHub

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

bottine wants to merge 80 commits into master from bottine/combinatorics.quiver/schreier
bottine
bottine include changes from bottine/quiver_refactor
c1bf235d
bottine minor
6798f016
bottine minor
688b0f66
bottine alignment
2dfae3a6
bottine only push
4fabd0c8
bottine only push'
a3471ecd
bottine reorg
63138404
antoinelab01 Update src/combinatorics/quiver/basic.lean
80f772bc
antoinelab01 .
63146c97
bottine Merge branch 'bottine/quiver_push' into bottine/quiver_symmetrify_ref…
ffe1934d
bottine symmetric stuff for quivers
e61a62a7
bottine lint
b69d7bc3
bottine instance
9bc1f07c
bottine Update src/combinatorics/quiver/basic.lean
6871a569
bottine comm->comp
89c258bf
bottine lift_spec_x->lift_x
002f1f40
bottine move `hom.cast` and `path.cast` to their own file
c579c5b1
bottine Merge branch 'master' into bottine/quiver_symmetrify_refactor
16ebd84a
bottine merge master
b2f82eaa
bottine map_reverse instance for functors of groupoids
3d07afe2
bottine merged
a671677e
bottine wip
a4f7c3fc
bottine no error
4a8e893e
bottine covering
2d0cb71f
bottine simp only
bb0f7d97
bottine minigolf
9f80f091
bottine names
5e946a5c
bottine merge
a695f6ba
bottine merge?
4dc0f137
bottine spaces after commas
861976a2
bottine merge
aaa32509
bottine Apply suggestions from code review
8d7d82e9
bottine style following suggestions
6bae3822
bottine Update src/combinatorics/quiver/covering.lean
894a25a2
bottine trying to simplify prefunctor.path_star_bijective
07ef6f4f
bottine back
0bb0bf95
bottine Merge remote-tracking branch 'origin/master' into bottine/combinatori…
d1fb0e76
bottine wip
1f635744
bottine wip
a294f565
bottine difficulties
e2c61271
bottine still
0702db0a
bottine dirty commit
cab7d0bf
bottine wip
955c494f
bottine very dirty commit
db3d53cb
bottine pffh
34524fac
bottine plenty of sorrys
b6454796
bottine even more sorrys
1c9468d0
bottine a bit of a todo
2de34c34
bottine notation because why not
6d98895a
bottine blah
0de6c110
bottine staying dirty
dd30b707
bottine two morphisms of covering agreeing on a vertex agree on any reachable…
81d6c90b
bottine more about morphisms of coverings
c8058a38
bottine solidifying somewhat
ec02a867
bottine solidifying somewhat
f336c13f
bottine managed a proof using prefunctor.ext alone !!
31047b0c
bottine more uniform notation
f5e390cd
bottine attribution
a8b98b7b
bottine sorry slayer
44a1f3da
bottine ??
880ae04b
bottine misc new things
6c24fa0c
bottine misc new things
49d5b5d7
bottine yeah
f6789f8e
bottine proud
5e509fe4
bottine still can't figure out ext
57792f4d
bottine one more
13814da1
bottine regression
df8639d2
bottine ok again
5f43f5ab
bottine prefunctor ext done!!!
792f983b
bottine cleaner
90d5fa51
bottine cleaner still, hopefully
c514712b
bottine plus
ac18bcfe
bottine yes
4b0ac366
bottine docs
068d74ec
bottine init
8f2d3797
bottine Yael's review, easy parts
b9ac8bd0
bottine to launch the CI again
af46d30e
bottine merge
e8f56d6d
bottine lint ups
a1437f98
bottine rename
cd30ffb7
bottine bottine added WIP
bottine bottine added t-algebra
bottine bottine added t-combinatorics
bottine bottine requested a review 2 years ago
bottine bottine marked this pull request as draft 2 years ago
mathlib-dependent-issues-bot mathlib-dependent-issues-bot added blocked-by-other-PR
mathlib-dependent-issues-bot
bottine bottine changed the title Bottine/combinatorics.quiver/schreier feat(combinatorics.quiver): Schreier and Cayley graphs 2 years ago
kim-em kim-em added not-too-late

Login to write a write a comment.

Login via GitHub

Reviewers
No reviews
Assignees
No one assigned
Labels
WIP blocked-by-other-PR t-algebra t-combinatorics not-too-late
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum