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) [AddMonoid M] {X : CategoryTheory.Discrete M} {Y : CategoryTheory.Discrete M} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id (𝟙_ (CategoryTheory.Discrete M)))) (CategoryTheory.MonoidalCategory.rightUnitor Y).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor X).hom f

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

Equations

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

theorem CategoryTheory.Discrete.addMonoidal.proof_3 (M : Type u_1) [AddMonoid M] : ∀ {X₁ Y₁ X₂ Y₂ : CategoryTheory.Discrete M}, (X₁ ⟶ Y₁) → (X₂ ⟶ Y₂) → (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) X₁ X₂ = (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) Y₁ Y₂

theorem CategoryTheory.Discrete.addMonoidal.proof_7 (M : Type u_1) [AddMonoid M] {X₁ : CategoryTheory.Discrete M} {Y₁ : CategoryTheory.Discrete M} {X₂ : CategoryTheory.Discrete M} {Y₂ : CategoryTheory.Discrete M} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂) : CategoryTheory.eqToHom (_ : (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) X₁ X₂ = (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) Y₁ Y₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) X₁ X₂ = (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) Y₁ X₂)) (CategoryTheory.eqToHom (_ : (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) Y₁ X₂ = (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) Y₁ Y₂))

theorem CategoryTheory.Discrete.addMonoidal.proof_8 (M : Type u_1) [AddMonoid M] (X₁ : CategoryTheory.Discrete M) (X₂ : CategoryTheory.Discrete M) : 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) [AddMonoid M] {X₁ : CategoryTheory.Discrete M} {X₂ : CategoryTheory.Discrete M} {X₃ : CategoryTheory.Discrete M} {Y₁ : CategoryTheory.Discrete M} {Y₂ : CategoryTheory.Discrete M} {Y₃ : CategoryTheory.Discrete M} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (f₃ : X₃ ⟶ Y₃) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) (CategoryTheory.MonoidalCategory.tensorObj X₁ X₂) X₃ = (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) (CategoryTheory.MonoidalCategory.tensorObj Y₁ Y₂) Y₃)) (CategoryTheory.eqToHom (_ : (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) ((fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) Y₁ Y₂) Y₃ = (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) Y₁ ((fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) Y₂ Y₃))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) ((fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) X₁ X₂) X₃ = (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) X₁ ((fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) X₂ X₃))) (CategoryTheory.eqToHom (_ : (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) X₁ (CategoryTheory.MonoidalCategory.tensorObj X₂ X₃) = (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) Y₁ (CategoryTheory.MonoidalCategory.tensorObj Y₂ Y₃)))

theorem CategoryTheory.Discrete.addMonoidal.proof_4 (M : Type u_1) [AddMonoid M] (X : CategoryTheory.Discrete M) (Y : CategoryTheory.Discrete M) (Z : CategoryTheory.Discrete M) : X.as + Y.as + Z.as = X.as + (Y.as + Z.as)

theorem CategoryTheory.Discrete.addMonoidal.proof_14 (M : Type u_1) [AddMonoid M] (W : CategoryTheory.Discrete M) (X : CategoryTheory.Discrete M) (Y : CategoryTheory.Discrete M) (Z : CategoryTheory.Discrete M) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) (CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj W X) Y) Z = (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) (CategoryTheory.MonoidalCategory.tensorObj W (CategoryTheory.MonoidalCategory.tensorObj X Y)) Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) ((fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) W (CategoryTheory.MonoidalCategory.tensorObj X Y)) Z = (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) W ((fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) (CategoryTheory.MonoidalCategory.tensorObj X Y) Z))) (CategoryTheory.eqToHom (_ : (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) W (CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) = (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) W (CategoryTheory.MonoidalCategory.tensorObj X (CategoryTheory.MonoidalCategory.tensorObj Y Z))))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) ((fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) (CategoryTheory.MonoidalCategory.tensorObj W X) Y) Z = (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) (CategoryTheory.MonoidalCategory.tensorObj W X) ((fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) Y Z))) (CategoryTheory.eqToHom (_ : (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) ((fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) W X) (CategoryTheory.MonoidalCategory.tensorObj Y Z) = (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) W ((fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) X (CategoryTheory.MonoidalCategory.tensorObj Y Z))))

theorem CategoryTheory.Discrete.addMonoidal.proof_2 (M : Type u_1) [AddMonoid M] : ∀ {X₁ X₂ : CategoryTheory.Discrete M}, (X₁ ⟶ X₂) → ∀ (X : CategoryTheory.Discrete M), (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) X₁ X = (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) X₂ X

