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_6 (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 : 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_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 ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.eqToHom ⋯)

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 ⋯) (CategoryTheory.eqToHom ⋯) = CategoryTheory.eqToHom ⋯

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

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_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_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 ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.eqToHom ⋯)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.eqToHom ⋯)

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 ⋯) (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.eqToHom ⋯)

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.whiskerLeft (𝟙_ (CategoryTheory.Discrete M)) f) (CategoryTheory.MonoidalCategory.leftUnitor Y).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor X).hom f

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

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_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 ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.eqToHom ⋯)

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_4 (M : Type u_1) [AddMonoid M] : ∀ (x x_1 x_2 : CategoryTheory.Discrete M), x.as + x_1.as + x_2.as = x.as + (x_1.as + x_2.as)

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Discrete.monoidal_associator (M : Type u) [Monoid M] : ∀ (x x_1 x_2 : CategoryTheory.Discrete M), CategoryTheory.MonoidalCategory.associator x x_1 x_2 = CategoryTheory.Discrete.eqToIso ⋯

@[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_rightUnitor (M : Type u) [Monoid M] (X : CategoryTheory.Discrete M) : CategoryTheory.MonoidalCategory.rightUnitor X = CategoryTheory.Discrete.eqToIso ⋯

@[simp]

theorem CategoryTheory.Discrete.addMonoidal_associator (M : Type u) [AddMonoid M] : ∀ (x x_1 x_2 : CategoryTheory.Discrete M), CategoryTheory.MonoidalCategory.associator x x_1 x_2 = CategoryTheory.Discrete.eqToIso ⋯

@[simp]

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

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

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_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_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_10 {M : Type u_1} [AddMonoid M] {N : Type u_2} [AddMonoid N] (F : M →+ N) (X : CategoryTheory.Discrete M) : CategoryTheory.eqToHom ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft { as := F X.as } (CategoryTheory.eqToHom ⋯)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.eqToHom ⋯))

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

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.whiskerLeft { as := F X'.as } (CategoryTheory.eqToHom ⋯)) (CategoryTheory.Discrete.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.eqToHom ⋯)

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_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 ({ obj := fun (X : CategoryTheory.Discrete M) => { as := F X.as }, map := fun {X Y : CategoryTheory.Discrete M} (f : X ⟶ Y) => CategoryTheory.Discrete.eqToHom ⋯, map_id := ⋯, map_comp := ⋯, ε := CategoryTheory.Discrete.eqToHom ⋯, μ := fun (X Y : CategoryTheory.Discrete M) => CategoryTheory.Discrete.eqToHom ⋯, μ_natural_left := ⋯, μ_natural_right := ⋯, associativity := ⋯, left_unitality := ⋯, right_unitality := ⋯ }.μ X Y)

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.whiskerRight (CategoryTheory.eqToHom ⋯) { as := F X'.as }) (CategoryTheory.Discrete.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.eqToHom ⋯)

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.whiskerRight (CategoryTheory.eqToHom ⋯) { as := F Z.as }) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.eqToHom ⋯)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft { as := F X.as } (CategoryTheory.eqToHom ⋯)) (CategoryTheory.Discrete.eqToHom ⋯))

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 ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.eqToHom ⋯)

theorem CategoryTheory.Discrete.addMonoidalFunctor.proof_11 {M : Type u_2} [AddMonoid M] {N : Type u_1} [AddMonoid N] (F : M →+ N) : CategoryTheory.IsIso { obj := fun (X : CategoryTheory.Discrete M) => { as := F X.as }, map := fun {X Y : CategoryTheory.Discrete M} (f : X ⟶ Y) => CategoryTheory.Discrete.eqToHom ⋯, map_id := ⋯, map_comp := ⋯, ε := CategoryTheory.Discrete.eqToHom ⋯, μ := fun (X Y : CategoryTheory.Discrete M) => CategoryTheory.Discrete.eqToHom ⋯, μ_natural_left := ⋯, μ_natural_right := ⋯, associativity := ⋯, left_unitality := ⋯, right_unitality := ⋯ }.ε

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.eqToHom ⋯ = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.eqToHom ⋯) { as := F X.as }) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.eqToHom ⋯))

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

