mathlib3
feat(algebraic_topology/fundamental_groupoid): Add topological retraction and relate to category_theory retraction
#16615
Open
Open
feat(algebraic_topology/fundamental_groupoid): Add topological retraction and relate to category_theory retraction #16615
mlavrent
wants to merge
59 commits into
master
from
fg-computations
Re-organize files to create separate folder for fg
c198c532
Add framework for helper functions converting fg to paths
58f00188
Add framework for computations to be done
9ca3a898
Finish off helpers
e2f20de3
Add definition of straight line homotopy
6c061fd3
Do stuff
07232793
Finish up some comps
f3606b61
Merge branch 'master' into fg-computations
48895987
Merge branch 'master' into fg-computations
6074079e
Merge branch 'master' into fg-computations
53b9b7aa
Add outline for adding topological retractions
aea20d57
Define the inclusion map
47da04bf
Get signatures for retraction type checking
13d643dd
Fix theorem statements
fff00dde
Implement types for split_mono of inclusion & retraction
f3c05e00
Add filler proof for composition op
64ef9267
Restructure back to flat for fg
1cdb0640
todos
c3a6d1a7
proof outline
0e366e5c
Add framework for contractible of convex instance
6b0fb485
finish proving epi_of_retraction
bc06b2da
Add doc comments
d27a061c
More formatting and clarification comment
f54b8bb1
Clean up main definitions docs
8af18ffd
Clean up sorry's
9f706092
Remove unfinished stuff for now
b3234a44
Fix
28d51480
mlavrent
changed the title
Formatting
db1e8360
Restructure to work more consistently
62569f09
Clean up split mono/split epi theorem proofs to simplify
7776bbc1
alreadydone
commented
on 2022-09-24
alreadydone
commented
on 2022-09-24
Do some stuff
6b6c69de
Add basic id, comp lemmas to help dealing with top
d4d3f734
Clean up epi/mono in groupoid proofs
79ea5bd9
Finish it up
76889591
Add doc comments and clean up
9a5ce07f
Switch from subtype to using set for the subspace of X
3b49f096
Linting fixes
9db7777a
Move instances of finite and infinite to type_tags
c48d8639
Add finite & infinite instances to additive and multiplicative
c5c3b371
Merge branch 'fin-inf-group-type-tags' into fg-surj
ca316868
Doc comment
7bc86e2d
Doc comment
81dc6e6b
Doc comment
a40c0340
Merge branch 'master' into fg-surj
8ddff7ca
Merge branch 'master' into fg-computations
234881a3
Merge branch 'master' of github.com:leanprover-community/mathlib into…
4a7d9dba
Merge branch 'master' of github.com:leanprover-community/mathlib into…
e75018d1
Add inhabited instance
6eaf67c1
Write what id is as a top_retraction
270dc963
Clean up
af1d1b0c
Merge branch 'master' into fg-computations
660a11ff
Apply suggestions from code review
c35fffa7
Apply suggestions from code review
ffc49188
Fix renaming
ec36e40d
Remove old comment
0ae9578e
Simplify proofs
90590e81
Cleanup things
7b3e0010
Merge branch 'master' into fg-computations
8a7f2e35
Merge branch 'fg-surj' into fg-computations
65918573
Reviewers
Assignees
No one assigned
Labels
awaiting-author
t-topology
too-late
Milestone
No milestone
Login to write a write a comment.
Login via GitHub