theorem CategoryTheory.Discrete.addMonoidal.proof_10 (M : Type u_1) [AddMonoid M] (X : CategoryTheory.Discrete M) (Y : CategoryTheory.Discrete M) : CategoryTheory.CategoryStruct.id { as := X.as + Y.as } = CategoryTheory.CategoryStruct.id { as := X.as + Y.as }

theorem CategoryTheory.Discrete.addMonoidal.proof_9 (M : Type u_1) [AddMonoid M] {X₁ : CategoryTheory.Discrete M} {Y₁ : CategoryTheory.Discrete M} {Z₁ : CategoryTheory.Discrete M} {X₂ : CategoryTheory.Discrete M} {Y₂ : CategoryTheory.Discrete M} {Z₂ : CategoryTheory.Discrete M} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂) : CategoryTheory.eqToHom (_ : (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) X₁ X₂ = (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) Z₁ Z₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) X₁ X₂ = (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) Y₁ Y₂)) (CategoryTheory.eqToHom (_ : (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) Y₁ Y₂ = (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) Z₁ Z₂))

theorem CategoryTheory.Discrete.addMonoidal.proof_12 (M : Type u_1) [AddMonoid M] {X : CategoryTheory.Discrete M} {Y : CategoryTheory.Discrete M} (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (𝟙_ (CategoryTheory.Discrete M))) f) (CategoryTheory.MonoidalCategory.leftUnitor Y).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor X).hom f

theorem CategoryTheory.Discrete.addMonoidal.proof_1 (M : Type u_1) [AddMonoid M] (X : CategoryTheory.Discrete M) : ∀ (x x_1 : CategoryTheory.Discrete M), (x ⟶ x_1) → (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) X x = (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) X x_1

theorem CategoryTheory.Discrete.addMonoidal.proof_15 (M : Type u_1) [AddMonoid M] (X : CategoryTheory.Discrete M) (Y : CategoryTheory.Discrete M) : CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) ((fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) X (𝟙_ (CategoryTheory.Discrete M))) Y = (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) X ((fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) (𝟙_ (CategoryTheory.Discrete M)) Y))) (CategoryTheory.eqToHom (_ : (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) X (CategoryTheory.MonoidalCategory.tensorObj (𝟙_ (CategoryTheory.Discrete M)) Y) = (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) X Y)) = CategoryTheory.eqToHom (_ : (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) (CategoryTheory.MonoidalCategory.tensorObj X (𝟙_ (CategoryTheory.Discrete M))) Y = (fun (X Y : CategoryTheory.Discrete M) => { as := X.as + Y.as }) X Y)

theorem CategoryTheory.Discrete.addMonoidal.proof_6 (M : Type u_1) [AddMonoid M] (X : CategoryTheory.Discrete M) : X.as + 0 = X.as

theorem CategoryTheory.Discrete.addMonoidal.proof_5 (M : Type u_1) [AddMonoid M] (X : CategoryTheory.Discrete M) : 0 + X.as = X.as

@[simp]

theorem CategoryTheory.Discrete.addMonoidal_rightUnitor (M : Type u) [AddMonoid M] (X : CategoryTheory.Discrete M) : CategoryTheory.MonoidalCategory.rightUnitor X = CategoryTheory.Discrete.eqToIso (_ : X.as + 0 = X.as)

@[simp]

theorem CategoryTheory.Discrete.addMonoidal_leftUnitor (M : Type u) [AddMonoid M] (X : CategoryTheory.Discrete M) : CategoryTheory.MonoidalCategory.leftUnitor X = CategoryTheory.Discrete.eqToIso (_ : 0 + X.as = X.as)

@[simp]

theorem CategoryTheory.Discrete.monoidal_rightUnitor (M : Type u) [Monoid M] (X : CategoryTheory.Discrete M) : CategoryTheory.MonoidalCategory.rightUnitor X = CategoryTheory.Discrete.eqToIso (_ : X.as * 1 = X.as)

@[simp]

theorem CategoryTheory.Discrete.monoidal_associator (M : Type u) [Monoid M] (X : CategoryTheory.Discrete M) (Y : CategoryTheory.Discrete M) (Z : CategoryTheory.Discrete M) : CategoryTheory.MonoidalCategory.associator 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) [AddMonoid M] (X : CategoryTheory.Discrete M) (Y : CategoryTheory.Discrete M) : (CategoryTheory.MonoidalCategory.tensorObj X Y).as = X.as + Y.as

@[simp]

