Where to put Yoneda for CommMon_?

Stream: mathlib4

[Michał Mrugała]

I have code ready to PR which shows that if an object represents a functor to CommMonCat then it is a commutative monoid object. The natural place to put this would be Mathlib.CategoryTheory.Monoidal.CommMon_. But my proof requires the category to be Cartesian, so it might belong in the Mathlib.CategoryTheory.ChosenFiniteProducts directory.

[Joël Riou]

It should probably go in Mathlib.CategoryTheory.Monoidal.Yoneda, and it would be nice to follow the same design as for MonCat and/or to deduce some results for CommMonCat from MonCat.

[Markus Himmel]

Joël's suggestion is better, but just for the record, we have a folder Mathlib.CategoryTheory.Monoidal.Cartesian for additional results that require cartesian structure

[Michał Mrugała]

Joël Riou said:

It should probably go in Mathlib.CategoryTheory.Monoidal.Yoneda, and it would be nice to follow the same design as for MonCat and/or to deduce some results for CommMonCat from MonCat.

That was my original idea. However, I have Yoneda results also ready for (Comm)Grp which I think should belong in a different file (maybe YonedaMon and YonedaGrp?) since if we're working with monoid objects we might not want to import group object API.