Monoidal

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

Statistics

Metric	Count
Definitions «term∂L», «term∂R», IsMonoidalDistrib, IsMonoidalLeftDistrib, IsMonoidalRightDistrib, leftDistrib, rightDistrib	7
Theorems of_MonoidalPreadditive_with_binary_coproducts, toIsMonoidalLeftDistrib, toIsMonoidalRightDistrib, of_isIso_coprodComparisonTensorLeft, preservesBinaryCoproducts_tensorLeft, of_isIso_coprodComparisonTensorRight, preservesBinaryCoproducts_tensorRight, isMonoidalLeftDistrib, leftDistrib_inv, isMonoidalDistrib_of_isMonoidalLeftDistrib, rightDistrib_of_leftDistrib, coprodComparison_tensorLeft_braiding_hom, coprodComparison_tensorRight_braiding_hom, coprod_inl_leftDistrib_hom, coprod_inl_leftDistrib_hom_assoc, coprod_inl_rightDistrib_hom, coprod_inl_rightDistrib_hom_assoc, coprod_inr_leftDistrib_hom, coprod_inr_leftDistrib_hom_assoc, coprod_inr_rightDistrib_hom, coprod_inr_rightDistrib_hom_assoc, of_symmetric_monoidal_closed, of_endofunctors, leftDistrib_hom, rightDistrib_hom, whiskerLeft_coprod_inl_leftDistrib_inv, whiskerLeft_coprod_inl_leftDistrib_inv_assoc, whiskerLeft_coprod_inr_leftDistrib_inv, whiskerLeft_coprod_inr_leftDistrib_inv_assoc, whiskerRight_coprod_inl_rightDistrib_inv, whiskerRight_coprod_inl_rightDistrib_inv_assoc, whiskerRight_coprod_inr_rightDistrib_inv, whiskerRight_coprod_inr_rightDistrib_inv_assoc	33
Total	40

CategoryTheory

Definitions