theorem CategoryTheory.Discrete.monoidal_tensorObj_as (M : Type u) [Monoid M] (X : CategoryTheory.Discrete M) (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 (_ : 1 * X.as = X.as)

@[simp]

theorem CategoryTheory.Discrete.addMonoidal_associator (M : Type u) [AddMonoid M] (X : CategoryTheory.Discrete M) (Y : CategoryTheory.Discrete M) (Z : CategoryTheory.Discrete M) : CategoryTheory.MonoidalCategory.associator X Y Z = CategoryTheory.Discrete.eqToIso (_ : X.as + Y.as + Z.as = X.as + (Y.as + Z.as))

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

Equations

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

@[simp]

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

@[simp]

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

theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_11 {M : Type u_2} [AddMonoid M] {N : Type u_1} [AddMonoid N] (F : M →+ N) : CategoryTheory.IsIso (CategoryTheory.LaxMonoidalFunctor.mk (CategoryTheory.Functor.mk { obj := fun (X : CategoryTheory.Discrete M) => { as := F X.as }, map := fun {X Y : CategoryTheory.Discrete M} (f : X ⟶ Y) => CategoryTheory.Discrete.eqToHom (_ : F X.as = F Y.as) }) (CategoryTheory.Discrete.eqToHom (_ : 0 = F 0)) fun (X Y : CategoryTheory.Discrete M) => CategoryTheory.Discrete.eqToHom (_ : F X.as + F Y.as = F (X.as + Y.as))).ε

theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_10 {M : Type u_1} [AddMonoid M] {N : Type u_2} [AddMonoid N] (F : M →+ N) (X : CategoryTheory.Discrete M) : (CategoryTheory.MonoidalCategory.rightUnitor ((CategoryTheory.Functor.mk { obj := fun (X : CategoryTheory.Discrete M) => { as := F X.as }, map := fun {X Y : CategoryTheory.Discrete M} (f : X ⟶ Y) => CategoryTheory.Discrete.eqToHom (_ : F X.as = F Y.as) }).toPrefunctor.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.mk { obj := fun (X : CategoryTheory.Discrete M) => { as := F X.as }, map := fun {X Y : CategoryTheory.Discrete M} (f : X ⟶ Y) => CategoryTheory.Discrete.eqToHom (_ : F X.as = F Y.as) }).toPrefunctor.obj X)) (CategoryTheory.Discrete.eqToHom (_ : 0 = F 0))) (CategoryTheory.CategoryStruct.comp ((fun (X Y : CategoryTheory.Discrete M) => CategoryTheory.Discrete.eqToHom (_ : F X.as + F Y.as = F (X.as + Y.as))) X (𝟙_ (CategoryTheory.Discrete M))) ((CategoryTheory.Functor.mk { obj := fun (X : CategoryTheory.Discrete M) => { as := F X.as }, map := fun {X Y : CategoryTheory.Discrete M} (f : X ⟶ Y) => CategoryTheory.Discrete.eqToHom (_ : F X.as = F Y.as) }).toPrefunctor.map (CategoryTheory.MonoidalCategory.rightUnitor X).hom))

theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_8 {M : Type u_1} [AddMonoid M] {N : Type u_2} [AddMonoid N] (F : M →+ N) (X : CategoryTheory.Discrete M) (Y : CategoryTheory.Discrete M) (Z : CategoryTheory.Discrete M) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom ((fun (X Y : CategoryTheory.Discrete M) => CategoryTheory.Discrete.eqToHom (_ : F X.as + F Y.as = F (X.as + Y.as))) X Y) (CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.mk { obj := fun (X : CategoryTheory.Discrete M) => { as := F X.as }, map := fun {X Y : CategoryTheory.Discrete M} (f : X ⟶ Y) => CategoryTheory.Discrete.eqToHom (_ : F X.as = F Y.as) }).toPrefunctor.obj Z))) (CategoryTheory.CategoryStruct.comp ((fun (X Y : CategoryTheory.Discrete M) => CategoryTheory.Discrete.eqToHom (_ : F X.as + F Y.as = F (X.as + Y.as))) (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) ((CategoryTheory.Functor.mk { obj := fun (X : CategoryTheory.Discrete M) => { as := F X.as }, map := fun {X Y : CategoryTheory.Discrete M} (f : X ⟶ Y) => CategoryTheory.Discrete.eqToHom (_ : F X.as = F Y.as) }).toPrefunctor.map (CategoryTheory.MonoidalCategory.associator X Y Z).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator ((CategoryTheory.Functor.mk { obj := fun (X : CategoryTheory.Discrete M) => { as := F X.as }, map := fun {X Y : CategoryTheory.Discrete M} (f : X ⟶ Y) => CategoryTheory.Discrete.eqToHom (_ : F X.as = F Y.as) }).toPrefunctor.obj X) ((CategoryTheory.Functor.mk { obj := fun (X : CategoryTheory.Discrete M) => { as := F X.as }, map := fun {X Y : CategoryTheory.Discrete M} (f : X ⟶ Y) => CategoryTheory.Discrete.eqToHom (_ : F X.as = F Y.as) }).toPrefunctor.obj Y) ((CategoryTheory.Functor.mk { obj := fun (X : CategoryTheory.Discrete M) => { as := F X.as }, map := fun {X Y : CategoryTheory.Discrete M} (f : X ⟶ Y) => CategoryTheory.Discrete.eqToHom (_ : F X.as = F Y.as) }).toPrefunctor.obj Z)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.mk { obj := fun (X : CategoryTheory.Discrete M) => { as := F X.as }, map := fun {X Y : CategoryTheory.Discrete M} (f : X ⟶ Y) => CategoryTheory.Discrete.eqToHom (_ : F X.as = F Y.as) }).toPrefunctor.obj X)) ((fun (X Y : CategoryTheory.Discrete M) => CategoryTheory.Discrete.eqToHom (_ : F X.as + F Y.as = F (X.as + Y.as))) Y Z)) ((fun (X Y : CategoryTheory.Discrete M) => CategoryTheory.Discrete.eqToHom (_ : F X.as + F Y.as = F (X.as + Y.as))) X (CategoryTheory.MonoidalCategory.tensorObj Y Z)))

theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_2 {M : Type u_1} [AddMonoid M] {N : Type u_2} [AddMonoid N] (F : M →+ N) (X : CategoryTheory.Discrete M) : CategoryTheory.CategoryStruct.id { as := F X.as } = CategoryTheory.CategoryStruct.id { as := F X.as }

theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_9 {M : Type u_1} [AddMonoid M] {N : Type u_2} [AddMonoid N] (F : M →+ N) (X : CategoryTheory.Discrete M) : (CategoryTheory.MonoidalCategory.leftUnitor ((CategoryTheory.Functor.mk { obj := fun (X : CategoryTheory.Discrete M) => { as := F X.as }, map := fun {X Y : CategoryTheory.Discrete M} (f : X ⟶ Y) => CategoryTheory.Discrete.eqToHom (_ : F X.as = F Y.as) }).toPrefunctor.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.Discrete.eqToHom (_ : 0 = F 0)) (CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.mk { obj := fun (X : CategoryTheory.Discrete M) => { as := F X.as }, map := fun {X Y : CategoryTheory.Discrete M} (f : X ⟶ Y) => CategoryTheory.Discrete.eqToHom (_ : F X.as = F Y.as) }).toPrefunctor.obj X))) (CategoryTheory.CategoryStruct.comp ((fun (X Y : CategoryTheory.Discrete M) => CategoryTheory.Discrete.eqToHom (_ : F X.as + F Y.as = F (X.as + Y.as))) (𝟙_ (CategoryTheory.Discrete M)) X) ((CategoryTheory.Functor.mk { obj := fun (X : CategoryTheory.Discrete M) => { as := F X.as }, map := fun {X Y : CategoryTheory.Discrete M} (f : X ⟶ Y) => CategoryTheory.Discrete.eqToHom (_ : F X.as = F Y.as) }).toPrefunctor.map (CategoryTheory.MonoidalCategory.leftUnitor X).hom))

theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_1 {M : Type u_2} [AddMonoid M] {N : Type u_1} [AddMonoid N] (F : M →+ N) : ∀ {X Y : CategoryTheory.Discrete M}, (X ⟶ Y) → F X.as = F Y.as

theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_3 {M : Type u_1} [AddMonoid M] {N : Type u_2} [AddMonoid N] (F : M →+ N) {X : CategoryTheory.Discrete M} {Y : CategoryTheory.Discrete M} {Z : CategoryTheory.Discrete M} (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryTheory.Discrete.eqToHom (_ : F X.as = F Z.as) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : (fun (X : CategoryTheory.Discrete M) => { as := F X.as }) X = (fun (X : CategoryTheory.Discrete M) => { as := F X.as }) Y)) (CategoryTheory.eqToHom (_ : (fun (X : CategoryTheory.Discrete M) => { as := F X.as }) Y = (fun (X : CategoryTheory.Discrete M) => { as := F X.as }) Z))

theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_4 {M : Type u_2} [AddMonoid M] {N : Type u_1} [AddMonoid N] (F : M →+ N) : 0 = F 0

