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.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

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

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 => { 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) [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_8 (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_11 (M : Type u_1) [AddMonoid M] {X : CategoryTheory.Discrete M} {Y : CategoryTheory.Discrete M} (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) [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 => { 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) [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 => { 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) [AddMonoid M] : ∀ {X₁ X₂ : CategoryTheory.Discrete M}, (X₁ ⟶ X₂) → ∀ (X : CategoryTheory.Discrete M), (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) [AddMonoid M] (X : CategoryTheory.Discrete M) : 0 + X.as = X.as

theorem CategoryTheory.Discrete.addMonoidal.proof_9 (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 => { 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) [AddMonoid M] (X : CategoryTheory.Discrete M) : X.as + 0 = X.as

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 => { 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) [AddMonoid M] (X : CategoryTheory.Discrete M) (Y : CategoryTheory.Discrete M) : 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) [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 => { 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) [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 }

@[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)

@[simp]

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

@[simp]

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

theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_11 {M : Type u_1} [AddMonoid M] {N : Type u_1} [AddMonoid N] (F : M →+ N) (X : CategoryTheory.Discrete M) (Y : CategoryTheory.Discrete M) : 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} [AddMonoid M] {N : Type u_1} [AddMonoid N] (F : M →+ N) (X : CategoryTheory.Discrete M) : 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.MonoidalCategory.tensorUnit (CategoryTheory.Discrete M))) ((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.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorUnit (CategoryTheory.Discrete M)) X))) (CategoryTheory.eqToHom (_ : (fun X => { as := ↑F X.as }) (CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorUnit (CategoryTheory.Discrete M)) X) = (fun X => { as := ↑F X.as }) X)))

theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_2 {M : Type u_1} [AddMonoid M] {N : Type u_1} [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_1} [AddMonoid N] (F : M →+ N) (X : CategoryTheory.Discrete M) : 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.MonoidalCategory.tensorUnit (CategoryTheory.Discrete M))) = (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.MonoidalCategory.tensorObj X (CategoryTheory.MonoidalCategory.tensorUnit (CategoryTheory.Discrete M))))) (CategoryTheory.eqToHom (_ : (fun X => { as := ↑F X.as }) (CategoryTheory.MonoidalCategory.tensorObj X (CategoryTheory.MonoidalCategory.tensorUnit (CategoryTheory.Discrete M))) = (fun X => { as := ↑F X.as }) X)))

theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_1 {M : Type u_1} [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_1} [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 => { 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} [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.

theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_6 {M : Type u_1} [AddMonoid M] {N : Type u_1} [AddMonoid N] (F : M →+ N) {X : CategoryTheory.Discrete M} {Y : CategoryTheory.Discrete M} {X' : CategoryTheory.Discrete M} {Y' : CategoryTheory.Discrete M} (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.MonoidalCategory.tensorObj X X'))) (CategoryTheory.eqToHom (_ : (fun X => { as := ↑F X.as }) (CategoryTheory.MonoidalCategory.tensorObj X X') = (fun X => { as := ↑F X.as }) (CategoryTheory.MonoidalCategory.tensorObj Y Y')))

theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_5 {M : Type u_1} [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_7 {M : Type u_1} [AddMonoid M] {N : Type u_1} [AddMonoid N] (F : M →+ N) (X : CategoryTheory.Discrete M) (Y : CategoryTheory.Discrete M) (Z : CategoryTheory.Discrete M) : 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.MonoidalCategory.tensorObj X Y)) ((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.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj X Y) Z))) (CategoryTheory.eqToHom (_ : (fun X => { as := ↑F X.as }) (CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) = (fun X => { as := ↑F X.as }) (CategoryTheory.MonoidalCategory.tensorObj X (CategoryTheory.MonoidalCategory.tensorObj Y Z))))) = 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 (CategoryTheory.MonoidalCategory.tensorObj Y Z).as = ↑F (X.as + (CategoryTheory.MonoidalCategory.tensorObj Y Z).as))))

theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_10 {M : Type u_1} [AddMonoid M] {N : Type u_1} [AddMonoid N] (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} [AddMonoid M] {N : Type u} [AddMonoid N] (F : M →+ N) (X : CategoryTheory.Discrete M) : ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.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.LaxMonoidalFunctor.μ (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.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.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.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.LaxMonoidalFunctor.μ (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.

theorem CategoryTheory.Discrete.addMonoidalFunctorComp.proof_6 {M : Type u_1} [AddMonoid M] {N : Type u_1} [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.obj (CategoryTheory.MonoidalCategory.tensorObj X Y))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor (AddMonoidHom.comp G F)).toLaxMonoidalFunctor.toFunctor.obj X)) (CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor (AddMonoidHom.comp G F)).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 ((CategoryTheory.Discrete.addMonoidalFunctor F).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 ((CategoryTheory.Discrete.addMonoidalFunctor F).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 ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj X) ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj Y)))) (CategoryTheory.eqToHom (_ : (fun X => { as := ↑G X.as }) (CategoryTheory.MonoidalCategory.tensorObj ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj X) ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj Y)) = (fun X => { as := ↑G X.as }) ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj (CategoryTheory.MonoidalCategory.tensorObj X Y)))))

