mathlib3
feat(category_theory/groupoid/quotient): quotients and presentations of groupoids
#17109
Open
Open
feat(category_theory/groupoid/quotient): quotients and presentations of groupoids #17109
bottine
wants to merge
167 commits into
master
from
bottine/quotient_groupoids
add free groupoid
fc8bc6c5
some mods
baed3738
formating
6ebe9a3a
make linter happy
e942dfe5
docs
899b86af
groupoid.inv = is_iso.inv; inv_equiv
34898924
remove [simp] from groupoid.inv_comp/comp_inv
fa8f261c
forgotten namespace
3866b580
notsure
c1ba089b
Merge remote-tracking branch 'origin/groupoid_inv' into bottine/free_…
a5a8c38b
cleanup
067d9760
no tactic mode in prefunctor.ext
7d978826
docstring
ab532d9c
free groupoid via quotient of path category
7acff8d3
remove noise
7ce84654
free gorupoid more stuff but stuck at spec and spec_unique
494dba36
need lift_spec and lift_unique for all of symmetrify, quotient, paths…
628e2747
lift_spec and lift_spec_unique work for the groupoid, but still need …
ff396b65
all lifts and lift_specs and lift_spec_uniques done
3d4d4cb1
more stuff in quiver symmetrization
40fab3b0
word management messy messy
2bed16a6
details
c9354dc6
nosorry
ba492cd9
lints
24aa84ee
simp unhappy
2ffdbd3d
details
511f286d
Merge remote-tracking branch 'origin/groupoid_inv' into bottine/free_…
c2f502a7
instance priority
b3dcdb99
linty
adf42a47
some simplifications
5b2fd353
cleaning up and trying to understand how to compose
3a3633a4
red_step now an inductive type (proposed by @joelriou)
b4aaa9aa
docstring
2ba79ea1
durdur
eb3f391d
stubs for ump
8f7da799
`of` is a functor yay
e233181f
simpa instead of `simp, assumption`
17661a41
not ez
461ed459
cleanup for PR
f63916a0
cleanup PR
7a0e07f3
trying to make lean happy
2ea99cac
unwanted file
54b3e665
happy lint
62d2986b
Merge branch 'master' into bottine/free_groupoid_cats
c34c6e11
forward image and cleanup of discrete by using an inductively defined…
29ebc300
towards graph_like subgroupoids and decomposition of normal subgroupoids
901095fc
correct statement
d4e7602f
stuff
93413ec8
bringing back the quotient… no way around it, is there?
99eb8b89
bringing back the quotient… no way around it, is there? (pt 2)
56e8a4dc
this way is probably relatively useless
70da7293
back on the 'two steps' approach to quotients!!
69759942
...
2c2c8552
reorg mostly
2fa6b331
Merge remote-tracking branch 'origin/master' into bottine/subgroupoid…
d668c9bb
stuff
80a61f70
needed stuff
155c38dc
getting sort of overwhelmed
b9d938c5
getting sort of overwhelmed
84a0e4ac
blah
ad250706
commas
cf7188fd
isotropy quotient
2efc2cc6
isotropy quotient done
7ce24487
more towards quotients
06544d8e
stopping for now
03aa18c9
comma slash indent
2e0b6376
Merge remote-tracking branch 'origin/master' into bottine/subgroupoid
285f095a
instance
d3335218
missed instance
67f44c01
nonempty instance plus eq_to_hom rather than eq.rec
e20f2266
lolol
dec8753c
lol₂
6e844316
coe_le and associated
a1ee597f
Update src/category_theory/groupoid/free_groupoid.lean
37bdc180
Update src/category_theory/groupoid/free_groupoid.lean
a6df9b27
Update src/category_theory/groupoid/free_groupoid.lean
04e811b1
Update src/category_theory/path_category.lean
cdc5635e
Update src/category_theory/path_category.lean
97b44d42
Update src/category_theory/path_category.lean
de72fa70
Update src/combinatorics/quiver/basic.lean
f9f99282
Merge branch 'master' into bottine/free_groupoid_cats
3af2c011
lift_unique homogen
0f6d2dfc
commas + forgot lift_unique homogen
067902df
misc
19cdc164
_root_
b6ad8b22
functoriality
11be0a2b
quotient has ump
4726473a
corrections after @alreadydone + new defs
14988805
Apply suggestions from code review
ed6c5307
some more corrections after @alreadydone
fe1d01f6
more corrections
8b00cbd8
set_like
f077b61e
100cols
5e274e93
lots
6bf6d102
nolots
1a67d6b5
lol
16b1e3e8
conversion to eq_to_hom
7e6b9927
barf
c20d1fc3
borf
adaee751
ok
c5e104f3
more ok
a400b208
finish abuse
b4ccdcfa
universal groupoid OK
eede846c
stuff
e00bdb10
empty commit
52654f44
Merge remote-tracking branch 'origin/bottine/free_groupoid_cats2' int…
e4c223c5
ump of presentation
dc98252a
some reorg
b4085558
quiver reorg it's starting to look OK
4d586288
universal
99f42244
merge
2c5abb18
corrections after @alreadydone
703bd571
merged?
e27cecb2
dunno
0665f66e
merge
545900b8
noinstance
3263f73f
quiver troubles
36a835f9
Revert "quiver troubles"
c16baaa3
back to working quivers I believe
518b2e43
introducing coverings
8f09d27d
action painful
7c4443f5
more actions less painful
434eb7b7
dunno
21b87380
cleaning up quotients
6da14035
more towards quotient
ed250d69
more more more quotient
e5bf01c3
quotients_two_steps only one hole!
c8de1238
cleaner
5e40443a
no sorry
ea393e0a
cleanup for quotients
555675c3
cleanup troubles
1e2c859c
rename quotient_two_steps -> quotient
761b8e97
quotients and presentations wip
62dc7932
misc
23734416
subgroupoid looking OK
76f93b55
dirty commit
8a62270a
one sorry left (dirty commit)
b1b0c890
ker = … finished soon
fb4cedb2
quivers back to master
010f6b55
really now
53d25a28
dunno
d93daeb2
no sorry in quotient
85b8a989
cleaning up
1b9c2706
cleaned up?
0d3034bf
doc
a40c9516
making the commit smaller
7813b5bc
punctuation
b7e50647
some airquote golfing
e8af3146
Merge branch 'master' into bottine/subgroupoid_more
e3124885
Merge branch 'master' into bottine/quotient_groupoids
ab35b577
Merge branch 'master' into bottine/subgroupoid_more
17ce05cb
master was right :(
0588836b
Apply suggestions from code review
2cc562ad
cleanup
b6b2f99e
cleanup++
627c27a5
minor
a3321e97
merge changes from subgroupoid_more_less
f9289328
minor
07d24a45
useless commit
a0328d06
Merge remote-tracking branch 'origin/master' into bottine/subgroupoid…
72e0be65
Apply suggestions from code review
1f8ef487
errors
420da16d
review
27574aeb
merging changes from the subgroupoid commits
97b5ff2c
dirty
b0579b69
merging complete
f31491a7
minor stuff
79cdccf9
Reviewers
No reviews
Assignees
No one assigned
Labels
needs-refactor
merge-conflict
t-algebra
too-late
Milestone
No milestone
Login to write a write a comment.
Login via GitHub