def CategoryTheory.Discrete.addMonoidalFunctor {M : Type u} [AddMonoid M] {N : Type u'} [AddMonoid N] (F : M →+ N) : CategoryTheory.MonoidalFunctor (CategoryTheory.Discrete M) (CategoryTheory.Discrete 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.

theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_6 {M : Type u_1} [AddMonoid M] {N : Type u_2} [AddMonoid N] (F : M →+ N) {X : CategoryTheory.Discrete M} {Y : CategoryTheory.Discrete M} (f : X ⟶ Y) (X' : CategoryTheory.Discrete M) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom ((CategoryTheory.Functor.mk { obj := fun (X : CategoryTheory.Discrete M) => { as := F X.as }, map := fun {X Y : CategoryTheory.Discrete M} (f : X ⟶ Y) => CategoryTheory.Discrete.eqToHom (_ : F X.as = F Y.as) }).toPrefunctor.map f) (CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.mk { obj := fun (X : CategoryTheory.Discrete M) => { as := F X.as }, map := fun {X Y : CategoryTheory.Discrete M} (f : X ⟶ Y) => CategoryTheory.Discrete.eqToHom (_ : F X.as = F Y.as) }).toPrefunctor.obj X'))) ((fun (X Y : CategoryTheory.Discrete M) => CategoryTheory.Discrete.eqToHom (_ : F X.as + F Y.as = F (X.as + Y.as))) Y X') = CategoryTheory.CategoryStruct.comp ((fun (X Y : CategoryTheory.Discrete M) => CategoryTheory.Discrete.eqToHom (_ : F X.as + F Y.as = F (X.as + Y.as))) X X') ((CategoryTheory.Functor.mk { obj := fun (X : CategoryTheory.Discrete M) => { as := F X.as }, map := fun {X Y : CategoryTheory.Discrete M} (f : X ⟶ Y) => CategoryTheory.Discrete.eqToHom (_ : F X.as = F Y.as) }).toPrefunctor.map (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id X')))

theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_5 {M : Type u_2} [AddMonoid M] {N : Type u_1} [AddMonoid N] (F : M →+ N) (X : CategoryTheory.Discrete M) (Y : CategoryTheory.Discrete M) : F X.as + F Y.as = F (X.as + Y.as)

theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_12 {M : Type u_1} [AddMonoid M] {N : Type u_2} [AddMonoid N] (F : M →+ N) (X : CategoryTheory.Discrete M) (Y : CategoryTheory.Discrete M) : CategoryTheory.IsIso ((CategoryTheory.LaxMonoidalFunctor.mk (CategoryTheory.Functor.mk { obj := fun (X : CategoryTheory.Discrete M) => { as := F X.as }, map := fun {X Y : CategoryTheory.Discrete M} (f : X ⟶ Y) => CategoryTheory.Discrete.eqToHom (_ : F X.as = F Y.as) }) (CategoryTheory.Discrete.eqToHom (_ : 0 = F 0)) fun (X Y : CategoryTheory.Discrete M) => CategoryTheory.Discrete.eqToHom (_ : F X.as + F Y.as = F (X.as + Y.as))).μ X Y)

theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_7 {M : Type u_1} [AddMonoid M] {N : Type u_2} [AddMonoid N] (F : M →+ N) {X : CategoryTheory.Discrete M} {Y : CategoryTheory.Discrete M} (X' : CategoryTheory.Discrete M) (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.mk { obj := fun (X : CategoryTheory.Discrete M) => { as := F X.as }, map := fun {X Y : CategoryTheory.Discrete M} (f : X ⟶ Y) => CategoryTheory.Discrete.eqToHom (_ : F X.as = F Y.as) }).toPrefunctor.obj X')) ((CategoryTheory.Functor.mk { obj := fun (X : CategoryTheory.Discrete M) => { as := F X.as }, map := fun {X Y : CategoryTheory.Discrete M} (f : X ⟶ Y) => CategoryTheory.Discrete.eqToHom (_ : F X.as = F Y.as) }).toPrefunctor.map f)) ((fun (X Y : CategoryTheory.Discrete M) => CategoryTheory.Discrete.eqToHom (_ : F X.as + F Y.as = F (X.as + Y.as))) X' Y) = CategoryTheory.CategoryStruct.comp ((fun (X Y : CategoryTheory.Discrete M) => CategoryTheory.Discrete.eqToHom (_ : F X.as + F Y.as = F (X.as + Y.as))) X' X) ((CategoryTheory.Functor.mk { obj := fun (X : CategoryTheory.Discrete M) => { as := F X.as }, map := fun {X Y : CategoryTheory.Discrete M} (f : X ⟶ Y) => CategoryTheory.Discrete.eqToHom (_ : F X.as = F Y.as) }).toPrefunctor.map (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X') f))

@[simp]

theorem CategoryTheory.Discrete.addMonoidalFunctor_toLaxMonoidalFunctor_toFunctor_obj_as {M : Type u} [AddMonoid M] {N : Type u'} [AddMonoid N] (F : M →+ N) (X : CategoryTheory.Discrete M) : ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj X).as = F X.as

@[simp]

theorem CategoryTheory.Discrete.monoidalFunctor_toLaxMonoidalFunctor_μ {M : Type u} [Monoid M] {N : Type u'} [Monoid N] (F : M →* N) (X : CategoryTheory.Discrete M) (Y : CategoryTheory.Discrete M) : (CategoryTheory.Discrete.monoidalFunctor F).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} [AddMonoid M] {N : Type u'} [AddMonoid N] (F : M →+ N) : ∀ {X Y : CategoryTheory.Discrete M} (f : X ⟶ Y), (CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.toPrefunctor.map f = CategoryTheory.Discrete.eqToHom (_ : F X.as = F Y.as)

@[simp]

theorem CategoryTheory.Discrete.monoidalFunctor_toLaxMonoidalFunctor_toFunctor_obj_as {M : Type u} [Monoid M] {N : Type u'} [Monoid N] (F : M →* N) (X : CategoryTheory.Discrete M) : ((CategoryTheory.Discrete.monoidalFunctor F).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj X).as = F X.as

@[simp]

theorem CategoryTheory.Discrete.addMonoidalFunctor_toLaxMonoidalFunctor_ε {M : Type u} [AddMonoid M] {N : Type u'} [AddMonoid N] (F : M →+ N) : (CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.ε = CategoryTheory.Discrete.eqToHom (_ : 0 = F 0)

@[simp]

theorem CategoryTheory.Discrete.monoidalFunctor_toLaxMonoidalFunctor_toFunctor_map {M : Type u} [Monoid M] {N : Type u'} [Monoid N] (F : M →* N) : ∀ {X Y : CategoryTheory.Discrete M} (f : X ⟶ Y), (CategoryTheory.Discrete.monoidalFunctor F).toLaxMonoidalFunctor.toFunctor.toPrefunctor.map f = CategoryTheory.Discrete.eqToHom (_ : F X.as = F Y.as)

@[simp]

theorem CategoryTheory.Discrete.addMonoidalFunctor_toLaxMonoidalFunctor_μ {M : Type u} [AddMonoid M] {N : Type u'} [AddMonoid N] (F : M →+ N) (X : CategoryTheory.Discrete M) (Y : CategoryTheory.Discrete M) : (CategoryTheory.Discrete.addMonoidalFunctor F).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} [Monoid M] {N : Type u'} [Monoid N] (F : M →* N) : (CategoryTheory.Discrete.monoidalFunctor F).toLaxMonoidalFunctor.ε = CategoryTheory.Discrete.eqToHom (_ : 1 = F 1)

def CategoryTheory.Discrete.monoidalFunctor {M : Type u} [Monoid M] {N : Type u'} [Monoid N] (F : M →* N) : CategoryTheory.MonoidalFunctor (CategoryTheory.Discrete M) (CategoryTheory.Discrete 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.

theorem CategoryTheory.Discrete.addMonoidalFunctorComp.proof_6 {M : Type u_1} [AddMonoid M] {N : Type u_2} [AddMonoid N] {K : Type u_1} [AddMonoid K] (F : M →+ N) (G : N →+ K) (X : CategoryTheory.Discrete M) (Y : CategoryTheory.Discrete M) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Discrete.eqToHom (_ : (AddMonoidHom.comp G F) X.as + (AddMonoidHom.comp G F) Y.as = (AddMonoidHom.comp G F) (X.as + Y.as))) (CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor (AddMonoidHom.comp G F)).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj (CategoryTheory.MonoidalCategory.tensorObj X Y))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor (AddMonoidHom.comp G F)).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj X)) (CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor (AddMonoidHom.comp G F)).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj Y))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : CategoryTheory.MonoidalCategory.tensorObj ((CategoryTheory.Functor.mk { obj := fun (X : CategoryTheory.Discrete N) => { as := G X.as }, map := fun {X Y : CategoryTheory.Discrete N} (f : X ⟶ Y) => CategoryTheory.Discrete.eqToHom (_ : G X.as = G Y.as) }).toPrefunctor.obj ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj X)) ((CategoryTheory.Functor.mk { obj := fun (X : CategoryTheory.Discrete N) => { as := G X.as }, map := fun {X Y : CategoryTheory.Discrete N} (f : X ⟶ Y) => CategoryTheory.Discrete.eqToHom (_ : G X.as = G Y.as) }).toPrefunctor.obj ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj Y)) = (CategoryTheory.Functor.mk { obj := fun (X : CategoryTheory.Discrete N) => { as := G X.as }, map := fun {X Y : CategoryTheory.Discrete N} (f : X ⟶ Y) => CategoryTheory.Discrete.eqToHom (_ : G X.as = G Y.as) }).toPrefunctor.obj (CategoryTheory.MonoidalCategory.tensorObj ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj X) ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj Y)))) (CategoryTheory.eqToHom (_ : (fun (X : CategoryTheory.Discrete N) => { as := G X.as }) (CategoryTheory.MonoidalCategory.tensorObj ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj X) ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj Y)) = (fun (X : CategoryTheory.Discrete N) => { as := G X.as }) ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj (CategoryTheory.MonoidalCategory.tensorObj X Y)))))

