[Merged by Bors] - feat(CategoryTheory): a sequential limit of surjections is surjective

[dagurtomas]

We prove that in a concrete category whose forgetful functor preserves sequential limits, a sequential limit of surjections is surjective. Since this will be applied to LightProfinite, we provide the necessary instance to be able to apply this lemma as well.

---

• depends on: [Merged by Bors] - refactor(LightProfinite): redefine light profinite spaces as second countable profinite spaces #13319

This will be used in a future PR to prove that a sequential limit of epimorphisms in LightCondSet is an epimorphism.

[joelriou]

Is not it possible to deduce this from the results in CategoryTheory.CofilteredSystem? (The API may have to be slightly developed though.)

[dagurtomas]

Is not it possible to deduce this from the results in CategoryTheory.CofilteredSystem? (The API may have to be slightly developed though.)

That file deals mostly with cofiltered systems of finite sets. Here I have a cofiltered system (indexed by N^op) of light profinite sets, possibly inifinite. It is surely possible, however, to deduce this from a similar statement about inverse systems in Type _, because the forgetful functor from LightProfinite to Type _ preserves the limits in question. 

[erdOne]

LGTM modulo the nitpick on naming.

[dagurtomas]

Fixed the name

[erdOne]

Thanks!
maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by erdOne.

[kim-em]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style