# Monoids as discrete monoidal categories #

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

theorem CategoryTheory.Discrete.addMonoidal.proof_13 (M : Type u_1) [] {X : } {Y : } (f : X Y) :
Equations
theorem CategoryTheory.Discrete.addMonoidal.proof_3 (M : Type u_1) [] :
∀ {X₁ Y₁ X₂ Y₂ : }, (X₁ Y₁)(X₂ Y₂)(fun (X Y : ) => { as := X.as + Y.as }) X₁ X₂ = (fun (X Y : ) => { as := X.as + Y.as }) Y₁ Y₂
theorem CategoryTheory.Discrete.addMonoidal.proof_7 (M : Type u_1) [] {X₁ : } {Y₁ : } {X₂ : } {Y₂ : } (f : X₁ Y₁) (g : X₂ Y₂) :
theorem CategoryTheory.Discrete.addMonoidal.proof_8 (M : Type u_1) [] (X₁ : ) (X₂ : ) :
CategoryTheory.CategoryStruct.id { as := X₁.as + X₂.as } = CategoryTheory.CategoryStruct.id { as := X₁.as + X₂.as }
theorem CategoryTheory.Discrete.addMonoidal.proof_11 (M : Type u_1) [] {X₁ : } {X₂ : } {X₃ : } {Y₁ : } {Y₂ : } {Y₃ : } (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) (f₃ : X₃ Y₃) :
theorem CategoryTheory.Discrete.addMonoidal.proof_4 (M : Type u_1) [] (X : ) (Y : ) (Z : ) :
X.as + Y.as + Z.as = X.as + (Y.as + Z.as)
theorem CategoryTheory.Discrete.addMonoidal.proof_2 (M : Type u_1) [] :
∀ {X₁ X₂ : }, (X₁ X₂)∀ (X : ), (fun (X Y : ) => { as := X.as + Y.as }) X₁ X = (fun (X Y : ) => { as := X.as + Y.as }) X₂ X
theorem CategoryTheory.Discrete.addMonoidal.proof_10 (M : Type u_1) [] (X : ) (Y : ) :
theorem CategoryTheory.Discrete.addMonoidal.proof_9 (M : Type u_1) [] {X₁ : } {Y₁ : } {Z₁ : } {X₂ : } {Y₂ : } {Z₂ : } (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) (g₁ : Y₁ Z₁) (g₂ : Y₂ Z₂) :
theorem CategoryTheory.Discrete.addMonoidal.proof_12 (M : Type u_1) [] {X : } {Y : } (f : X Y) :
theorem CategoryTheory.Discrete.addMonoidal.proof_1 (M : Type u_1) [] (X : ) :
∀ (x x_1 : ), (x x_1)(fun (X Y : ) => { as := X.as + Y.as }) X x = (fun (X Y : ) => { as := X.as + Y.as }) X x_1
theorem CategoryTheory.Discrete.addMonoidal.proof_15 (M : Type u_1) [] (X : ) (Y : ) :
theorem CategoryTheory.Discrete.addMonoidal.proof_6 (M : Type u_1) [] (X : ) :
X.as + 0 = X.as
theorem CategoryTheory.Discrete.addMonoidal.proof_5 (M : Type u_1) [] (X : ) :
0 + X.as = X.as
@[simp]
@[simp]
@[simp]
@[simp]
theorem CategoryTheory.Discrete.monoidal_associator (M : Type u) [] (X : ) (Y : ) (Z : ) :
@[simp]
theorem CategoryTheory.Discrete.addMonoidal_tensorObj_as (M : Type u) [] (X : ) (Y : ) :
= X.as + Y.as
@[simp]
theorem CategoryTheory.Discrete.monoidal_tensorObj_as (M : Type u) [] (X : ) (Y : ) :
= X.as * Y.as
@[simp]
@[simp]
theorem CategoryTheory.Discrete.addMonoidal_associator (M : Type u) [] (X : ) (Y : ) (Z : ) :
Equations
@[simp]
theorem CategoryTheory.Discrete.addMonoidal_tensorUnit_as (M : Type u) [] :
(𝟙_ ).as = 0
@[simp]
theorem CategoryTheory.Discrete.monoidal_tensorUnit_as (M : Type u) [] :
(𝟙_ ).as = 1
theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_11 {M : Type u_2} [] {N : Type u_1} [] (F : M →+ N) :
CategoryTheory.IsIso { obj := fun (X : ) => { as := F X.as }, map := fun {X Y : } (f : X Y) => , map_id := , map_comp := , ε := , μ := fun (X Y : ) => , μ_natural_left := , μ_natural_right := , associativity := , left_unitality := , right_unitality := }
theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_10 {M : Type u_1} [] {N : Type u_2} [] (F : M →+ N) (X : ) :
theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_8 {M : Type u_1} [] {N : Type u_2} [] (F : M →+ N) (X : ) (Y : ) (Z : ) :
theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_2 {M : Type u_1} [] {N : Type u_2} [] (F : M →+ N) (X : ) :
theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_9 {M : Type u_1} [] {N : Type u_2} [] (F : M →+ N) (X : ) :
theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_1 {M : Type u_2} [] {N : Type u_1} [] (F : M →+ N) :
∀ {X Y : }, (X Y)F X.as = F Y.as
theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_3 {M : Type u_1} [] {N : Type u_2} [] (F : M →+ N) {X : } {Y : } {Z : } (f : X Y) (g : Y Z) :
theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_4 {M : Type u_2} [] {N : Type u_1} [] (F : M →+ N) :
0 = F 0
def CategoryTheory.Discrete.addMonoidalFunctor {M : Type u} [] {N : Type u'} [] (F : M →+ N) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_6 {M : Type u_1} [] {N : Type u_2} [] (F : M →+ N) {X : } {Y : } (f : X Y) (X' : ) :
theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_5 {M : Type u_2} [] {N : Type u_1} [] (F : M →+ N) (X : ) (Y : ) :
F X.as + F Y.as = F (X.as + Y.as)
theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_12 {M : Type u_1} [] {N : Type u_2} [] (F : M →+ N) (X : ) (Y : ) :
CategoryTheory.IsIso ({ obj := fun (X : ) => { as := F X.as }, map := fun {X Y : } (f : X Y) => , map_id := , map_comp := , ε := , μ := fun (X Y : ) => , μ_natural_left := , μ_natural_right := , associativity := , left_unitality := , right_unitality := } X Y)
theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_7 {M : Type u_1} [] {N : Type u_2} [] (F : M →+ N) {X : } {Y : } (X' : ) (f : X Y) :
@[simp]
theorem CategoryTheory.Discrete.addMonoidalFunctor_toLaxMonoidalFunctor_toFunctor_obj_as {M : Type u} [] {N : Type u'} [] (F : M →+ N) (X : ) :
().as = F X.as
@[simp]
theorem CategoryTheory.Discrete.monoidalFunctor_toLaxMonoidalFunctor_μ {M : Type u} [] {N : Type u'} [] (F : M →* N) (X : ) (Y : ) :
@[simp]
theorem CategoryTheory.Discrete.addMonoidalFunctor_toLaxMonoidalFunctor_toFunctor_map {M : Type u} [] {N : Type u'} [] (F : M →+ N) :
∀ {X Y : } (f : X Y),
@[simp]
theorem CategoryTheory.Discrete.monoidalFunctor_toLaxMonoidalFunctor_toFunctor_obj_as {M : Type u} [] {N : Type u'} [] (F : M →* N) (X : ) :
().as = F X.as
@[simp]
theorem CategoryTheory.Discrete.monoidalFunctor_toLaxMonoidalFunctor_toFunctor_map {M : Type u} [] {N : Type u'} [] (F : M →* N) :
∀ {X Y : } (f : X Y),
@[simp]
theorem CategoryTheory.Discrete.addMonoidalFunctor_toLaxMonoidalFunctor_μ {M : Type u} [] {N : Type u'} [] (F : M →+ N) (X : ) (Y : ) :
@[simp]
def CategoryTheory.Discrete.monoidalFunctor {M : Type u} [] {N : Type u'} [] (F : M →* N) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Discrete.addMonoidalFunctorComp.proof_1 {M : Type u_1} [] {N : Type u_2} [] {K : Type u_1} [] (F : M →+ N) (G : N →+ K) ⦃X : ⦃Y : (f : X Y) :
theorem CategoryTheory.Discrete.addMonoidalFunctorComp.proof_8 {M : Type u_1} [] {N : Type u_2} [] {K : Type u_1} [] (F : M →+ N) (G : N →+ K) :
CategoryTheory.CategoryStruct.comp { app := fun (X : ) => CategoryTheory.CategoryStruct.id (().obj X), naturality := , unit := , tensor := } { app := fun (X : ) => , naturality := , unit := , tensor := } =
theorem CategoryTheory.Discrete.addMonoidalFunctorComp.proof_4 {M : Type u_1} [] {N : Type u_2} [] {K : Type u_1} [] (F : M →+ N) (G : N →+ K) ⦃X : ⦃Y : (f : X Y) :
=
theorem CategoryTheory.Discrete.addMonoidalFunctorComp.proof_2 {M : Type u_1} [] {N : Type u_2} [] {K : Type u_1} [] (F : M →+ N) (G : N →+ K) :
=
def CategoryTheory.Discrete.addMonoidalFunctorComp {M : Type u} [] {N : Type u'} [] {K : Type u} [] (F : M →+ N) (G : N →+ K) :

The monoidal natural isomorphism corresponding to composing two additive morphisms.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.Discrete.addMonoidalFunctorComp.proof_7 {M : Type u_1} [] {N : Type u_2} [] {K : Type u_1} [] (F : M →+ N) (G : N →+ K) :
CategoryTheory.CategoryStruct.comp { app := fun (X : ) => , naturality := , unit := , tensor := } { app := fun (X : ) => CategoryTheory.CategoryStruct.id (().obj X), naturality := , unit := , tensor := } =
theorem CategoryTheory.Discrete.addMonoidalFunctorComp.proof_3 {M : Type u_1} [] {N : Type u_2} [] {K : Type u_1} [] (F : M →+ N) (G : N →+ K) (X : ) (Y : ) :
theorem CategoryTheory.Discrete.addMonoidalFunctorComp.proof_5 {M : Type u_1} [] {N : Type u_2} [] {K : Type u_1} [] (F : M →+ N) (G : N →+ K) :
def CategoryTheory.Discrete.monoidalFunctorComp {M : Type u} [] {N : Type u'} [] {K : Type u} [] (F : M →* N) (G : N →* K) :

The monoidal natural isomorphism corresponding to composing two multiplicative morphisms.

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