# Documentation

A monoidal category is MonoidalPreadditive if it is preadditive and tensor product of morphisms is linear in both factors.

A category is MonoidalPreadditive if tensoring is additive in both factors.

Note we don't extend Preadditive C here, as Abelian C already extends it, and we'll need to have both typeclasses sometimes.

• whiskerLeft_zero : ∀ {X Y Z : C},
• zero_whiskerRight : ∀ {X Y Z : C},
• whiskerLeft_add : ∀ {X Y Z : C} (f g : Y Z),
• add_whiskerRight : ∀ {X Y Z : C} (f g : Y Z),
Instances
@[simp]
theorem CategoryTheory.MonoidalPreadditive.whiskerLeft_zero {C : Type u_1} [] [self : ] {X : C} {Y : C} {Z : C} :
@[simp]
theorem CategoryTheory.MonoidalPreadditive.zero_whiskerRight {C : Type u_1} [] [self : ] {X : C} {Y : C} {Z : C} :
@[simp]
theorem CategoryTheory.MonoidalPreadditive.whiskerLeft_add {C : Type u_1} [] [self : ] {X : C} {Y : C} {Z : C} (f : Y Z) (g : Y Z) :
@[simp]
theorem CategoryTheory.MonoidalPreadditive.add_whiskerRight {C : Type u_1} [] [self : ] {X : C} {Y : C} {Z : C} (f : Y Z) (g : Y Z) :
@[simp]
theorem CategoryTheory.MonoidalPreadditive.tensor_zero {C : Type u_1} [] {W : C} {X : C} {Y : C} {Z : C} (f : W X) :
@[simp]
theorem CategoryTheory.MonoidalPreadditive.zero_tensor {C : Type u_1} [] {W : C} {X : C} {Y : C} {Z : C} (f : Y Z) :
theorem CategoryTheory.MonoidalPreadditive.tensor_add {C : Type u_1} [] {W : C} {X : C} {Y : C} {Z : C} (f : W X) (g : Y Z) (h : Y Z) :
theorem CategoryTheory.MonoidalPreadditive.add_tensor {C : Type u_1} [] {W : C} {X : C} {Y : C} {Z : C} (f : W X) (g : W X) (h : Y Z) :
instance CategoryTheory.tensorLeft_additive {C : Type u_1} [] (X : C) :
Equations
• =
instance CategoryTheory.tensorRight_additive {C : Type u_1} [] (X : C) :
Equations
• =
instance CategoryTheory.tensoringLeft_additive {C : Type u_1} [] (X : C) :
Equations
• =
instance CategoryTheory.tensoringRight_additive {C : Type u_1} [] (X : C) :
Equations
• =
theorem CategoryTheory.monoidalPreadditive_of_faithful {C : Type u_1} [] {D : Type u_2} [] (F : ) [F.Faithful] [F.Additive] :

A faithful additive monoidal functor to a monoidal preadditive category ensures that the domain is monoidal preadditive.

theorem CategoryTheory.whiskerLeft_sum {C : Type u_1} [] (P : C) {Q : C} {R : C} {J : Type u_2} (s : ) (g : J(Q R)) :
CategoryTheory.MonoidalCategory.whiskerLeft P (js, g j) = js,
theorem CategoryTheory.sum_whiskerRight {C : Type u_1} [] {Q : C} {R : C} {J : Type u_2} (s : ) (g : J(Q R)) (P : C) :
CategoryTheory.MonoidalCategory.whiskerRight (js, g j) P = js,
theorem CategoryTheory.tensor_sum {C : Type u_1} [] {P : C} {Q : C} {R : C} {S : C} {J : Type u_2} (s : ) (f : P Q) (g : J(R S)) :
CategoryTheory.MonoidalCategory.tensorHom f (js, g j) = js,
theorem CategoryTheory.sum_tensor {C : Type u_1} [] {P : C} {Q : C} {R : C} {S : C} {J : Type u_2} (s : ) (f : P Q) (g : J(R S)) :
CategoryTheory.MonoidalCategory.tensorHom (js, g j) f = js,
Equations
• One or more equations did not get rendered due to their size.
Equations
• One or more equations did not get rendered due to their size.
def CategoryTheory.leftDistributor {C : Type u_1} [] {J : Type} [] (X : C) (f : JC) :
fun (j : J) =>

The isomorphism showing how tensor product on the left distributes over direct sums.

