[Merged by Bors] - feat(simplex_category): various epi/mono lemmas

[joelriou]

---

Various results are obtained about injective/bijective/surjective maps in simplex_category. In particular, non surjective maps factors through some δ, and non injective maps factors through some σ. (The next step after this PR shall be proving has_strong_epi_mono_factorisation simplex_category.)

[rwbarton]

I added a comment about those lemmas whose purpose was not immediately obvious to me. It seems to me that you could pretty much just delete all these lemmas with minor refactorings to the remaining ones (though I didn't look that closely) and make the "narrative" of the file more transparent. If you want these lemmas for later use, then maybe it would be better to add them as part of a later PR where the context is more clear.

[rwbarton]

BTW, what's your plan for has_strong_epi_mono_factorisation simplex_category? It seems like the easiest way might be to do the work in the non-skeletal version and then transport the factorization to simplex_category.

[joelriou]

Thanks for the review. I have removed the eq_to_iso/hom versions. I may have to add some of them back in the future, we'll see...
For the strong_epi_mono_factorisation, I had considered doing it first in NonemptyFinLinOrd, but it turned out it was as convenient to do it directly in simplex_category.

[adamtopaz]

These lemmas all look reasonable enough to me. What are you planning to do with this PR?

[semorrison]

@joelriou, could you mark conversations as "resolved" where possible? It's easier for new reviewers to come in if we don't have to decipher which requested changes have and haven't been made.

[jcommelin]

Thanks 🎉

bors merge

[bors]

Build failed (retrying...):

• Build mathlib

[bors]

Canceled.

[eric-wieser]

bors d+

Once you've merged master and it's building again, feel free to put it back on the queue.

[bors]

✌️ joelriou can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[joelriou]

bors merge

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests