Defining specific categories

Stream: general

[Hastin Kapoor]

I want to define the category of smooth manifolds and smooth maps. Is there an example of how one can create a particular category?

[Joël Riou]

You may look at https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Category/ModuleCat/Basic.html#ModuleCat.moduleCategory to see how the category of modules over a ring is defined. (To do it for manifolds is probably not the easiest task...)