theorem CategoryTheory.Discrete.addMonoidalFunctorComp.proof_1 {M : Type u_1} [AddMonoid M] {N : Type u_2} [AddMonoid N] {K : Type u_1} [AddMonoid K] (F : M →+ N) (G : N →+ K) ⦃X : CategoryTheory.Discrete M⦄ ⦃Y : CategoryTheory.Discrete M⦄ (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Discrete.eqToHom (_ : G ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj X).as = G ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj Y).as)) (CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor G).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj Y))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor G).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj X))) (CategoryTheory.Discrete.eqToHom (_ : (AddMonoidHom.comp G F) X.as = (AddMonoidHom.comp G F) Y.as))

theorem CategoryTheory.Discrete.addMonoidalFunctorComp.proof_8 {M : Type u_1} [AddMonoid M] {N : Type u_2} [AddMonoid N] {K : Type u_1} [AddMonoid K] (F : M →+ N) (G : N →+ K) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalNatTrans.mk (CategoryTheory.NatTrans.mk fun (X : CategoryTheory.Discrete M) => CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor (AddMonoidHom.comp G F)).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj X))) (CategoryTheory.MonoidalNatTrans.mk (CategoryTheory.NatTrans.mk fun (X : CategoryTheory.Discrete M) => CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor F ⊗⋙ CategoryTheory.Discrete.addMonoidalFunctor G).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj X))) = CategoryTheory.CategoryStruct.id (CategoryTheory.Discrete.addMonoidalFunctor (AddMonoidHom.comp G F))

