feat(CategoryTheory/Action): category of continuous actions

[chrisflav]

trafficstars

Introduces the category ContAction V G for any concrete category V with a forgetful functor to TopCat and monoid G. It is realized as a full subcategory of Action V G where the induced action is continuous.

Also introduces the full subcategory DiscreteContAction V G where the underlying topological space is discrete.

---

This is an alternative design of #12878. The difference is that instead of bundling a topological space instance in ContAction, we require V to have a HasForget₂ V TopCat instance. Examples could be:

• V = TopCat: category of topological G-sets
• V = TopCommRingCat: category of topological G-rings

[chrisflav]

Thanks for the suggestions, I adapted them in the last commit.

[joelriou]

This design seems better to me as compared to #12878

[chrisflav]

This design seems better to me as compared to #12878

I closed #12878 and adapted your suggestions.

[joelriou]

Thanks!

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style