Monoids as discrete monoidal categories

The discrete category on a monoid is a monoidal category. Multiplicative morphisms induced monoidal functors.

instance CategoryTheory.Discrete.monoidal (M : Type u) [Monoid M] : CategoryTheory.MonoidalCategory (CategoryTheory.Discrete M)

Equations

• CategoryTheory.Discrete.monoidal M = CategoryTheory.MonoidalCategory.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

instance CategoryTheory.Discrete.addMonoidal (M : Type u) [AddMonoid M] : CategoryTheory.MonoidalCategory (CategoryTheory.Discrete M)

Equations

• CategoryTheory.Discrete.addMonoidal M = CategoryTheory.MonoidalCategory.mk ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

@[simp]

theorem CategoryTheory.Discrete.addMonoidal_tensorObj_as (M : Type u) [AddMonoid M] (X Y : CategoryTheory.Discrete M) : (CategoryTheory.MonoidalCategory.tensorObj X Y).as = X.as + Y.as

@[simp]

theorem CategoryTheory.Discrete.monoidal_leftUnitor (M : Type u) [Monoid M] (X : CategoryTheory.Discrete M) : CategoryTheory.MonoidalCategory.leftUnitor X = CategoryTheory.Discrete.eqToIso ⋯

@[simp]

theorem CategoryTheory.Discrete.addMonoidal_associator (M : Type u) [AddMonoid M] (x✝ x✝¹ x✝² : CategoryTheory.Discrete M) : CategoryTheory.MonoidalCategory.associator x✝ x✝¹ x✝² = CategoryTheory.Discrete.eqToIso ⋯

@[simp]

theorem CategoryTheory.Discrete.addMonoidal_leftUnitor (M : Type u) [AddMonoid M] (X : CategoryTheory.Discrete M) : CategoryTheory.MonoidalCategory.leftUnitor X = CategoryTheory.Discrete.eqToIso ⋯

@[simp]

theorem CategoryTheory.Discrete.monoidal_tensorObj_as (M : Type u) [Monoid M] (X Y : CategoryTheory.Discrete M) : (CategoryTheory.MonoidalCategory.tensorObj X Y).as = X.as * Y.as

@[simp]

theorem CategoryTheory.Discrete.monoidal_rightUnitor (M : Type u) [Monoid M] (X : CategoryTheory.Discrete M) : CategoryTheory.MonoidalCategory.rightUnitor X = CategoryTheory.Discrete.eqToIso ⋯

@[simp]

theorem CategoryTheory.Discrete.monoidal_associator (M : Type u) [Monoid M] (x✝ x✝¹ x✝² : CategoryTheory.Discrete M) : CategoryTheory.MonoidalCategory.associator x✝ x✝¹ x✝² = CategoryTheory.Discrete.eqToIso ⋯

@[simp]

theorem CategoryTheory.Discrete.addMonoidal_rightUnitor (M : Type u) [AddMonoid M] (X : CategoryTheory.Discrete M) : CategoryTheory.MonoidalCategory.rightUnitor X = CategoryTheory.Discrete.eqToIso ⋯

@[simp]

theorem CategoryTheory.Discrete.monoidal_tensorUnit_as (M : Type u) [Monoid M] : (𝟙_ (CategoryTheory.Discrete M)).as = 1

@[simp]

theorem CategoryTheory.Discrete.addMonoidal_tensorUnit_as (M : Type u) [AddMonoid M] : (𝟙_ (CategoryTheory.Discrete M)).as = 0

