Commit 2024-12-14 20:37 37a149f0

feat(Algebra/Category/Grp/ForgetCorepresentable, Algebra/Category/MonCat/ForgetCorepresentable): the forgetful functor on the category of monoids is corepresentable (#19964) The forgetful functor on the various categories of monoids (additive/multiplicative/commutative/etc) are representable by the natural numbers. This basically copies the corresponding code for the group categories, and moves two lemmas from Algebra.Category.Grp.ForgetCorepresentable to Algebra.Category.MonCat.ForgetCorepresentable, to avoid having a MonCat file importing a Grp file. Will be used to proved that to prove that the forgetful functor on MonCat creates all limits.