# Documentation

Mathlib.CategoryTheory.Monoidal.Discrete

# 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) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (fun X Y => { as := X.as + Y.as }) X { as := 0 } = (fun X Y => { as := X.as + Y.as }) Y { as := 0 })) (CategoryTheory.eqToHom (_ : (fun X Y => { as := X.as + Y.as }) Y { as := 0 } = Y)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (fun X Y => { as := X.as + Y.as }) X { as := 0 } = X)) f
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 : ) (Z : ) :
X.as + Y.as + Z.as = X.as + (Y.as + Z.as)
theorem CategoryTheory.Discrete.addMonoidal.proof_8 (M : Type u_1) [] (X : ) (Y : ) :
theorem CategoryTheory.Discrete.addMonoidal.proof_11 (M : Type u_1) [] {X : } {Y : } (f : X Y) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (fun X Y => { as := X.as + Y.as }) { as := 0 } X = (fun X Y => { as := X.as + Y.as }) { as := 0 } Y)) (CategoryTheory.eqToHom (_ : (fun X Y => { as := X.as + Y.as }) { as := 0 } Y = Y)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (fun X Y => { as := X.as + Y.as }) { as := 0 } X = X)) f
theorem CategoryTheory.Discrete.addMonoidal.proof_4 (M : Type u_1) [] {X₁ : } {Y₁ : } {X₂ : } {Y₂ : } (f : X₁ Y₁) (g : X₂ Y₂) :
CategoryTheory.eqToHom (_ : (fun X Y => { as := X.as + Y.as }) X₁ X₂ = (fun X Y => { as := X.as + Y.as }) Y₁ Y₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (fun X Y => { as := X.as + Y.as }) X₁ X₂ = (fun X Y => { as := X.as + Y.as }) Y₁ X₂)) (CategoryTheory.eqToHom (_ : (fun X Y => { as := X.as + Y.as }) Y₁ X₂ = (fun X Y => { as := X.as + Y.as }) Y₁ Y₂))
theorem CategoryTheory.Discrete.addMonoidal.proof_14 (M : Type u_1) [] (W : ) (X : ) (Y : ) (Z : ) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (fun X Y => { as := X.as + Y.as }) ((fun X Y => { as := X.as + Y.as }) ((fun X Y => { as := X.as + Y.as }) W X) Y) Z = (fun X Y => { as := X.as + Y.as }) ((fun X Y => { as := X.as + Y.as }) W ((fun X Y => { as := X.as + Y.as }) X Y)) Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (fun X Y => { as := X.as + Y.as }) ((fun X Y => { as := X.as + Y.as }) W ((fun X Y => { as := X.as + Y.as }) X Y)) Z = (fun X Y => { as := X.as + Y.as }) W ((fun X Y => { as := X.as + Y.as }) ((fun X Y => { as := X.as + Y.as }) X Y) Z))) (CategoryTheory.eqToHom (_ : (fun X Y => { as := X.as + Y.as }) W ((fun X Y => { as := X.as + Y.as }) ((fun X Y => { as := X.as + Y.as }) X Y) Z) = (fun X Y => { as := X.as + Y.as }) W ((fun X Y => { as := X.as + Y.as }) X ((fun X Y => { as := X.as + Y.as }) Y Z))))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (fun X Y => { as := X.as + Y.as }) ((fun X Y => { as := X.as + Y.as }) ((fun X Y => { as := X.as + Y.as }) W X) Y) Z = (fun X Y => { as := X.as + Y.as }) ((fun X Y => { as := X.as + Y.as }) W X) ((fun X Y => { as := X.as + Y.as }) Y Z))) (CategoryTheory.eqToHom (_ : (fun X Y => { as := X.as + Y.as }) ((fun X Y => { as := X.as + Y.as }) W X) ((fun X Y => { as := X.as + Y.as }) Y Z) = (fun X Y => { as := X.as + Y.as }) W ((fun X Y => { as := X.as + Y.as }) X ((fun X Y => { as := X.as + Y.as }) Y Z))))
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 : ) :
0 + X.as = X.as
theorem CategoryTheory.Discrete.addMonoidal.proof_9 (M : Type u_1) [] {X₁ : } {X₂ : } {X₃ : } {Y₁ : } {Y₂ : } {Y₃ : } (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) (f₃ : X₃ Y₃) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (fun X Y => { as := X.as + Y.as }) ((fun X Y => { as := X.as + Y.as }) X₁ X₂) X₃ = (fun X Y => { as := X.as + Y.as }) ((fun X Y => { as := X.as + Y.as }) Y₁ Y₂) Y₃)) (CategoryTheory.eqToHom (_ : (fun X Y => { as := X.as + Y.as }) ((fun X Y => { as := X.as + Y.as }) Y₁ Y₂) Y₃ = (fun X Y => { as := X.as + Y.as }) Y₁ ((fun X Y => { as := X.as + Y.as }) Y₂ Y₃))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (fun X Y => { as := X.as + Y.as }) ((fun X Y => { as := X.as + Y.as }) X₁ X₂) X₃ = (fun X Y => { as := X.as + Y.as }) X₁ ((fun X Y => { as := X.as + Y.as }) X₂ X₃))) (CategoryTheory.eqToHom (_ : (fun X Y => { as := X.as + Y.as }) X₁ ((fun X Y => { as := X.as + Y.as }) X₂ X₃) = (fun X Y => { as := X.as + Y.as }) Y₁ ((fun X Y => { as := X.as + Y.as }) Y₂ Y₃)))
theorem CategoryTheory.Discrete.addMonoidal.proof_12 (M : Type u_1) [] (X : ) :
X.as + 0 = X.as
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 : ) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (fun X Y => { as := X.as + Y.as }) ((fun X Y => { as := X.as + Y.as }) X { as := 0 }) Y = (fun X Y => { as := X.as + Y.as }) X ((fun X Y => { as := X.as + Y.as }) { as := 0 } Y))) (CategoryTheory.eqToHom (_ : (fun X Y => { as := X.as + Y.as }) X ((fun X Y => { as := X.as + Y.as }) { as := 0 } Y) = (fun X Y => { as := X.as + Y.as }) X Y)) = CategoryTheory.eqToHom (_ : (fun X Y => { as := X.as + Y.as }) ((fun X Y => { as := X.as + Y.as }) X { as := 0 }) Y = (fun X Y => { as := X.as + Y.as }) X Y)
theorem CategoryTheory.Discrete.addMonoidal.proof_6 (M : Type u_1) [] {X₁ : } {Y₁ : } {Z₁ : } {X₂ : } {Y₂ : } {Z₂ : } (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) (g₁ : Y₁ Z₁) (g₂ : Y₂ Z₂) :
CategoryTheory.eqToHom (_ : (fun X Y => { as := X.as + Y.as }) X₁ X₂ = (fun X Y => { as := X.as + Y.as }) Z₁ Z₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (fun X Y => { as := X.as + Y.as }) X₁ X₂ = (fun X Y => { as := X.as + Y.as }) Y₁ Y₂)) (CategoryTheory.eqToHom (_ : (fun X Y => { as := X.as + Y.as }) Y₁ Y₂ = (fun X Y => { as := X.as + Y.as }) Z₁ Z₂))
theorem CategoryTheory.Discrete.addMonoidal.proof_5 (M : Type u_1) [] (X₁ : ) (X₂ : ) :
CategoryTheory.CategoryStruct.id { as := X₁.as + X₂.as } = CategoryTheory.CategoryStruct.id { as := X₁.as + X₂.as }
@[simp]
@[simp]
theorem CategoryTheory.Discrete.monoidal_associator (M : Type u) [] (X : ) (Y : ) (Z : ) :
= CategoryTheory.Discrete.eqToIso (_ : X.as * Y.as * Z.as = X.as * (Y.as * Z.as))
@[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 : ) :
= CategoryTheory.Discrete.eqToIso (_ : X.as + Y.as + Z.as = X.as + (Y.as + Z.as))
theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_11 {M : Type u_1} [] {N : Type u_1} [] (F : M →+ N) (X : ) (Y : ) :
CategoryTheory.IsIso (CategoryTheory.LaxMonoidalFunctor.μ (CategoryTheory.LaxMonoidalFunctor.mk (CategoryTheory.Functor.mk { obj := fun X => { as := F X.as }, map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : F X.as = F Y.as) }) (CategoryTheory.Discrete.eqToHom (_ : 0 = F 0)) fun X Y => CategoryTheory.Discrete.eqToHom (_ : F X.as + F Y.as = F (X.as + Y.as))) X Y)
theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_8 {M : Type u_1} [] {N : Type u_1} [] (F : M →+ N) (X : ) :
CategoryTheory.eqToHom (_ : (fun X Y => { as := X.as + Y.as }) { as := 0 } { as := F X.as } = { as := F X.as }) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.Discrete.eqToHom (_ : 0 = F 0)) (CategoryTheory.CategoryStruct.id { as := F X.as })) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : CategoryTheory.MonoidalCategory.tensorObj ((CategoryTheory.Functor.mk { obj := fun X => { as := F X.as }, map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : F X.as = F Y.as) }).obj ()) ((CategoryTheory.Functor.mk { obj := fun X => { as := F X.as }, map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : F X.as = F Y.as) }).obj X) = (CategoryTheory.Functor.mk { obj := fun X => { as := F X.as }, map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : F X.as = F Y.as) }).obj ())) (CategoryTheory.eqToHom (_ : (fun X => { as := F X.as }) () = (fun X => { as := F X.as }) X)))
theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_2 {M : Type u_1} [] {N : Type u_1} [] (F : M →+ N) (X : ) :
theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_9 {M : Type u_1} [] {N : Type u_1} [] (F : M →+ N) (X : ) :
CategoryTheory.eqToHom (_ : (fun X Y => { as := X.as + Y.as }) { as := F X.as } { as := 0 } = { as := F X.as }) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id { as := F X.as }) (CategoryTheory.Discrete.eqToHom (_ : 0 = F 0))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : CategoryTheory.MonoidalCategory.tensorObj ((CategoryTheory.Functor.mk { obj := fun X => { as := F X.as }, map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : F X.as = F Y.as) }).obj X) ((CategoryTheory.Functor.mk { obj := fun X => { as := F X.as }, map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : F X.as = F Y.as) }).obj ()) = (CategoryTheory.Functor.mk { obj := fun X => { as := F X.as }, map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : F X.as = F Y.as) }).obj ())) (CategoryTheory.eqToHom (_ : (fun X => { as := F X.as }) () = (fun X => { as := F X.as }) X)))
theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_1 {M : Type u_1} [] {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_1} [] (F : M →+ N) {X : } {Y : } {Z : } (f : X Y) (g : Y Z) :
CategoryTheory.Discrete.eqToHom (_ : F X.as = F Z.as) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (fun X => { as := F X.as }) X = (fun X => { as := F X.as }) Y)) (CategoryTheory.eqToHom (_ : (fun X => { as := F X.as }) Y = (fun X => { as := F X.as }) Z))
theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_4 {M : Type u_1} [] {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.

Instances For
theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_6 {M : Type u_1} [] {N : Type u_1} [] (F : M →+ N) {X : } {Y : } {X' : } {Y' : } (f : X Y) (g : X' Y') :
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.Discrete.eqToHom (_ : F X.as = F Y.as)) (CategoryTheory.Discrete.eqToHom (_ : F X'.as = F Y'.as))) (CategoryTheory.Discrete.eqToHom (_ : F Y.as + F Y'.as = F (Y.as + Y'.as))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : CategoryTheory.MonoidalCategory.tensorObj ((CategoryTheory.Functor.mk { obj := fun X => { as := F X.as }, map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : F X.as = F Y.as) }).obj X) ((CategoryTheory.Functor.mk { obj := fun X => { as := F X.as }, map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : F X.as = F Y.as) }).obj X') = (CategoryTheory.Functor.mk { obj := fun X => { as := F X.as }, map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : F X.as = F Y.as) }).obj ())) (CategoryTheory.eqToHom (_ : (fun X => { as := F X.as }) () = (fun X => { as := F X.as }) ()))
theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_5 {M : Type u_1} [] {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_7 {M : Type u_1} [] {N : Type u_1} [] (F : M →+ N) (X : ) (Y : ) (Z : ) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.Discrete.eqToHom (_ : F X.as + F Y.as = F (X.as + Y.as))) (CategoryTheory.CategoryStruct.id { as := F Z.as })) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : CategoryTheory.MonoidalCategory.tensorObj ((CategoryTheory.Functor.mk { obj := fun X => { as := F X.as }, map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : F X.as = F Y.as) }).obj ()) ((CategoryTheory.Functor.mk { obj := fun X => { as := F X.as }, map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : F X.as = F Y.as) }).obj Z) = (CategoryTheory.Functor.mk { obj := fun X => { as := F X.as }, map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : F X.as = F Y.as) }).obj ())) (CategoryTheory.eqToHom (_ : (fun X => { as := F X.as }) () = (fun X => { as := F X.as }) ()))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (fun X Y => { as := X.as + Y.as }) ((fun X Y => { as := X.as + Y.as }) { as := F X.as } { as := F Y.as }) { as := F Z.as } = (fun X Y => { as := X.as + Y.as }) { as := F X.as } ((fun X Y => { as := X.as + Y.as }) { as := F Y.as } { as := F Z.as }))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id { as := F X.as }) (CategoryTheory.Discrete.eqToHom (_ : F Y.as + F Z.as = F (Y.as + Z.as)))) (CategoryTheory.Discrete.eqToHom (_ : F X.as + F = F (X.as + ))))
theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_10 {M : Type u_1} [] {N : Type u_1} [] (F : M →+ N) :
CategoryTheory.IsIso (CategoryTheory.LaxMonoidalFunctor.mk (CategoryTheory.Functor.mk { obj := fun X => { as := F X.as }, map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : F X.as = F Y.as) }) (CategoryTheory.Discrete.eqToHom (_ : 0 = F 0)) fun X Y => CategoryTheory.Discrete.eqToHom (_ : F X.as + F Y.as = F (X.as + Y.as))).ε
@[simp]
theorem CategoryTheory.Discrete.addMonoidalFunctor_toLaxMonoidalFunctor_toFunctor_obj_as {M : Type u} [] {N : Type u} [] (F : M →+ N) (X : ) :
(().toLaxMonoidalFunctor.toFunctor.obj X).as = F X.as
@[simp]
theorem CategoryTheory.Discrete.monoidalFunctor_toLaxMonoidalFunctor_μ {M : Type u} [] {N : Type u} [] (F : M →* N) (X : ) (Y : ) :
CategoryTheory.LaxMonoidalFunctor.μ ().toLaxMonoidalFunctor X Y = CategoryTheory.Discrete.eqToHom (_ : F X.as * F Y.as = F (X.as * Y.as))
@[simp]
theorem CategoryTheory.Discrete.addMonoidalFunctor_toLaxMonoidalFunctor_toFunctor_map {M : Type u} [] {N : Type u} [] (F : M →+ N) :
∀ {X Y : } (f : X Y), ().toLaxMonoidalFunctor.toFunctor.map f = CategoryTheory.Discrete.eqToHom (_ : F X.as = F Y.as)
@[simp]
theorem CategoryTheory.Discrete.monoidalFunctor_toLaxMonoidalFunctor_toFunctor_obj_as {M : Type u} [] {N : Type u} [] (F : M →* N) (X : ) :
(().toLaxMonoidalFunctor.toFunctor.obj X).as = F X.as
@[simp]
theorem CategoryTheory.Discrete.addMonoidalFunctor_toLaxMonoidalFunctor_ε {M : Type u} [] {N : Type u} [] (F : M →+ N) :
().toLaxMonoidalFunctor = CategoryTheory.Discrete.eqToHom (_ : 0 = F 0)
@[simp]
theorem CategoryTheory.Discrete.monoidalFunctor_toLaxMonoidalFunctor_toFunctor_map {M : Type u} [] {N : Type u} [] (F : M →* N) :
∀ {X Y : } (f : X Y), ().toLaxMonoidalFunctor.toFunctor.map f = CategoryTheory.Discrete.eqToHom (_ : F X.as = F Y.as)
@[simp]
theorem CategoryTheory.Discrete.addMonoidalFunctor_toLaxMonoidalFunctor_μ {M : Type u} [] {N : Type u} [] (F : M →+ N) (X : ) (Y : ) :
CategoryTheory.LaxMonoidalFunctor.μ ().toLaxMonoidalFunctor X Y = CategoryTheory.Discrete.eqToHom (_ : F X.as + F Y.as = F (X.as + Y.as))
@[simp]
theorem CategoryTheory.Discrete.monoidalFunctor_toLaxMonoidalFunctor_ε {M : Type u} [] {N : Type u} [] (F : M →* N) :
().toLaxMonoidalFunctor = CategoryTheory.Discrete.eqToHom (_ : 1 = F 1)
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.