theorem CategoryTheory.Discrete.addMonoidalFunctorComp.proof_4 {M : Type u_1} [AddMonoid M] {N : Type u_2} [AddMonoid N] {K : Type u_1} [AddMonoid K] (F : M →+ N) (G : N →+ K) ⦃X : CategoryTheory.Discrete M⦄ ⦃Y : CategoryTheory.Discrete M⦄ (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Discrete.eqToHom (_ : (AddMonoidHom.comp G F) X.as = (AddMonoidHom.comp G F) Y.as)) (CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor (AddMonoidHom.comp G F)).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj Y)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor (AddMonoidHom.comp G F)).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj X)) (CategoryTheory.Discrete.eqToHom (_ : G ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj X).as = G ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj Y).as))

theorem CategoryTheory.Discrete.addMonoidalFunctorComp.proof_2 {M : Type u_1} [AddMonoid M] {N : Type u_2} [AddMonoid N] {K : Type u_1} [AddMonoid K] (F : M →+ N) (G : N →+ K) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : 𝟙_ (CategoryTheory.Discrete K) = (CategoryTheory.Functor.mk { obj := fun (X : CategoryTheory.Discrete N) => { as := G X.as }, map := fun {X Y : CategoryTheory.Discrete N} (f : X ⟶ Y) => CategoryTheory.Discrete.eqToHom (_ : G X.as = G Y.as) }).toPrefunctor.obj (𝟙_ (CategoryTheory.Discrete N)))) (CategoryTheory.eqToHom (_ : (fun (X : CategoryTheory.Discrete N) => { as := G X.as }) (𝟙_ (CategoryTheory.Discrete N)) = (fun (X : CategoryTheory.Discrete N) => { as := G X.as }) ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj (𝟙_ (CategoryTheory.Discrete M)))))) (CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor G).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj (𝟙_ (CategoryTheory.Discrete M))))) = CategoryTheory.Discrete.eqToHom (_ : 0 = (AddMonoidHom.comp G F) 0)

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 ⊗⋙ CategoryTheory.Discrete.addMonoidalFunctor G ≅ CategoryTheory.Discrete.addMonoidalFunctor (AddMonoidHom.comp G F)

The monoidal natural isomorphism corresponding to composing two additive morphisms.

Equations

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