@[simp]

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

@[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).obj X).as = F X.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).map f = CategoryTheory.Discrete.eqToHom ⋯

@[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).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) : (CategoryTheory.Discrete.monoidalFunctor F).ε = CategoryTheory.Discrete.eqToHom ⋯

@[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).map f = CategoryTheory.Discrete.eqToHom ⋯

@[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).μ X Y = CategoryTheory.Discrete.eqToHom ⋯

@[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).μ X Y = CategoryTheory.Discrete.eqToHom ⋯

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_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 ⋯) (CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor (G.comp F)).obj (𝟙_ (CategoryTheory.Discrete M)))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.eqToHom ⋯)

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 { app := fun (x : CategoryTheory.Discrete M) => CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor F ⊗⋙ CategoryTheory.Discrete.addMonoidalFunctor G).obj x), naturality := ⋯, unit := ⋯, tensor := ⋯ } { app := fun (x : CategoryTheory.Discrete M) => CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor (G.comp F)).obj x), naturality := ⋯, unit := ⋯, tensor := ⋯ } = CategoryTheory.CategoryStruct.id (CategoryTheory.Discrete.addMonoidalFunctor F ⊗⋙ CategoryTheory.Discrete.addMonoidalFunctor G)

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.eqToHom ⋯)) (CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor G).obj ((CategoryTheory.Discrete.addMonoidalFunctor F).obj (𝟙_ (CategoryTheory.Discrete M))))) = CategoryTheory.Discrete.eqToHom ⋯

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 { app := fun (x : CategoryTheory.Discrete M) => CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor (G.comp F)).obj x), naturality := ⋯, unit := ⋯, tensor := ⋯ } { app := fun (x : CategoryTheory.Discrete M) => CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor F ⊗⋙ CategoryTheory.Discrete.addMonoidalFunctor G).obj x), naturality := ⋯, unit := ⋯, tensor := ⋯ } = CategoryTheory.CategoryStruct.id (CategoryTheory.Discrete.addMonoidalFunctor (G.comp 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 ⋯) (CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor (G.comp F)).obj Y)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor (G.comp F)).obj X)) (CategoryTheory.Discrete.eqToHom ⋯)

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.eqToHom ⋯)) (CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor G).obj ((CategoryTheory.Discrete.addMonoidalFunctor F).obj (CategoryTheory.MonoidalCategory.tensorObj X Y)))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor G).obj ((CategoryTheory.Discrete.addMonoidalFunctor F).obj X))) (CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor G).obj ((CategoryTheory.Discrete.addMonoidalFunctor F).obj Y)))) (CategoryTheory.Discrete.eqToHom ⋯)

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 ⋯) (CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor (G.comp F)).obj (CategoryTheory.MonoidalCategory.tensorObj X Y))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor (G.comp F)).obj X)) (CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor (G.comp F)).obj Y))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.eqToHom ⋯))

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 (G.comp 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_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 ⋯) (CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor G).obj ((CategoryTheory.Discrete.addMonoidalFunctor F).obj Y))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id ((CategoryTheory.Discrete.addMonoidalFunctor G).obj ((CategoryTheory.Discrete.addMonoidalFunctor F).obj X))) (CategoryTheory.Discrete.eqToHom ⋯)

def CategoryTheory.Discrete.monoidalFunctorComp {M : Type u} [Monoid M] {N : Type u'} [Monoid N] {K : Type u} [Monoid K] (F : M →* N) (G : N →* K) : CategoryTheory.Discrete.monoidalFunctor F ⊗⋙ CategoryTheory.Discrete.monoidalFunctor G ≅ CategoryTheory.Discrete.monoidalFunctor (G.comp F)

The monoidal natural isomorphism corresponding to composing two multiplicative morphisms.

Equations

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