Instances For
theorem CategoryTheory.Discrete.addMonoidalFunctorComp.proof_6 {M : Type u_1} [] {N : Type u_1} [] {K : Type u_1} [] (F : M →+ N) (G : N →+ K) (X : ) (Y : ) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Discrete.eqToHom (_ : ↑() X.as + ↑() Y.as = ↑() (X.as + Y.as))) (CategoryTheory.CategoryStruct.id (().toLaxMonoidalFunctor.toFunctor.obj ())) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (().toLaxMonoidalFunctor.toFunctor.obj X)) (CategoryTheory.CategoryStruct.id (().toLaxMonoidalFunctor.toFunctor.obj Y))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : CategoryTheory.MonoidalCategory.tensorObj ((CategoryTheory.Functor.mk { obj := fun X => { as := G X.as }, map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : G X.as = G Y.as) }).obj (().toLaxMonoidalFunctor.toFunctor.obj X)) ((CategoryTheory.Functor.mk { obj := fun X => { as := G X.as }, map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : G X.as = G Y.as) }).obj (().toLaxMonoidalFunctor.toFunctor.obj Y)) = (CategoryTheory.Functor.mk { obj := fun X => { as := G X.as }, map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : G X.as = G Y.as) }).obj (CategoryTheory.MonoidalCategory.tensorObj (().toLaxMonoidalFunctor.toFunctor.obj X) (().toLaxMonoidalFunctor.toFunctor.obj Y)))) (CategoryTheory.eqToHom (_ : (fun X => { as := G X.as }) (CategoryTheory.MonoidalCategory.tensorObj (().toLaxMonoidalFunctor.toFunctor.obj X) (().toLaxMonoidalFunctor.toFunctor.obj Y)) = (fun X => { as := G X.as }) (().toLaxMonoidalFunctor.toFunctor.obj ()))))
theorem CategoryTheory.Discrete.addMonoidalFunctorComp.proof_1 {M : Type u_1} [] {N : Type u_1} [] {K : Type u_1} [] (F : M →+ N) (G : N →+ K) ⦃X : ⦃Y : (f : X Y) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Discrete.eqToHom (_ : G (().toLaxMonoidalFunctor.toFunctor.obj X).as = G (().toLaxMonoidalFunctor.toFunctor.obj Y).as)) (CategoryTheory.CategoryStruct.id (().toLaxMonoidalFunctor.toFunctor.obj (().toLaxMonoidalFunctor.toFunctor.obj Y))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (().toLaxMonoidalFunctor.toFunctor.obj (().toLaxMonoidalFunctor.toFunctor.obj X))) (CategoryTheory.Discrete.eqToHom (_ : ↑() X.as = ↑() Y.as))
theorem CategoryTheory.Discrete.addMonoidalFunctorComp.proof_4 {M : Type u_1} [] {N : Type u_1} [] {K : Type u_1} [] (F : M →+ N) (G : N →+ K) ⦃X : ⦃Y : (f : X Y) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Discrete.eqToHom (_ : ↑() X.as = ↑() Y.as)) (CategoryTheory.CategoryStruct.id (().toLaxMonoidalFunctor.toFunctor.obj Y)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id (().toLaxMonoidalFunctor.toFunctor.obj X)) (CategoryTheory.Discrete.eqToHom (_ : G (().toLaxMonoidalFunctor.toFunctor.obj X).as = G (().toLaxMonoidalFunctor.toFunctor.obj Y).as))
theorem CategoryTheory.Discrete.addMonoidalFunctorComp.proof_2 {M : Type u_1} [] {N : Type u_1} [] {K : Type u_1} [] (F : M →+ N) (G : N →+ K) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : = (CategoryTheory.Functor.mk { obj := fun X => { as := G X.as }, map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : G X.as = G Y.as) }).obj ())) (CategoryTheory.eqToHom (_ : (fun X => { as := G X.as }) () = (fun X => { as := G X.as }) (().toLaxMonoidalFunctor.toFunctor.obj ())))) (CategoryTheory.CategoryStruct.id (().toLaxMonoidalFunctor.toFunctor.obj (().toLaxMonoidalFunctor.toFunctor.obj ()))) = CategoryTheory.Discrete.eqToHom (_ : 0 = ↑() 0)
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.