Name	Category	Theorems
IsMonoidalDistrib 📖	CompData	3 math math: SymmetricCategory.isMonoidalDistrib_of_isMonoidalLeftDistrib, isMonoidalDistrib.of_symmetric_monoidal_closed, IsMonoidalDistrib.of_MonoidalPreadditive_with_binary_coproducts
IsMonoidalLeftDistrib 📖	CompData	4 math math: IsMonoidalDistrib.toIsMonoidalLeftDistrib, IsMonoidalLeftDistrib.of_isIso_coprodComparisonTensorLeft, MonoidalClosed.isMonoidalLeftDistrib, isMonoidalLeftDistrib.of_endofunctors
IsMonoidalRightDistrib 📖	CompData	2 math math: IsMonoidalRightDistrib.of_isIso_coprodComparisonTensorRight, IsMonoidalDistrib.toIsMonoidalRightDistrib
leftDistrib 📖	CompOp	11 math math: whiskerLeft_coprod_inr_leftDistrib_inv, coprod_inl_leftDistrib_hom, whiskerLeft_coprod_inl_leftDistrib_inv, whiskerLeft_coprod_inl_leftDistrib_inv_assoc, coprod_inl_leftDistrib_hom_assoc, coprod_inr_leftDistrib_hom, SymmetricCategory.rightDistrib_of_leftDistrib, coprod_inr_leftDistrib_hom_assoc, leftDistrib_hom, MonoidalClosed.leftDistrib_inv, whiskerLeft_coprod_inr_leftDistrib_inv_assoc
rightDistrib 📖	CompOp	10 math math: coprod_inr_rightDistrib_hom_assoc, whiskerRight_coprod_inr_rightDistrib_inv_assoc, whiskerRight_coprod_inl_rightDistrib_inv, coprod_inl_rightDistrib_hom, coprod_inr_rightDistrib_hom, SymmetricCategory.rightDistrib_of_leftDistrib, whiskerRight_coprod_inl_rightDistrib_inv_assoc, whiskerRight_coprod_inr_rightDistrib_inv, rightDistrib_hom, coprod_inl_rightDistrib_hom_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coprodComparison_tensorLeft_braiding_hom 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Limits.coprod Functor.obj MonoidalCategory.tensorLeft Limits.hasColimitOfHasColimitsOfShape Discrete Limits.WalkingPair discreteCategory Limits.pair MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.coprodComparison Iso.hom BraidedCategory.braiding MonoidalCategory.tensorRight Limits.coprod.map	—	Limits.hasColimitOfHasColimitsOfShape Limits.coprod.desc_comp BraidedCategory.braiding_naturality_right Limits.coprod.map_desc
coprodComparison_tensorRight_braiding_hom 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct Limits.coprod Functor.obj MonoidalCategory.tensorRight Limits.hasColimitOfHasColimitsOfShape Discrete Limits.WalkingPair discreteCategory Limits.pair MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.coprodComparison Iso.hom BraidedCategory.braiding SymmetricCategory.toBraidedCategory MonoidalCategory.tensorLeft Limits.coprod.map	—	Limits.hasColimitOfHasColimitsOfShape Limits.coprod.desc_comp BraidedCategory.braiding_naturality_left Limits.coprod.map_desc
coprod_inl_leftDistrib_hom 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.coprod Limits.hasColimitOfHasColimitsOfShape Discrete Limits.WalkingPair discreteCategory Limits.pair Limits.coprod.inl Iso.hom leftDistrib MonoidalCategoryStruct.whiskerLeft	—	Limits.hasColimitOfHasColimitsOfShape leftDistrib_hom Limits.coprod.inl_desc
coprod_inl_leftDistrib_hom_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.coprod Limits.hasColimitOfHasColimitsOfShape Discrete Limits.WalkingPair discreteCategory Limits.pair Limits.coprod.inl Iso.hom leftDistrib MonoidalCategoryStruct.whiskerLeft	—	Limits.hasColimitOfHasColimitsOfShape Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' coprod_inl_leftDistrib_hom
coprod_inl_rightDistrib_hom 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.coprod Limits.hasColimitOfHasColimitsOfShape Discrete Limits.WalkingPair discreteCategory Limits.pair Limits.coprod.inl Iso.hom rightDistrib MonoidalCategoryStruct.whiskerRight	—	Limits.hasColimitOfHasColimitsOfShape rightDistrib_hom Limits.coprod.inl_desc
coprod_inl_rightDistrib_hom_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.coprod Limits.hasColimitOfHasColimitsOfShape Discrete Limits.WalkingPair discreteCategory Limits.pair Limits.coprod.inl Iso.hom rightDistrib MonoidalCategoryStruct.whiskerRight	—	Limits.hasColimitOfHasColimitsOfShape Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' coprod_inl_rightDistrib_hom
coprod_inr_leftDistrib_hom 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.coprod Limits.hasColimitOfHasColimitsOfShape Discrete Limits.WalkingPair discreteCategory Limits.pair Limits.coprod.inr Iso.hom leftDistrib MonoidalCategoryStruct.whiskerLeft	—	Limits.hasColimitOfHasColimitsOfShape leftDistrib_hom Limits.coprod.inr_desc
coprod_inr_leftDistrib_hom_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.coprod Limits.hasColimitOfHasColimitsOfShape Discrete Limits.WalkingPair discreteCategory Limits.pair Limits.coprod.inr Iso.hom leftDistrib MonoidalCategoryStruct.whiskerLeft	—	Limits.hasColimitOfHasColimitsOfShape Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' coprod_inr_leftDistrib_hom
coprod_inr_rightDistrib_hom 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.coprod Limits.hasColimitOfHasColimitsOfShape Discrete Limits.WalkingPair discreteCategory Limits.pair Limits.coprod.inr Iso.hom rightDistrib MonoidalCategoryStruct.whiskerRight	—	Limits.hasColimitOfHasColimitsOfShape rightDistrib_hom Limits.coprod.inr_desc
coprod_inr_rightDistrib_hom_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.coprod Limits.hasColimitOfHasColimitsOfShape Discrete Limits.WalkingPair discreteCategory Limits.pair Limits.coprod.inr Iso.hom rightDistrib MonoidalCategoryStruct.whiskerRight	—	Limits.hasColimitOfHasColimitsOfShape Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' coprod_inr_rightDistrib_hom
leftDistrib_hom 📖	mathematical	—	Iso.hom Limits.coprod MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.hasColimitOfHasColimitsOfShape Discrete Limits.WalkingPair discreteCategory Limits.pair leftDistrib Limits.coprod.desc MonoidalCategoryStruct.whiskerLeft Limits.coprod.inl Limits.coprod.inr	—	Limits.hasColimitOfHasColimitsOfShape
rightDistrib_hom 📖	mathematical	—	Iso.hom Limits.coprod MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.hasColimitOfHasColimitsOfShape Discrete Limits.WalkingPair discreteCategory Limits.pair rightDistrib Limits.coprod.desc MonoidalCategoryStruct.whiskerRight Limits.coprod.inl Limits.coprod.inr	—	Limits.hasColimitOfHasColimitsOfShape
whiskerLeft_coprod_inl_leftDistrib_inv 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.coprod Limits.hasColimitOfHasColimitsOfShape Discrete Limits.WalkingPair discreteCategory Limits.pair MonoidalCategoryStruct.whiskerLeft Limits.coprod.inl Iso.inv leftDistrib	—	Limits.hasColimitOfHasColimitsOfShape Iso.cancel_iso_hom_right Category.assoc Iso.inv_hom_id Category.comp_id coprod_inl_leftDistrib_hom
whiskerLeft_coprod_inl_leftDistrib_inv_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.coprod Limits.hasColimitOfHasColimitsOfShape Discrete Limits.WalkingPair discreteCategory Limits.pair MonoidalCategoryStruct.whiskerLeft Limits.coprod.inl Iso.inv leftDistrib	—	Limits.hasColimitOfHasColimitsOfShape Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' whiskerLeft_coprod_inl_leftDistrib_inv
whiskerLeft_coprod_inr_leftDistrib_inv 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.coprod Limits.hasColimitOfHasColimitsOfShape Discrete Limits.WalkingPair discreteCategory Limits.pair MonoidalCategoryStruct.whiskerLeft Limits.coprod.inr Iso.inv leftDistrib	—	Limits.hasColimitOfHasColimitsOfShape Iso.cancel_iso_hom_right Category.assoc Iso.inv_hom_id Category.comp_id coprod_inr_leftDistrib_hom
whiskerLeft_coprod_inr_leftDistrib_inv_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.coprod Limits.hasColimitOfHasColimitsOfShape Discrete Limits.WalkingPair discreteCategory Limits.pair MonoidalCategoryStruct.whiskerLeft Limits.coprod.inr Iso.inv leftDistrib	—	Limits.hasColimitOfHasColimitsOfShape Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' whiskerLeft_coprod_inr_leftDistrib_inv
whiskerRight_coprod_inl_rightDistrib_inv 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.coprod Limits.hasColimitOfHasColimitsOfShape Discrete Limits.WalkingPair discreteCategory Limits.pair MonoidalCategoryStruct.whiskerRight Limits.coprod.inl Iso.inv rightDistrib	—	Limits.hasColimitOfHasColimitsOfShape Iso.cancel_iso_hom_right Category.assoc Iso.inv_hom_id Category.comp_id coprod_inl_rightDistrib_hom
whiskerRight_coprod_inl_rightDistrib_inv_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.coprod Limits.hasColimitOfHasColimitsOfShape Discrete Limits.WalkingPair discreteCategory Limits.pair MonoidalCategoryStruct.whiskerRight Limits.coprod.inl Iso.inv rightDistrib	—	Limits.hasColimitOfHasColimitsOfShape Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' whiskerRight_coprod_inl_rightDistrib_inv
whiskerRight_coprod_inr_rightDistrib_inv 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.coprod Limits.hasColimitOfHasColimitsOfShape Discrete Limits.WalkingPair discreteCategory Limits.pair MonoidalCategoryStruct.whiskerRight Limits.coprod.inr Iso.inv rightDistrib	—	Limits.hasColimitOfHasColimitsOfShape Iso.cancel_iso_hom_right Category.assoc Iso.inv_hom_id Category.comp_id coprod_inr_rightDistrib_hom
whiskerRight_coprod_inr_rightDistrib_inv_assoc 📖	mathematical	—	CategoryStruct.comp Category.toCategoryStruct MonoidalCategoryStruct.tensorObj MonoidalCategory.toMonoidalCategoryStruct Limits.coprod Limits.hasColimitOfHasColimitsOfShape Discrete Limits.WalkingPair discreteCategory Limits.pair MonoidalCategoryStruct.whiskerRight Limits.coprod.inr Iso.inv rightDistrib	—	Limits.hasColimitOfHasColimitsOfShape Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' whiskerRight_coprod_inr_rightDistrib_inv