theorem CategoryTheory.Discrete.addMonoidalFunctorComp.proof_7 {M : Type u_1} [AddMonoid M] {N : Type u_2} [AddMonoid N] {K : Type u_1} [AddMonoid K] (F : M →+ N) (G : N →+ K) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalNatTrans.mk (CategoryTheory.NatTrans.mk fun (X : CategoryTheory.Discrete M) => CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor F ⊗⋙ CategoryTheory.Discrete.addMonoidalFunctor G).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj X))) (CategoryTheory.MonoidalNatTrans.mk (CategoryTheory.NatTrans.mk fun (X : CategoryTheory.Discrete M) => CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor (AddMonoidHom.comp G F)).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj X))) = CategoryTheory.CategoryStruct.id (CategoryTheory.Discrete.addMonoidalFunctor F ⊗⋙ CategoryTheory.Discrete.addMonoidalFunctor G)

theorem CategoryTheory.Discrete.addMonoidalFunctorComp.proof_3 {M : Type u_1} [AddMonoid M] {N : Type u_2} [AddMonoid N] {K : Type u_1} [AddMonoid K] (F : M →+ N) (G : N →+ K) (X : CategoryTheory.Discrete M) (Y : CategoryTheory.Discrete M) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : CategoryTheory.MonoidalCategory.tensorObj ((CategoryTheory.Functor.mk { obj := fun (X : CategoryTheory.Discrete N) => { as := G X.as }, map := fun {X Y : CategoryTheory.Discrete N} (f : X ⟶ Y) => CategoryTheory.Discrete.eqToHom (_ : G X.as = G Y.as) }).toPrefunctor.obj ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj X)) ((CategoryTheory.Functor.mk { obj := fun (X : CategoryTheory.Discrete N) => { as := G X.as }, map := fun {X Y : CategoryTheory.Discrete N} (f : X ⟶ Y) => CategoryTheory.Discrete.eqToHom (_ : G X.as = G Y.as) }).toPrefunctor.obj ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj Y)) = (CategoryTheory.Functor.mk { obj := fun (X : CategoryTheory.Discrete N) => { as := G X.as }, map := fun {X Y : CategoryTheory.Discrete N} (f : X ⟶ Y) => CategoryTheory.Discrete.eqToHom (_ : G X.as = G Y.as) }).toPrefunctor.obj (CategoryTheory.MonoidalCategory.tensorObj ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj X) ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj Y)))) (CategoryTheory.eqToHom (_ : (fun (X : CategoryTheory.Discrete N) => { as := G X.as }) (CategoryTheory.MonoidalCategory.tensorObj ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj X) ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj Y)) = (fun (X : CategoryTheory.Discrete N) => { as := G X.as }) ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj (CategoryTheory.MonoidalCategory.tensorObj X Y))))) (CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor G).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj (CategoryTheory.MonoidalCategory.tensorObj X Y)))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor G).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj X))) (CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor G).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj Y)))) (CategoryTheory.Discrete.eqToHom (_ : (AddMonoidHom.comp G F) X.as + (AddMonoidHom.comp G F) Y.as = (AddMonoidHom.comp G F) (X.as + Y.as)))

theorem CategoryTheory.Discrete.addMonoidalFunctorComp.proof_5 {M : Type u_1} [AddMonoid M] {N : Type u_2} [AddMonoid N] {K : Type u_1} [AddMonoid K] (F : M →+ N) (G : N →+ K) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Discrete.eqToHom (_ : 0 = (AddMonoidHom.comp G F) 0)) (CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor (AddMonoidHom.comp G F)).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj (𝟙_ (CategoryTheory.Discrete M)))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : 𝟙_ (CategoryTheory.Discrete K) = (CategoryTheory.Functor.mk { obj := fun (X : CategoryTheory.Discrete N) => { as := G X.as }, map := fun {X Y : CategoryTheory.Discrete N} (f : X ⟶ Y) => CategoryTheory.Discrete.eqToHom (_ : G X.as = G Y.as) }).toPrefunctor.obj (𝟙_ (CategoryTheory.Discrete N)))) (CategoryTheory.eqToHom (_ : (fun (X : CategoryTheory.Discrete N) => { as := G X.as }) (𝟙_ (CategoryTheory.Discrete N)) = (fun (X : CategoryTheory.Discrete N) => { as := G X.as }) ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.toPrefunctor.obj (𝟙_ (CategoryTheory.Discrete M)))))

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 ⊗⋙ CategoryTheory.Discrete.monoidalFunctor G ≅ CategoryTheory.Discrete.monoidalFunctor (MonoidHom.comp G F)

The monoidal natural isomorphism corresponding to composing two multiplicative morphisms.

Equations

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