Instances For
theorem CategoryTheory.Discrete.addMonoidalFunctorComp.proof_3 {M : Type u_1} [] {N : Type u_1} [] {K : Type u_1} [] (F : M →+ N) (G : N →+ K) (X : ) (Y : ) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : CategoryTheory.MonoidalCategory.tensorObj ((CategoryTheory.Functor.mk { obj := fun X => { as := G X.as }, map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : G X.as = G Y.as) }).obj (().toLaxMonoidalFunctor.toFunctor.obj X)) ((CategoryTheory.Functor.mk { obj := fun X => { as := G X.as }, map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : G X.as = G Y.as) }).obj (().toLaxMonoidalFunctor.toFunctor.obj Y)) = (CategoryTheory.Functor.mk { obj := fun X => { as := G X.as }, map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : G X.as = G Y.as) }).obj (CategoryTheory.MonoidalCategory.tensorObj (().toLaxMonoidalFunctor.toFunctor.obj X) (().toLaxMonoidalFunctor.toFunctor.obj Y)))) (CategoryTheory.eqToHom (_ : (fun X => { as := G X.as }) (CategoryTheory.MonoidalCategory.tensorObj (().toLaxMonoidalFunctor.toFunctor.obj X) (().toLaxMonoidalFunctor.toFunctor.obj Y)) = (fun X => { as := G X.as }) (().toLaxMonoidalFunctor.toFunctor.obj ())))) (CategoryTheory.CategoryStruct.id (().toLaxMonoidalFunctor.toFunctor.obj (().toLaxMonoidalFunctor.toFunctor.obj ()))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (().toLaxMonoidalFunctor.toFunctor.obj (().toLaxMonoidalFunctor.toFunctor.obj X))) (CategoryTheory.CategoryStruct.id (().toLaxMonoidalFunctor.toFunctor.obj (().toLaxMonoidalFunctor.toFunctor.obj Y)))) (CategoryTheory.Discrete.eqToHom (_ : ↑() X.as + ↑() Y.as = ↑() (X.as + Y.as)))
theorem CategoryTheory.Discrete.addMonoidalFunctorComp.proof_5 {M : Type u_1} [] {N : Type u_1} [] {K : Type u_1} [] (F : M →+ N) (G : N →+ K) :
CategoryTheory.CategoryStruct.comp (CategoryTheory.Discrete.eqToHom (_ : 0 = ↑() 0)) (CategoryTheory.CategoryStruct.id (().toLaxMonoidalFunctor.toFunctor.obj ())) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : = (CategoryTheory.Functor.mk { obj := fun X => { as := G X.as }, map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : G X.as = G Y.as) }).obj ())) (CategoryTheory.eqToHom (_ : (fun X => { as := G X.as }) () = (fun X => { as := G X.as }) (().toLaxMonoidalFunctor.toFunctor.obj ())))
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.

Instances For