Commutative monoid objects in ModuleCat R

Mathlib's ModuleCat.MonModuleEquivalenceAlgebra.MonObj.toRing makes the carrier of a monoid object in ModuleCat R a ring, whose multiplication is x * y = μ (x ⊗ₜ y). This file records that the ring is commutative when the monoid object is commutative.

@[instance_reducible]

noncomputable def ModuleCat.MonModuleEquivalenceAlgebra.MonObj.toCommRing {R : Type u} [CommRing R] (A : ModuleCat R) [CategoryTheory.MonObj A] [CategoryTheory.IsCommMonObj A] : CommRing ↑A

The commutative ring structure on a commutative monoid object in ModuleCat R: the ring structure ModuleCat.MonModuleEquivalenceAlgebra.MonObj.toRing, whose multiplication is commutative by commutativity of the monoid object.

Like MonObj.toRing, this is not an instance, since it does not round trip from a commutative ring to a monoid object and back.

Equations

• ModuleCat.MonModuleEquivalenceAlgebra.MonObj.toCommRing A = { toRing := ModuleCat.MonModuleEquivalenceAlgebra.MonObj.toRing A, mul_comm := ⋯ }