CategoryTheory.Distributive

Definitions

Name	Category	Theorems
«term∂L» 📖	CompOp	—
«term∂R» 📖	CompOp	—

CategoryTheory.IsMonoidalDistrib

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_MonoidalPreadditive_with_binary_coproducts 📖	mathematical	—	CategoryTheory.IsMonoidalDistrib	—	CategoryTheory.Limits.preservesBinaryCoproducts_of_preservesBinaryBiproducts CategoryTheory.Functor.preservesZeroMorphisms_of_additive CategoryTheory.tensoringLeft_additive CategoryTheory.Limits.preservesBinaryBiproducts_of_preservesBiproducts CategoryTheory.Limits.PreservesFiniteBiproducts.preserves CategoryTheory.instPreservesFiniteBiproductsTensorLeft Finite.of_fintype CategoryTheory.tensoringRight_additive CategoryTheory.instPreservesFiniteBiproductsTensorRight
toIsMonoidalLeftDistrib 📖	mathematical	—	CategoryTheory.IsMonoidalLeftDistrib	—	—
toIsMonoidalRightDistrib 📖	mathematical	—	CategoryTheory.IsMonoidalRightDistrib	—	—

CategoryTheory.IsMonoidalLeftDistrib

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_isIso_coprodComparisonTensorLeft 📖	mathematical	CategoryTheory.IsIso CategoryTheory.Limits.coprod CategoryTheory.Functor.obj CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair CategoryTheory.Limits.coprodComparison	CategoryTheory.IsMonoidalLeftDistrib	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.preservesBinaryCoproducts_of_isIso_coprodComparison
preservesBinaryCoproducts_tensorLeft 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.MonoidalCategory.tensorLeft	—	—

