Closed fredrik-bakke closed 3 months ago
I should introduce path-cosplit maps and mere path-cosplit maps as separate notions. I'll leave this PR as a draft until I do.
EDIT: done.
Thanks for the swift review! Hopefully, this concept comes in useful. I don't think I've heard of a concept such as this one before, but it seems like it should be possible to do some homotopy group computations with it.
A (mere)
k
-path-cosplit map is defined inductively-2
-path-cosplit map is a map that is (merely) a retractk+1
-path-cosplit map is a map whose action on identifications is (merely)k
-path-cosplit.We show
k
-path-cosplitting is a propertyk
-truncated maps arek
-path-cosplitk
-path-cosplit maps are (merely)k+1
-path-cosplitk
-truncated types via (mere)k
-path-cosplit maps arek
-truncatedk
-path-cosplit maps intok
-truncated types arek
-truncated.