Preadditive

📁 Source: Mathlib/CategoryTheory/Monoidal/Preadditive.lean

Statistics

Metric	Count
Definitions MonoidalPreadditive, leftDistributor, rightDistributor	3
Theorems add_tensor, add_whiskerRight, tensor_add, tensor_zero, whiskerLeft_add, whiskerLeft_zero, zero_tensor, zero_whiskerRight, biproduct_ι_comp_leftDistributor_hom, biproduct_ι_comp_leftDistributor_hom_assoc, biproduct_ι_comp_leftDistributor_inv, biproduct_ι_comp_leftDistributor_inv_assoc, biproduct_ι_comp_rightDistributor_hom, biproduct_ι_comp_rightDistributor_hom_assoc, biproduct_ι_comp_rightDistributor_inv, biproduct_ι_comp_rightDistributor_inv_assoc, instPreservesFiniteBiproductsTensorLeft, instPreservesFiniteBiproductsTensorRight, leftDistributor_assoc, leftDistributor_ext_left, leftDistributor_ext_left_iff, leftDistributor_ext_right, leftDistributor_ext_right_iff, leftDistributor_ext₂_left, leftDistributor_ext₂_left_iff, leftDistributor_ext₂_right, leftDistributor_ext₂_right_iff, leftDistributor_hom, leftDistributor_hom_comp_biproduct_π, leftDistributor_hom_comp_biproduct_π_assoc, leftDistributor_inv, leftDistributor_inv_comp_biproduct_π, leftDistributor_inv_comp_biproduct_π_assoc, leftDistributor_rightDistributor_assoc, monoidalPreadditive_of_faithful, rightDistributor_assoc, rightDistributor_ext_left, rightDistributor_ext_left_iff, rightDistributor_ext_right, rightDistributor_ext_right_iff, rightDistributor_ext₂_left, rightDistributor_ext₂_left_iff, rightDistributor_ext₂_right, rightDistributor_ext₂_right_iff, rightDistributor_hom, rightDistributor_hom_comp_biproduct_π, rightDistributor_hom_comp_biproduct_π_assoc, rightDistributor_inv, rightDistributor_inv_comp_biproduct_π, rightDistributor_inv_comp_biproduct_π_assoc, sum_tensor, sum_whiskerRight, tensorLeft_additive, tensorRight_additive, tensor_sum, tensoringLeft_additive, tensoringRight_additive, whiskerLeft_sum	58
Total	61

CategoryTheory

Definitions

