Monoids as discrete monoidal categories

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

@[implicit_reducible]

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

@[implicit_reducible]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

@[simp]

theorem CategoryTheory.Discrete.monoidalFunctor_obj {M : Type u} [Monoid M] {N : Type u'} [Monoid N] (F : M →* N) (m : M) : (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) : (addMonoidalFunctor F).obj { as := m } = { as := F m }

@[implicit_reducible]

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

@[implicit_reducible]

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

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

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

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

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

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

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

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

theorem CategoryTheory.Discrete.addMonoidalFunctor_δ {M : Type u} [AddMonoid M] {N : Type u'} [AddMonoid N] (F : M →+ N) (m₁ m₂ : Discrete M) : Functor.OplaxMonoidal.δ (addMonoidalFunctor F) m₁ m₂ = 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) : (monoidalFunctor F).comp (monoidalFunctor G) ≅ monoidalFunctor (G.comp F)

The monoidal natural isomorphism corresponding to composing two multiplicative morphisms.

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) : (addMonoidalFunctor F).comp (addMonoidalFunctor G) ≅ addMonoidalFunctor (G.comp F)

The monoidal natural isomorphism corresponding to composing two additive morphisms.

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) : NatTrans.IsMonoidal (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) : NatTrans.IsMonoidal (addMonoidalFunctorComp F G).hom