CategoryTheory.IsMonoidalRightDistrib

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_isIso_coprodComparisonTensorRight 📖	mathematical	CategoryTheory.IsIso CategoryTheory.Limits.coprod CategoryTheory.Functor.obj CategoryTheory.MonoidalCategory.tensorRight CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair CategoryTheory.Limits.coprodComparison	CategoryTheory.IsMonoidalRightDistrib	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.preservesBinaryCoproducts_of_isIso_coprodComparison
preservesBinaryCoproducts_tensorRight 📖	mathematical	—	CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.MonoidalCategory.tensorRight	—	—

CategoryTheory.MonoidalClosed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isMonoidalLeftDistrib 📖	mathematical	—	CategoryTheory.IsMonoidalLeftDistrib	—	CategoryTheory.Limits.PreservesFiniteColimits.preservesFiniteColimits CategoryTheory.Limits.PreservesColimits.preservesFiniteColimits CategoryTheory.instPreservesColimitsTensorLeft
leftDistrib_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Limits.coprod CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair CategoryTheory.leftDistrib isMonoidalLeftDistrib uncurry closed CategoryTheory.Limits.coprod.desc CategoryTheory.Functor.obj CategoryTheory.ihom curry CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr	—	CategoryTheory.Limits.hasColimitOfHasColimitsOfShape isMonoidalLeftDistrib curry_eq_iff CategoryTheory.Limits.coprod.hom_ext CategoryTheory.whiskerLeft_coprod_inl_leftDistrib_inv CategoryTheory.Limits.colimit.ι_desc CategoryTheory.whiskerLeft_coprod_inr_leftDistrib_inv

CategoryTheory.SymmetricCategory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isMonoidalDistrib_of_isMonoidalLeftDistrib 📖	mathematical	—	CategoryTheory.IsMonoidalDistrib	—	CategoryTheory.Limits.preservesColimitsOfShape_of_natIso CategoryTheory.IsMonoidalLeftDistrib.preservesBinaryCoproducts_tensorLeft
rightDistrib_of_leftDistrib 📖	mathematical	—	CategoryTheory.rightDistrib CategoryTheory.IsMonoidalDistrib.toIsMonoidalRightDistrib CategoryTheory.Iso.trans CategoryTheory.Limits.coprod CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory CategoryTheory.Limits.pair CategoryTheory.Limits.coprod.mapIso CategoryTheory.BraidedCategory.braiding toBraidedCategory CategoryTheory.leftDistrib CategoryTheory.IsMonoidalDistrib.toIsMonoidalLeftDistrib	—	CategoryTheory.Iso.ext CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.IsMonoidalDistrib.toIsMonoidalRightDistrib CategoryTheory.IsMonoidalDistrib.toIsMonoidalLeftDistrib CategoryTheory.Limits.coprod.hom_ext CategoryTheory.rightDistrib_hom CategoryTheory.Limits.colimit.ι_desc CategoryTheory.leftDistrib_hom CategoryTheory.Limits.coprod.desc_comp CategoryTheory.BraidedCategory.braiding_naturality_right CategoryTheory.Limits.coprod.map_desc symmetry_assoc

CategoryTheory.isMonoidalDistrib

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_symmetric_monoidal_closed 📖	mathematical	—	CategoryTheory.IsMonoidalDistrib	—	CategoryTheory.SymmetricCategory.isMonoidalDistrib_of_isMonoidalLeftDistrib CategoryTheory.MonoidalClosed.isMonoidalLeftDistrib

CategoryTheory.isMonoidalLeftDistrib

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_endofunctors 📖	mathematical	—	CategoryTheory.IsMonoidalLeftDistrib CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.endofunctorMonoidalCategory CategoryTheory.Limits.functorCategoryHasColimitsOfShape CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair CategoryTheory.discreteCategory	—	CategoryTheory.Limits.functorCategoryHasColimitsOfShape CategoryTheory.whiskeringLeft_preservesColimitsOfShape

---

← Back to Index