Equations
• = .mapBiproduct f
Instances For
theorem CategoryTheory.leftDistributor_hom {C : Type u_1} [] {J : Type} [] (X : C) (f : JC) :
.hom = j : J,
theorem CategoryTheory.leftDistributor_inv {C : Type u_1} [] {J : Type} [] (X : C) (f : JC) :
.inv = j : J,
@[simp]
theorem CategoryTheory.leftDistributor_hom_comp_biproduct_π_assoc {C : Type u_1} [] {J : Type} [] (X : C) (f : JC) (j : J) {Z : C} (h : ) :
@[simp]
theorem CategoryTheory.leftDistributor_hom_comp_biproduct_π {C : Type u_1} [] {J : Type} [] (X : C) (f : JC) (j : J) :
@[simp]
theorem CategoryTheory.biproduct_ι_comp_leftDistributor_hom_assoc {C : Type u_1} [] {J : Type} [] (X : C) (f : JC) (j : J) {Z : C} (h : ( fun (j : J) => ) Z) :
@[simp]
theorem CategoryTheory.biproduct_ι_comp_leftDistributor_hom {C : Type u_1} [] {J : Type} [] (X : C) (f : JC) (j : J) :
@[simp]
theorem CategoryTheory.leftDistributor_inv_comp_biproduct_π_assoc {C : Type u_1} [] {J : Type} [] (X : C) (f : JC) (j : J) {Z : C} (h : ) :
@[simp]
theorem CategoryTheory.leftDistributor_inv_comp_biproduct_π {C : Type u_1} [] {J : Type} [] (X : C) (f : JC) (j : J) :
@[simp]
theorem CategoryTheory.biproduct_ι_comp_leftDistributor_inv_assoc {C : Type u_1} [] {J : Type} [] (X : C) (f : JC) (j : J) {Z : C} (h : ) :
@[simp]
theorem CategoryTheory.biproduct_ι_comp_leftDistributor_inv {C : Type u_1} [] {J : Type} [] (X : C) (f : JC) (j : J) :
theorem CategoryTheory.leftDistributor_assoc {C : Type u_1} [] {J : Type} [] (X : C) (Y : C) (f : JC) :
( ≪≫ CategoryTheory.leftDistributor X fun (j : J) => ) = ().symm ≪≫
def CategoryTheory.rightDistributor {C : Type u_1} [] {J : Type} [] (f : JC) (X : C) :
fun (j : J) =>

The isomorphism showing how tensor product on the right distributes over direct sums.

Equations
• = .mapBiproduct f
Instances For
theorem CategoryTheory.rightDistributor_hom {C : Type u_1} [] {J : Type} [] (f : JC) (X : C) :
.hom = j : J,
theorem CategoryTheory.rightDistributor_inv {C : Type u_1} [] {J : Type} [] (f : JC) (X : C) :
.inv = j : J,
@[simp]
theorem CategoryTheory.rightDistributor_hom_comp_biproduct_π_assoc {C : Type u_1} [] {J : Type} [] (f : JC) (X : C) (j : J) {Z : C} (h : ) :
@[simp]
theorem CategoryTheory.rightDistributor_hom_comp_biproduct_π {C : Type u_1} [] {J : Type} [] (f : JC) (X : C) (j : J) :
@[simp]
theorem CategoryTheory.biproduct_ι_comp_rightDistributor_hom_assoc {C : Type u_1} [] {J : Type} [] (f : JC) (X : C) (j : J) {Z : C} (h : ( fun (j : J) => ) Z) :
@[simp]
theorem CategoryTheory.biproduct_ι_comp_rightDistributor_hom {C : Type u_1} [] {J : Type} [] (f : JC) (X : C) (j : J) :
@[simp]
theorem CategoryTheory.rightDistributor_inv_comp_biproduct_π_assoc {C : Type u_1} [] {J : Type} [] (f : JC) (X : C) (j : J) {Z : C} (h : ) :
@[simp]
theorem CategoryTheory.rightDistributor_inv_comp_biproduct_π {C : Type u_1} [] {J : Type} [] (f : JC) (X : C) (j : J) :
@[simp]
theorem CategoryTheory.biproduct_ι_comp_rightDistributor_inv_assoc {C : Type u_1} [] {J : Type} [] (f : JC) (X : C) (j : J) {Z : C} (h : ) :
@[simp]
theorem CategoryTheory.biproduct_ι_comp_rightDistributor_inv {C : Type u_1} [] {J : Type} [] (f : JC) (X : C) (j : J) :
theorem CategoryTheory.rightDistributor_assoc {C : Type u_1} [] {J : Type} [] (f : JC) (X : C) (Y : C) :
theorem CategoryTheory.leftDistributor_rightDistributor_assoc {C : Type u_1} [] {J : Type} [] (X : C) (f : JC) (Y : C) :
theorem CategoryTheory.leftDistributor_ext_left {C : Type u_1} [] {J : Type} [] {X : C} {Y : C} {f : JC} {g : } {h : } (w : ) :
g = h
theorem CategoryTheory.leftDistributor_ext_right {C : Type u_1} [] {J : Type} [] {X : C} {Y : C} {f : JC} {g : } {h : } (w : ) :
g = h
theorem CategoryTheory.leftDistributor_ext₂_left {C : Type u_1} [] {J : Type} [] {X : C} {Y : C} {Z : C} {f : JC} (w : ∀ (j : J), = ) :
g = h
theorem CategoryTheory.leftDistributor_ext₂_right {C : Type u_1} [] {J : Type} [] {X : C} {Y : C} {Z : C} {f : JC} (w : ∀ (j : J), ) :
g = h
theorem CategoryTheory.rightDistributor_ext_left {C : Type u_1} [] {J : Type} [] {f : JC} {X : C} {Y : C} {g : } {h : } (w : ) :
g = h
theorem CategoryTheory.rightDistributor_ext_right {C : Type u_1} [] {J : Type} [] {f : JC} {X : C} {Y : C} {g : } {h : } (w : ) :
g = h
theorem CategoryTheory.rightDistributor_ext₂_left {C : Type u_1} [] {J : Type} [] {f : JC} {X : C} {Y : C} {Z : C} (w : ∀ (j : J), = ) :
g = h
theorem CategoryTheory.rightDistributor_ext₂_right {C : Type u_1} [] {J : Type} [] {f : JC} {X : C} {Y : C} {Z : C} (w : ∀ (j : J), ) :
g = h