Name	Category	Theorems
MonoidalPreadditive 📖	CompData	4 math math: monoidalPreadditive_of_faithful, ObjectProperty.instMonoidalPreadditiveFullSubcategory, Action.instMonoidalPreadditive, ModuleCat.instMonoidalPreadditive
leftDistributor 📖	CompOp	12 math math: biproduct_ι_comp_leftDistributor_hom_assoc, leftDistributor_hom, leftDistributor_hom_comp_biproduct_π, biproduct_ι_comp_leftDistributor_hom, leftDistributor_rightDistributor_assoc, leftDistributor_inv, leftDistributor_inv_comp_biproduct_π_assoc, biproduct_ι_comp_leftDistributor_inv, leftDistributor_hom_comp_biproduct_π_assoc, leftDistributor_assoc, biproduct_ι_comp_leftDistributor_inv_assoc, leftDistributor_inv_comp_biproduct_π
rightDistributor 📖	CompOp	12 math math: biproduct_ι_comp_rightDistributor_inv, biproduct_ι_comp_rightDistributor_hom, rightDistributor_hom_comp_biproduct_π_assoc, rightDistributor_inv_comp_biproduct_π, rightDistributor_inv, biproduct_ι_comp_rightDistributor_hom_assoc, rightDistributor_assoc, leftDistributor_rightDistributor_assoc, biproduct_ι_comp_rightDistributor_inv_assoc, rightDistributor_inv_comp_biproduct_π_assoc, rightDistributor_hom_comp_biproduct_π, rightDistributor_hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
biproduct_ι_comp_leftDistributor_hom 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.biproduct Preadditive.preadditiveHasZeroMorphisms Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite MonoidalCategoryStruct.whiskerLeft Limits.biproduct.ι Iso.hom leftDistributor	—	nonempty_fintype Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite Finite.of_fintype leftDistributor_hom Preadditive.comp_sum Finset.sum_congr Limits.biproduct.ι_π MonoidalCategory.whiskerLeft_dite MonoidalCategory.whiskerLeft_eqToHom MonoidalPreadditive.whiskerLeft_zero dite_comp Limits.zero_comp Finset.sum_dite_eq Category.id_comp
biproduct_ι_comp_leftDistributor_hom_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.biproduct Preadditive.preadditiveHasZeroMorphisms Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite MonoidalCategoryStruct.whiskerLeft Limits.biproduct.ι Iso.hom leftDistributor	—	Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' biproduct_ι_comp_leftDistributor_hom
biproduct_ι_comp_leftDistributor_inv 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.biproduct Preadditive.preadditiveHasZeroMorphisms Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite Limits.biproduct.ι Iso.inv leftDistributor MonoidalCategoryStruct.whiskerLeft	—	nonempty_fintype Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite Finite.of_fintype leftDistributor_inv Preadditive.comp_sum Finset.sum_congr Limits.biproduct.ι_π_assoc dite_comp Limits.zero_comp Finset.sum_dite_eq Category.id_comp
biproduct_ι_comp_leftDistributor_inv_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.biproduct Preadditive.preadditiveHasZeroMorphisms Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite Limits.biproduct.ι Iso.inv leftDistributor MonoidalCategoryStruct.whiskerLeft	—	Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' biproduct_ι_comp_leftDistributor_inv
biproduct_ι_comp_rightDistributor_hom 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.biproduct Preadditive.preadditiveHasZeroMorphisms Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite MonoidalCategoryStruct.whiskerRight Limits.biproduct.ι Iso.hom rightDistributor	—	nonempty_fintype Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite Finite.of_fintype rightDistributor_hom Preadditive.comp_sum Finset.sum_congr Limits.biproduct.ι_π MonoidalCategory.dite_whiskerRight MonoidalCategory.eqToHom_whiskerRight MonoidalPreadditive.zero_whiskerRight dite_comp Limits.zero_comp Finset.sum_dite_eq Category.id_comp
biproduct_ι_comp_rightDistributor_hom_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.biproduct Preadditive.preadditiveHasZeroMorphisms Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite MonoidalCategoryStruct.whiskerRight Limits.biproduct.ι Iso.hom rightDistributor	—	Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' biproduct_ι_comp_rightDistributor_hom
biproduct_ι_comp_rightDistributor_inv 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.biproduct Preadditive.preadditiveHasZeroMorphisms Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite Limits.biproduct.ι Iso.inv rightDistributor MonoidalCategoryStruct.whiskerRight	—	nonempty_fintype Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite Finite.of_fintype rightDistributor_inv Preadditive.comp_sum Finset.sum_congr Limits.biproduct.ι_π_assoc dite_comp Limits.zero_comp Finset.sum_dite_eq Category.id_comp
biproduct_ι_comp_rightDistributor_inv_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.biproduct Preadditive.preadditiveHasZeroMorphisms Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite Limits.biproduct.ι Iso.inv rightDistributor MonoidalCategoryStruct.whiskerRight	—	Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' biproduct_ι_comp_rightDistributor_inv
instPreservesFiniteBiproductsTensorLeft 📖	mathematical	—	Limits.PreservesFiniteBiproducts Preadditive.preadditiveHasZeroMorphisms MonoidalCategory.tensorLeft Functor.preservesZeroMorphisms_of_additive tensoringLeft_additive	—	Functor.preservesZeroMorphisms_of_additive tensoringLeft_additive nonempty_fintype Finset.sum_congr MonoidalCategory.tensorHom_comp_tensorHom Category.comp_id Limits.IsBilimit.total
instPreservesFiniteBiproductsTensorRight 📖	mathematical	—	Limits.PreservesFiniteBiproducts Preadditive.preadditiveHasZeroMorphisms MonoidalCategory.tensorRight Functor.preservesZeroMorphisms_of_additive tensoringRight_additive	—	Functor.preservesZeroMorphisms_of_additive tensoringRight_additive nonempty_fintype Finset.sum_congr MonoidalCategory.tensorHom_comp_tensorHom Category.comp_id Limits.IsBilimit.total
leftDistributor_assoc 📖	mathematical	—	Iso.trans MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.biproduct Preadditive.preadditiveHasZeroMorphisms Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite MonoidalCategory.tensorIso asIso CategoryStruct.id Category.toCategoryStruct IsIso.id leftDistributor Iso.symm MonoidalCategoryStruct.associator Limits.biproduct.mapIso	—	nonempty_fintype Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite IsIso.id Iso.ext Limits.biproduct.hom_ext Finite.of_fintype leftDistributor_hom tensor_sum Finset.sum_congr MonoidalCategory.id_tensor_comp Preadditive.comp_sum Preadditive.sum_comp Category.assoc Limits.biproduct.ι_π comp_dite Limits.comp_zero Finset.sum_dite_irrel Finset.sum_const_zero Finset.sum_dite_eq' Category.comp_id Limits.biproduct.ι_map MonoidalCategory.tensor_dite MonoidalCategory.id_tensorHom MonoidalCategory.whiskerLeft_eqToHom MonoidalPreadditive.whiskerLeft_zero MonoidalCategory.tensor_whiskerLeft Iso.inv_hom_id Iso.inv_hom_id_assoc
leftDistributor_ext_left 📖	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.biproduct Preadditive.preadditiveHasZeroMorphisms Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite MonoidalCategoryStruct.whiskerLeft Limits.biproduct.ι	—	—	Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite nonempty_fintype cancel_epi epi_of_strongEpi strongEpi_of_isIso Iso.isIso_inv Limits.biproduct.hom_ext' biproduct_ι_comp_leftDistributor_inv_assoc
leftDistributor_ext_left_iff 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.biproduct Preadditive.preadditiveHasZeroMorphisms Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite MonoidalCategoryStruct.whiskerLeft Limits.biproduct.ι	—	Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite leftDistributor_ext_left
leftDistributor_ext_right 📖	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.biproduct Preadditive.preadditiveHasZeroMorphisms Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite MonoidalCategoryStruct.whiskerLeft Limits.biproduct.π	—	—	Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite nonempty_fintype cancel_mono mono_of_strongMono strongMono_of_isIso Iso.isIso_hom Limits.biproduct.hom_ext Category.assoc leftDistributor_hom_comp_biproduct_π
leftDistributor_ext_right_iff 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.biproduct Preadditive.preadditiveHasZeroMorphisms Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite MonoidalCategoryStruct.whiskerLeft Limits.biproduct.π	—	Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite leftDistributor_ext_right
leftDistributor_ext₂_left 📖	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.biproduct Preadditive.preadditiveHasZeroMorphisms Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite MonoidalCategoryStruct.whiskerLeft Limits.biproduct.ι	—	—	Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite cancel_epi epi_of_strongEpi strongEpi_of_isIso Iso.isIso_hom leftDistributor_ext_left MonoidalCategory.tensor_whiskerLeft Category.assoc Iso.inv_hom_id_assoc
leftDistributor_ext₂_left_iff 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.biproduct Preadditive.preadditiveHasZeroMorphisms Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite MonoidalCategoryStruct.whiskerLeft Limits.biproduct.ι	—	Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite leftDistributor_ext₂_left
leftDistributor_ext₂_right 📖	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.biproduct Preadditive.preadditiveHasZeroMorphisms Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite MonoidalCategoryStruct.whiskerLeft Limits.biproduct.π	—	—	Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite cancel_mono mono_of_strongMono strongMono_of_isIso Iso.isIso_inv leftDistributor_ext_right MonoidalCategory.tensor_whiskerLeft Category.assoc Iso.inv_hom_id_assoc
leftDistributor_ext₂_right_iff 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.biproduct Preadditive.preadditiveHasZeroMorphisms Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite MonoidalCategoryStruct.whiskerLeft Limits.biproduct.π	—	Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite leftDistributor_ext₂_right
leftDistributor_hom 📖	mathematical	—	Iso.hom MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.biproduct Preadditive.preadditiveHasZeroMorphisms Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite Finite.of_fintype leftDistributor Finset.sum Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct AddCommGroup.toAddCommMonoid Preadditive.homGroup Finset.univ CategoryStruct.comp MonoidalCategoryStruct.whiskerLeft Limits.biproduct.π Limits.biproduct.ι	—	Limits.biproduct.hom_ext Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite Finite.of_fintype Functor.hasBiproduct_of_preserves Limits.biproduct.lift_π Preadditive.sum_comp Finset.sum_congr Category.assoc Limits.biproduct.ι_π comp_dite Limits.comp_zero Finset.sum_dite_eq' Category.comp_id
leftDistributor_hom_comp_biproduct_π 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.biproduct Preadditive.preadditiveHasZeroMorphisms Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite Iso.hom leftDistributor Limits.biproduct.π MonoidalCategoryStruct.whiskerLeft	—	nonempty_fintype Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite Finite.of_fintype leftDistributor_hom Preadditive.sum_comp Finset.sum_congr Category.assoc Limits.biproduct.ι_π comp_dite Limits.comp_zero Finset.sum_dite_eq' Category.comp_id
leftDistributor_hom_comp_biproduct_π_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.biproduct Preadditive.preadditiveHasZeroMorphisms Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite Iso.hom leftDistributor Limits.biproduct.π MonoidalCategoryStruct.whiskerLeft	—	Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftDistributor_hom_comp_biproduct_π
leftDistributor_inv 📖	mathematical	—	Iso.inv MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.biproduct Preadditive.preadditiveHasZeroMorphisms Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite Finite.of_fintype leftDistributor Finset.sum Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct AddCommGroup.toAddCommMonoid Preadditive.homGroup Finset.univ CategoryStruct.comp Limits.biproduct.π MonoidalCategoryStruct.whiskerLeft Limits.biproduct.ι	—	Limits.biproduct.hom_ext' Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite Finite.of_fintype Functor.hasBiproduct_of_preserves Limits.biproduct.ι_desc Preadditive.comp_sum Finset.sum_congr Limits.biproduct.ι_π_assoc dite_comp Limits.zero_comp Finset.sum_dite_eq Category.id_comp
leftDistributor_inv_comp_biproduct_π 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Limits.biproduct Preadditive.preadditiveHasZeroMorphisms MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite Iso.inv leftDistributor MonoidalCategoryStruct.whiskerLeft Limits.biproduct.π	—	nonempty_fintype Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite Finite.of_fintype leftDistributor_inv Preadditive.sum_comp Finset.sum_congr Category.assoc Limits.biproduct.ι_π MonoidalCategory.whiskerLeft_dite MonoidalCategory.whiskerLeft_eqToHom MonoidalPreadditive.whiskerLeft_zero comp_dite Limits.comp_zero Finset.sum_dite_eq' Category.comp_id
leftDistributor_inv_comp_biproduct_π_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Limits.biproduct Preadditive.preadditiveHasZeroMorphisms MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite Iso.inv leftDistributor MonoidalCategoryStruct.whiskerLeft Limits.biproduct.π	—	Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' leftDistributor_inv_comp_biproduct_π
leftDistributor_rightDistributor_assoc 📖	mathematical	—	Iso.trans MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.biproduct Preadditive.preadditiveHasZeroMorphisms Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite MonoidalCategory.tensorIso leftDistributor asIso CategoryStruct.id Category.toCategoryStruct IsIso.id rightDistributor MonoidalCategoryStruct.associator Limits.biproduct.mapIso Iso.symm	—	nonempty_fintype Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite IsIso.id Iso.ext Limits.biproduct.hom_ext Finite.of_fintype leftDistributor_hom sum_tensor Finset.sum_congr MonoidalCategory.comp_tensor_id rightDistributor_hom Preadditive.comp_sum Preadditive.sum_comp Category.assoc Limits.biproduct.ι_π comp_dite Limits.comp_zero Finset.sum_dite_irrel Finset.sum_const_zero Finset.sum_dite_eq' Category.comp_id tensor_sum Limits.biproduct.ι_map MonoidalCategory.dite_tensor MonoidalCategory.tensor_dite dite_comp MonoidalCategory.id_tensorHom MonoidalCategory.tensorHom_id MonoidalCategory.comp_whiskerRight MonoidalCategory.whisker_assoc MonoidalCategory.eqToHom_whiskerRight MonoidalPreadditive.zero_whiskerRight MonoidalCategory.whiskerLeft_comp MonoidalCategory.whiskerLeft_eqToHom MonoidalPreadditive.whiskerLeft_zero Limits.zero_comp Category.id_comp
monoidalPreadditive_of_faithful 📖	mathematical	—	MonoidalPreadditive	—	Functor.map_injective Functor.Monoidal.map_whiskerLeft Functor.map_zero Functor.preservesZeroMorphisms_of_additive MonoidalPreadditive.whiskerLeft_zero Limits.zero_comp Limits.comp_zero Functor.Monoidal.map_whiskerRight MonoidalPreadditive.zero_whiskerRight Functor.map_add MonoidalPreadditive.whiskerLeft_add Preadditive.add_comp Preadditive.comp_add MonoidalPreadditive.add_whiskerRight
rightDistributor_assoc 📖	mathematical	—	Iso.trans MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.biproduct Preadditive.preadditiveHasZeroMorphisms Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite MonoidalCategory.tensorIso rightDistributor asIso CategoryStruct.id Category.toCategoryStruct IsIso.id MonoidalCategoryStruct.associator Limits.biproduct.mapIso Iso.symm	—	nonempty_fintype Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite IsIso.id Iso.ext Limits.biproduct.hom_ext Finite.of_fintype rightDistributor_hom sum_tensor Finset.sum_congr MonoidalCategory.comp_tensor_id Preadditive.comp_sum Preadditive.sum_comp Category.assoc Limits.biproduct.ι_π comp_dite Limits.comp_zero Finset.sum_dite_irrel Finset.sum_const_zero Finset.sum_dite_eq' Category.comp_id Limits.biproduct.ι_map MonoidalCategory.dite_tensor MonoidalCategory.tensorHom_id MonoidalCategory.comp_whiskerRight MonoidalCategory.eqToHom_whiskerRight MonoidalPreadditive.zero_whiskerRight MonoidalCategory.whiskerRight_tensor Iso.hom_inv_id Iso.hom_inv_id_assoc
rightDistributor_ext_left 📖	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.biproduct Preadditive.preadditiveHasZeroMorphisms Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite MonoidalCategoryStruct.whiskerRight Limits.biproduct.ι	—	—	Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite nonempty_fintype cancel_epi epi_of_strongEpi strongEpi_of_isIso Iso.isIso_inv Limits.biproduct.hom_ext' biproduct_ι_comp_rightDistributor_inv_assoc
rightDistributor_ext_left_iff 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.biproduct Preadditive.preadditiveHasZeroMorphisms Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite MonoidalCategoryStruct.whiskerRight Limits.biproduct.ι	—	Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite rightDistributor_ext_left
rightDistributor_ext_right 📖	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.biproduct Preadditive.preadditiveHasZeroMorphisms Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite MonoidalCategoryStruct.whiskerRight Limits.biproduct.π	—	—	Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite nonempty_fintype cancel_mono mono_of_strongMono strongMono_of_isIso Iso.isIso_hom Limits.biproduct.hom_ext Category.assoc rightDistributor_hom_comp_biproduct_π
rightDistributor_ext_right_iff 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.biproduct Preadditive.preadditiveHasZeroMorphisms Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite MonoidalCategoryStruct.whiskerRight Limits.biproduct.π	—	Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite rightDistributor_ext_right
rightDistributor_ext₂_left 📖	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.biproduct Preadditive.preadditiveHasZeroMorphisms Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite MonoidalCategoryStruct.whiskerRight Limits.biproduct.ι	—	—	Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite cancel_epi epi_of_strongEpi strongEpi_of_isIso Iso.isIso_inv rightDistributor_ext_left MonoidalCategory.whiskerRight_tensor Category.assoc Iso.hom_inv_id_assoc
rightDistributor_ext₂_left_iff 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.biproduct Preadditive.preadditiveHasZeroMorphisms Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite MonoidalCategoryStruct.whiskerRight Limits.biproduct.ι	—	Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite rightDistributor_ext₂_left
rightDistributor_ext₂_right 📖	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.biproduct Preadditive.preadditiveHasZeroMorphisms Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite MonoidalCategoryStruct.whiskerRight Limits.biproduct.π	—	—	Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite cancel_mono mono_of_strongMono strongMono_of_isIso Iso.isIso_hom rightDistributor_ext_right MonoidalCategory.whiskerRight_tensor Category.assoc Iso.hom_inv_id_assoc
rightDistributor_ext₂_right_iff 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.biproduct Preadditive.preadditiveHasZeroMorphisms Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite MonoidalCategoryStruct.whiskerRight Limits.biproduct.π	—	Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite rightDistributor_ext₂_right
rightDistributor_hom 📖	mathematical	—	Iso.hom MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.biproduct Preadditive.preadditiveHasZeroMorphisms Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite Finite.of_fintype rightDistributor Finset.sum Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct AddCommGroup.toAddCommMonoid Preadditive.homGroup Finset.univ CategoryStruct.comp MonoidalCategoryStruct.whiskerRight Limits.biproduct.π Limits.biproduct.ι	—	Limits.biproduct.hom_ext Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite Finite.of_fintype Functor.hasBiproduct_of_preserves Limits.biproduct.lift_π Preadditive.sum_comp Finset.sum_congr Category.assoc Limits.biproduct.ι_π comp_dite Limits.comp_zero Finset.sum_dite_eq' Category.comp_id
rightDistributor_hom_comp_biproduct_π 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.biproduct Preadditive.preadditiveHasZeroMorphisms Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite Iso.hom rightDistributor Limits.biproduct.π MonoidalCategoryStruct.whiskerRight	—	nonempty_fintype Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite Finite.of_fintype rightDistributor_hom Preadditive.sum_comp Finset.sum_congr Category.assoc Limits.biproduct.ι_π comp_dite Limits.comp_zero Finset.sum_dite_eq' Category.comp_id
rightDistributor_hom_comp_biproduct_π_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.biproduct Preadditive.preadditiveHasZeroMorphisms Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite Iso.hom rightDistributor Limits.biproduct.π MonoidalCategoryStruct.whiskerRight	—	Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' rightDistributor_hom_comp_biproduct_π
rightDistributor_inv 📖	mathematical	—	Iso.inv MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.biproduct Preadditive.preadditiveHasZeroMorphisms Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite Finite.of_fintype rightDistributor Finset.sum Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct AddCommGroup.toAddCommMonoid Preadditive.homGroup Finset.univ CategoryStruct.comp Limits.biproduct.π MonoidalCategoryStruct.whiskerRight Limits.biproduct.ι	—	Limits.biproduct.hom_ext' Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite Finite.of_fintype Functor.hasBiproduct_of_preserves Limits.biproduct.ι_desc Preadditive.comp_sum Finset.sum_congr Limits.biproduct.ι_π_assoc dite_comp Limits.zero_comp Finset.sum_dite_eq Category.id_comp
rightDistributor_inv_comp_biproduct_π 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Limits.biproduct Preadditive.preadditiveHasZeroMorphisms MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite Iso.inv rightDistributor MonoidalCategoryStruct.whiskerRight Limits.biproduct.π	—	nonempty_fintype Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite Finite.of_fintype rightDistributor_inv Preadditive.sum_comp Finset.sum_congr Category.assoc Limits.biproduct.ι_π MonoidalCategory.dite_whiskerRight MonoidalCategory.eqToHom_whiskerRight MonoidalPreadditive.zero_whiskerRight comp_dite Limits.comp_zero Finset.sum_dite_eq' Category.comp_id
rightDistributor_inv_comp_biproduct_π_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Limits.biproduct Preadditive.preadditiveHasZeroMorphisms MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite Iso.inv rightDistributor MonoidalCategoryStruct.whiskerRight Limits.biproduct.π	—	Limits.HasBiproductsOfShape.has_biproduct Limits.hasBiproductsOfShape_finite Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' rightDistributor_inv_comp_biproduct_π
sum_tensor 📖	mathematical	—	MonoidalCategoryStruct.tensorHom MonoidalCategory.toMonoidalCategoryStruct Finset.sum Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct AddCommGroup.toAddCommMonoid Preadditive.homGroup MonoidalCategoryStruct.tensorObj	—	MonoidalCategory.tensorHom_def sum_whiskerRight Preadditive.sum_comp Finset.sum_congr
sum_whiskerRight 📖	mathematical	—	MonoidalCategoryStruct.whiskerRight MonoidalCategory.toMonoidalCategoryStruct Finset.sum Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct AddCommGroup.toAddCommMonoid Preadditive.homGroup MonoidalCategoryStruct.tensorObj	—	map_sum AddMonoidHom.instAddMonoidHomClass tensoringRight_additive
tensorLeft_additive 📖	mathematical	—	Functor.Additive MonoidalCategory.tensorLeft	—	MonoidalPreadditive.whiskerLeft_add
tensorRight_additive 📖	mathematical	—	Functor.Additive MonoidalCategory.tensorRight	—	MonoidalPreadditive.add_whiskerRight
tensor_sum 📖	mathematical	—	MonoidalCategoryStruct.tensorHom MonoidalCategory.toMonoidalCategoryStruct Finset.sum Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct AddCommGroup.toAddCommMonoid Preadditive.homGroup MonoidalCategoryStruct.tensorObj	—	MonoidalCategory.tensorHom_def whiskerLeft_sum Preadditive.comp_sum Finset.sum_congr
tensoringLeft_additive 📖	mathematical	—	Functor.Additive Functor.obj Functor Functor.category MonoidalCategory.tensoringLeft	—	MonoidalPreadditive.whiskerLeft_add
tensoringRight_additive 📖	mathematical	—	Functor.Additive Functor.obj Functor Functor.category MonoidalCategory.tensoringRight	—	MonoidalPreadditive.add_whiskerRight
whiskerLeft_sum 📖	mathematical	—	MonoidalCategoryStruct.whiskerLeft MonoidalCategory.toMonoidalCategoryStruct Finset.sum Quiver.Hom CategoryStruct.toQuiver Category.toCategoryStruct AddCommGroup.toAddCommMonoid Preadditive.homGroup MonoidalCategoryStruct.tensorObj	—	map_sum AddMonoidHom.instAddMonoidHomClass tensoringLeft_additive

