You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
I have a question which may sound very basic:
In a monoidal category, imagine you have a pointed object and a monoid object , and a pointed iso . (the 'point' of is its unit). Then it seems you can transfer the monoid structure from to , as in, if from my iso and the product in I construct the map , this is associative and unital with respect the 'point' of . I think I can just draw the commutative diagrams which prove this, but if I overlooked something, please tell me.
Now, this feels like I'm trying to say something much easier than that. Is there any piece of literature that succeeds saying in a simple way what I am saying in my convoluted way?
What you're saying sounds obvious to me and probably any category theorist. There's nothing "convoluted" about it. In a math paper you could just assert it and any decent referee would either instantly accept it or spend a few minutes checking it. Stating it and proving it as a theorem would seem heavy-handed.
Mathematicians do this transfer of structure routinely. For example, "suppose is a group and is a set equipped with a bijection . Then becomes a group". They often say such things without even bothering to write down the formulas for how it works.
Sometimes it's useful to dress this up in fancier language, e.g. "the forgetful functor from groups to sets is a discrete isofibration" "or "the forgetful functor from monoid objects to pointed objects is a discrete isofibration". But there's no point unless you have some task in mind that requires a more sophisticated outlook.
Thank you @John Baez for your quick answer. Indeed I'll need this for an article at some point and I don't think it needs a formal proof. Of course my precise case has some more details than that, is a product of monads (so a unital functor), is in fact a divided power free algebra functor from a product of operad with distributive laws, and I can produce a map that looks like a distributive law that will give a monad structure which will correspond to that of , but I was stuck proving that it was indeed a distributive law, and this "transfer of monoidicity" allows me not to prove it at all, which is a great relief.