def CategoryTheory.Discrete.monoidalFunctor {M : Type u} [Monoid M] {N : Type u'} [Monoid N] (F : M →* N) : CategoryTheory.Functor (CategoryTheory.Discrete M) (CategoryTheory.Discrete N)

A multiplicative morphism between monoids gives a monoidal functor between the corresponding discrete monoidal categories.

Equations

• CategoryTheory.Discrete.monoidalFunctor F = CategoryTheory.Discrete.functor fun (X : M) => { as := F X }

def CategoryTheory.Discrete.addMonoidalFunctor {M : Type u} [AddMonoid M] {N : Type u'} [AddMonoid N] (F : M →+ N) : CategoryTheory.Functor (CategoryTheory.Discrete M) (CategoryTheory.Discrete N)

An additive morphism between add_monoids gives a monoidal functor between the corresponding discrete monoidal categories.

Equations

• CategoryTheory.Discrete.addMonoidalFunctor F = CategoryTheory.Discrete.functor fun (X : M) => { as := F X }

@[simp]

theorem CategoryTheory.Discrete.monoidalFunctor_obj {M : Type u} [Monoid M] {N : Type u'} [Monoid N] (F : M →* N) (m : M) : (CategoryTheory.Discrete.monoidalFunctor F).obj { as := m } = { as := F m }

@[simp]

theorem CategoryTheory.Discrete.addMonoidalFunctor_obj {M : Type u} [AddMonoid M] {N : Type u'} [AddMonoid N] (F : M →+ N) (m : M) : (CategoryTheory.Discrete.addMonoidalFunctor F).obj { as := m } = { as := F m }

instance CategoryTheory.Discrete.monoidalFunctorMonoidal {M : Type u} [Monoid M] {N : Type u'} [Monoid N] (F : M →* N) : (CategoryTheory.Discrete.monoidalFunctor F).Monoidal

Equations

• One or more equations did not get rendered due to their size.

instance CategoryTheory.Discrete.addMonoidalFunctorMonoidal {M : Type u} [AddMonoid M] {N : Type u'} [AddMonoid N] (F : M →+ N) : (CategoryTheory.Discrete.addMonoidalFunctor F).Monoidal

Equations

• One or more equations did not get rendered due to their size.

theorem CategoryTheory.Discrete.monoidalFunctor_ε {M : Type u} [Monoid M] {N : Type u'} [Monoid N] (F : M →* N) : CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.Discrete.monoidalFunctor F) = CategoryTheory.Discrete.eqToHom ⋯

theorem CategoryTheory.Discrete.addMonoidalFunctor_ε {M : Type u} [AddMonoid M] {N : Type u'} [AddMonoid N] (F : M →+ N) : CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.Discrete.addMonoidalFunctor F) = CategoryTheory.Discrete.eqToHom ⋯

theorem CategoryTheory.Discrete.monoidalFunctor_η {M : Type u} [Monoid M] {N : Type u'} [Monoid N] (F : M →* N) : CategoryTheory.Functor.OplaxMonoidal.η (CategoryTheory.Discrete.monoidalFunctor F) = CategoryTheory.Discrete.eqToHom ⋯

theorem CategoryTheory.Discrete.addMonoidalFunctor_η {M : Type u} [AddMonoid M] {N : Type u'} [AddMonoid N] (F : M →+ N) : CategoryTheory.Functor.OplaxMonoidal.η (CategoryTheory.Discrete.addMonoidalFunctor F) = CategoryTheory.Discrete.eqToHom ⋯

theorem CategoryTheory.Discrete.monoidalFunctor_μ {M : Type u} [Monoid M] {N : Type u'} [Monoid N] (F : M →* N) (m₁ m₂ : CategoryTheory.Discrete M) : CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Discrete.monoidalFunctor F) m₁ m₂ = CategoryTheory.Discrete.eqToHom ⋯

theorem CategoryTheory.Discrete.addMonoidalFunctor_μ {M : Type u} [AddMonoid M] {N : Type u'} [AddMonoid N] (F : M →+ N) (m₁ m₂ : CategoryTheory.Discrete M) : CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Discrete.addMonoidalFunctor F) m₁ m₂ = CategoryTheory.Discrete.eqToHom ⋯

theorem CategoryTheory.Discrete.monoidalFunctor_δ {M : Type u} [Monoid M] {N : Type u'} [Monoid N] (F : M →* N) (m₁ m₂ : CategoryTheory.Discrete M) : CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.Discrete.monoidalFunctor F) m₁ m₂ = CategoryTheory.Discrete.eqToHom ⋯

theorem CategoryTheory.Discrete.addMonoidalFunctor_δ {M : Type u} [AddMonoid M] {N : Type u'} [AddMonoid N] (F : M →+ N) (m₁ m₂ : CategoryTheory.Discrete M) : CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.Discrete.addMonoidalFunctor F) m₁ m₂ = CategoryTheory.Discrete.eqToHom ⋯

def CategoryTheory.Discrete.monoidalFunctorComp {M : Type u} [Monoid M] {N : Type u'} [Monoid N] {K : Type u} [Monoid K] (F : M →* N) (G : N →* K) : (CategoryTheory.Discrete.monoidalFunctor F).comp (CategoryTheory.Discrete.monoidalFunctor G) ≅ CategoryTheory.Discrete.monoidalFunctor (G.comp F)

The monoidal natural isomorphism corresponding to composing two multiplicative morphisms.

Equations

• CategoryTheory.Discrete.monoidalFunctorComp F G = CategoryTheory.Iso.refl ((CategoryTheory.Discrete.monoidalFunctor F).comp (CategoryTheory.Discrete.monoidalFunctor G))

def CategoryTheory.Discrete.addMonoidalFunctorComp {M : Type u} [AddMonoid M] {N : Type u'} [AddMonoid N] {K : Type u} [AddMonoid K] (F : M →+ N) (G : N →+ K) : (CategoryTheory.Discrete.addMonoidalFunctor F).comp (CategoryTheory.Discrete.addMonoidalFunctor G) ≅ CategoryTheory.Discrete.addMonoidalFunctor (G.comp F)

The monoidal natural isomorphism corresponding to composing two additive morphisms.

Equations

• CategoryTheory.Discrete.addMonoidalFunctorComp F G = CategoryTheory.Iso.refl ((CategoryTheory.Discrete.addMonoidalFunctor F).comp (CategoryTheory.Discrete.addMonoidalFunctor G))

instance CategoryTheory.Discrete.monoidalFunctorComp_isMonoidal {M : Type u} [Monoid M] {N : Type u'} [Monoid N] {K : Type u} [Monoid K] (F : M →* N) (G : N →* K) : CategoryTheory.NatTrans.IsMonoidal (CategoryTheory.Discrete.monoidalFunctorComp F G).hom

instance CategoryTheory.Discrete.addMonoidalFunctorComp_isMonoidal {M : Type u} [AddMonoid M] {N : Type u'} [AddMonoid N] {K : Type u} [AddMonoid K] (F : M →+ N) (G : N →+ K) : CategoryTheory.NatTrans.IsMonoidal (CategoryTheory.Discrete.addMonoidalFunctorComp F G).hom