CategoryTheory.MonoidalPreadditive

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_tensor 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.MonoidalCategoryStruct.tensorObj	—	CategoryTheory.MonoidalCategory.tensorHom_def add_whiskerRight CategoryTheory.Preadditive.add_comp
add_whiskerRight 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.MonoidalCategoryStruct.tensorObj	—	—
tensor_add 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.MonoidalCategoryStruct.tensorObj	—	CategoryTheory.MonoidalCategory.tensorHom_def whiskerLeft_add CategoryTheory.Preadditive.comp_add
tensor_zero 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.MonoidalCategoryStruct.tensorObj	—	CategoryTheory.MonoidalCategory.tensorHom_def whiskerLeft_zero CategoryTheory.Limits.comp_zero
whiskerLeft_add 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid CategoryTheory.Preadditive.homGroup CategoryTheory.MonoidalCategoryStruct.tensorObj	—	—
whiskerLeft_zero 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.MonoidalCategoryStruct.tensorObj	—	—
zero_tensor 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.MonoidalCategoryStruct.tensorObj	—	CategoryTheory.MonoidalCategory.tensorHom_def zero_whiskerRight CategoryTheory.Limits.zero_comp
zero_whiskerRight 📖	mathematical	—	CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.HasZeroMorphisms.zero CategoryTheory.Preadditive.preadditiveHasZeroMorphisms CategoryTheory.MonoidalCategoryStruct.tensorObj	—	—

---

← Back to Index