theorem CategoryTheory.Discrete.addMonoidalFunctorComp.proof_1 {M : Type u_1} [AddMonoid M] {N : Type u_1} [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.obj X).as = ↑G ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj Y).as)) (CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor G).toLaxMonoidalFunctor.toFunctor.obj ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj Y))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor G).toLaxMonoidalFunctor.toFunctor.obj ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.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_1} [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.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor (AddMonoidHom.comp G F)).toLaxMonoidalFunctor.toFunctor.obj X))) (CategoryTheory.MonoidalNatTrans.mk (CategoryTheory.NatTrans.mk fun X => CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor F ⊗⋙ CategoryTheory.Discrete.addMonoidalFunctor G).toLaxMonoidalFunctor.toFunctor.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_1} [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.obj Y)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor (AddMonoidHom.comp G F)).toLaxMonoidalFunctor.toFunctor.obj X)) (CategoryTheory.Discrete.eqToHom (_ : ↑G ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj X).as = ↑G ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj Y).as))

theorem CategoryTheory.Discrete.addMonoidalFunctorComp.proof_2 {M : Type u_1} [AddMonoid M] {N : Type u_1} [AddMonoid N] {K : Type u_1} [AddMonoid K] (F : M →+ N) (G : N →+ K) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : CategoryTheory.MonoidalCategory.tensorUnit (CategoryTheory.Discrete K) = (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.tensorUnit (CategoryTheory.Discrete N)))) (CategoryTheory.eqToHom (_ : (fun X => { as := ↑G X.as }) (CategoryTheory.MonoidalCategory.tensorUnit (CategoryTheory.Discrete N)) = (fun X => { as := ↑G X.as }) ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj (CategoryTheory.MonoidalCategory.tensorUnit (CategoryTheory.Discrete M)))))) (CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor G).toLaxMonoidalFunctor.toFunctor.obj ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj (CategoryTheory.MonoidalCategory.tensorUnit (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.

theorem CategoryTheory.Discrete.addMonoidalFunctorComp.proof_7 {M : Type u_1} [AddMonoid M] {N : Type u_1} [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.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor F ⊗⋙ CategoryTheory.Discrete.addMonoidalFunctor G).toLaxMonoidalFunctor.toFunctor.obj X))) (CategoryTheory.MonoidalNatTrans.mk (CategoryTheory.NatTrans.mk fun X => CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor (AddMonoidHom.comp G F)).toLaxMonoidalFunctor.toFunctor.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_1} [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 => { as := ↑G X.as }, map := fun {X Y} f => CategoryTheory.Discrete.eqToHom (_ : ↑G X.as = ↑G Y.as) }).obj ((CategoryTheory.Discrete.addMonoidalFunctor F).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 ((CategoryTheory.Discrete.addMonoidalFunctor F).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 ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj X) ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj Y)))) (CategoryTheory.eqToHom (_ : (fun X => { as := ↑G X.as }) (CategoryTheory.MonoidalCategory.tensorObj ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj X) ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj Y)) = (fun X => { as := ↑G X.as }) ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj (CategoryTheory.MonoidalCategory.tensorObj X Y))))) (CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor G).toLaxMonoidalFunctor.toFunctor.obj ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj (CategoryTheory.MonoidalCategory.tensorObj X Y)))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor G).toLaxMonoidalFunctor.toFunctor.obj ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj X))) (CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor G).toLaxMonoidalFunctor.toFunctor.obj ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.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_1} [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.obj (CategoryTheory.MonoidalCategory.tensorUnit (CategoryTheory.Discrete M)))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : CategoryTheory.MonoidalCategory.tensorUnit (CategoryTheory.Discrete K) = (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.tensorUnit (CategoryTheory.Discrete N)))) (CategoryTheory.eqToHom (_ : (fun X => { as := ↑G X.as }) (CategoryTheory.MonoidalCategory.tensorUnit (CategoryTheory.Discrete N)) = (fun X => { as := ↑G X.as }) ((CategoryTheory.Discrete.addMonoidalFunctor F).toLaxMonoidalFunctor.toFunctor.obj (CategoryTheory.MonoidalCategory.tensorUnit (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.