Commutative monoid objects

This file provides general-purpose facts about commutative monoid objects.

Main declarations

• TauCeti.isCommMonObj_of_grp_iso: commutativity of a group object is preserved by isomorphism.

theorem TauCeti.isCommMonObj_of_grp_iso {C : Type u} [CategoryTheory.Category.{u_1, u} C] [CategoryTheory.CartesianMonoidalCategory C] [CategoryTheory.BraidedCategory C] {G H : CategoryTheory.Grp C} (e : G ≅ H) (hG : CategoryTheory.IsCommMonObj G.X) : CategoryTheory.IsCommMonObj H.X

Commutativity of a group object is preserved under isomorphism.