Added:
A detailed treatment is available in
added these pointers:
Discussion of (homotopy types of) covering spaces via homotopy type theory:
Kuen-Bang Hou, Covering Spaces in Homotopy Type Theory, extended abstract Type Theory, Homotopy Theory and Univalent Foundations (2013) doi:10.1007/978-3-319-21284-5_15
Kuen-Bang Hou, Robert Harper, Covering Spaces in Homotopy Type Theory, Leibniz International Proceedings in Informatics (LIPIcs) 97 (2018) doi:10.4230/LIPIcs.TYPES.2016.11, pdf
and with emphasis on the -truncation-modal homotopy type theory involved:
added pointer to:
Okay, so I have added to Hurewicz fibration a mentioning of covering spaces as examples here.
]]>Ah, that counterexample (here) is for “generalized covering spaces”.
]]>Hm, now I got myself mixed up. In the proof of the homotopy lifting lemma for covering spaces here, does it really need local (path-)connectedness?
]]>after the homotopy lifting lemma for covering spaces, I added a remark here saying that
this means that covering spaces are Serre fibrations,
there are counterexamples to them being always Hurewicz fibrations,
but the latter holds if base and total space admit CW-structure.
I have been editing the section Lifting properties.
Now the homotopy lifting property is stated in the generality that deserves this name (here) and the corollary “lift of homotopy between paths relative starting point for given lift of paths” is now an example afterwards (here).
]]>For completeness I have
split off an entry groupoid representation from representation
created an entry category of covering spaces.
I have added statement and proof of two more lemmas:
]]>the assumption on the base space needed is, semi-local simply-connectedness, that it be locally path-connected
Correct.
]]>It’s totally fine, Urs. I agree that the article was in need of tidying up, and please take your time.
It may be tautological, but this is the sort of “trivially trivial” material that category theory is good at rendering, and besides it’s hard to get the kind of quality of exposition in textbooks that I think we are ultimately after here. (Most textbooks still futz around with basepoints and stick to groups, not groupoids. It should be done right after all.)
]]>Thanks, Todd, for some patience. I might be about to change my mind and move it all back. But in either case the entry deserves some tidying-up.
I have tried to spell out the proof of the “fundamental theorem” now here.
It’s all very tautological, of course, but so I need to beware not falling into traps. For instance, I seem to think that the assumption on the base space needed is, besides semi-local simply-connectedness, that it be locally path-connected. Elsewhere I see instead local connectedness assumed. (?)
]]>I noticed. I would probably like to weigh in at some point on organizational matters, but I’m glad you’re thinking about this. One thing I might mention is that the whole “monodromy” discussion provides an explicit adjoint equivalence and obviates any need to bring up the axiom of choice (or at least this aspect should be brought out better), i.e., the fundamental theorem of covering space theory should make this adjoint equivalence explicit and hopefully not just say a certain functor is essentially surjective and fully faithful.
]]>I have splitt off an entry
from the entry covering space and moved to it Todd’s category-theoretic discussion In terms of a coend. Then I added also a description of the elementary construction.
(I am working towards a detailed expositional discussion of the fundamental theorem of covering spaces and am finding it helpful to organize the material a bit more, for readability. There is still other stuff at covering space that might usefully be moved to elsewhere.)
]]>Okay, I have improved (I hope) the phrasing of the last bit of the proof of “the lifting theorem” (in the section Properties – Lifting properties). In the course I added some further basics, such as the statement and proof that a covering projection is an open map (in the section Properties – Basic properties).
]]>I have also added statement and proof of “the lifting theorem” for covering spaces (here)
Presently the very last step in the proof is hard to read. I’ll see if I can improve this tomorrow.
]]>I have added the statement and the detailed elementary proof of the path lifting property of covering spaces: here.
]]>Anything that I wrote there can be removed. If I get the urge to think about such topics again I can go back to the history of the page.
]]>I have streamlined the statement of the “fundamental theorem” at covering space a little.
Eventually I’ll want this page to be ready for public consumption, usable as lecture notes. Presently it’s a bit of a mess. There are a handful of ancient query box comments sitting there, various from David (Roberts), some from Todd. Eventually I will be wishing to and working on removing these such as to make the entry text be finalized and polished.
]]>Sorry, Harry, I'm not sure what your response is to.
Edit: As for strict epimorphisms, I just searched and found that they are defined in Grothendieck's Seminaire Bourbaki No 190 (definition 2.2) - collected in FGA. I should add this to the page strict epimorphism for reference.
]]>Right Toby, the entry etale map from my memory is actually the entry etale space.
]]>