Documentation Verification Report

Monoidal

📁 Source: Mathlib/Algebra/Homology/Monoidal.lean

Statistics

Metric	Count
Definitions `HasGoodTensor₁₂`, `HasGoodTensor₂₃`, `HasTensor`, `inducingFunctorData`, `associator`, `leftUnitor`, `leftUnitor'`, `monoidalCategory`, `monoidalCategoryStruct`, `rightUnitor`, `rightUnitor'`, `tensorHom`, `tensorObj`, `tensorUnit`, `tensorUnitIso`, `ιTensorObj`	16
Theorems `instHasGoodTensor₁₂OfHasGoodTensor₁₂TensorX`, `instHasGoodTensor₂₃OfHasGoodTensorTensor₂₃X`, `instHasTensorOfHasTensorX`, `instHasTensorTensorUnit`, `instHasTensorTensorUnit_1`, `instHasTensorXTensorUnit`, `instHasTensorXTensorUnit_1`, `leftUnitor'_inv`, `leftUnitor'_inv_comm`, `leftUnitor'_inv_comm_assoc`, `rightUnitor'_inv`, `rightUnitor'_inv_comm`, `tensor_unit_d₂`, `unit_tensor_d₁`	14
Total	30

HomologicalComplex

Definitions

Name	Category	Theorems
`HasGoodTensor₁₂` 📖	MathDef	1 math math: `instHasGoodTensor₁₂OfHasGoodTensor₁₂TensorX`
`HasGoodTensor₂₃` 📖	MathDef	1 math math: `instHasGoodTensor₂₃OfHasGoodTensorTensor₂₃X`
`HasTensor` 📖	MathDef	3 math math: `instHasTensorTensorUnit`, `instHasTensorOfHasTensorX`, `instHasTensorTensorUnit_1`
`associator` 📖	CompOp	—
`leftUnitor` 📖	CompOp	—
`leftUnitor'` 📖	CompOp	3 math math: `leftUnitor'_inv_comm`, `leftUnitor'_inv_comm_assoc`, `leftUnitor'_inv`
`monoidalCategory` 📖	CompOp	—
`monoidalCategoryStruct` 📖	CompOp	—
`rightUnitor` 📖	CompOp	—
`rightUnitor'` 📖	CompOp	2 math math: `rightUnitor'_inv`, `rightUnitor'_inv_comm`
`tensorHom` 📖	CompOp	—
`tensorObj` 📖	CompOp	5 math math: `rightUnitor'_inv`, `leftUnitor'_inv_comm`, `leftUnitor'_inv_comm_assoc`, `leftUnitor'_inv`, `rightUnitor'_inv_comm`
`tensorUnit` 📖	CompOp	11 math math: `rightUnitor'_inv`, `instHasTensorTensorUnit`, `leftUnitor'_inv_comm`, `instHasTensorXTensorUnit_1`, `leftUnitor'_inv_comm_assoc`, `tensor_unit_d₂`, `leftUnitor'_inv`, `instHasTensorTensorUnit_1`, `unit_tensor_d₁`, `instHasTensorXTensorUnit`, `rightUnitor'_inv_comm`
`tensorUnitIso` 📖	CompOp	—
`ιTensorObj` 📖	CompOp	2 math math: `rightUnitor'_inv`, `leftUnitor'_inv`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instHasGoodTensor₁₂OfHasGoodTensor₁₂TensorX` 📖	mathematical	`CategoryTheory.GradedObject.HasGoodTensor₁₂Tensor` `X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms`	`HasGoodTensor₁₂`	—	—
`instHasGoodTensor₂₃OfHasGoodTensorTensor₂₃X` 📖	mathematical	`CategoryTheory.GradedObject.HasGoodTensorTensor₂₃` `X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms`	`HasGoodTensor₂₃`	—	—
`instHasTensorOfHasTensorX` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.MonoidalCategory.curriedTensor` `CategoryTheory.GradedObject.HasTensor` `X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms`	`HasTensor`	—	—
`instHasTensorTensorUnit` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.MonoidalCategory.curriedTensor` `CategoryTheory.Limits.PreservesColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.empty` `CategoryTheory.Functor.flip`	`HasTensor` `tensorUnit`	—	`instHasTensorXTensorUnit`
`instHasTensorTensorUnit_1` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.MonoidalCategory.curriedTensor` `CategoryTheory.Limits.PreservesColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.empty`	`HasTensor` `tensorUnit`	—	`instHasTensorXTensorUnit_1`
`instHasTensorXTensorUnit` 📖	mathematical	`CategoryTheory.Limits.PreservesColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.empty` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.Functor.flip` `CategoryTheory.MonoidalCategory.curriedTensor`	`CategoryTheory.GradedObject.HasTensor` `X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `tensorUnit`	—	`CategoryTheory.GradedObject.hasTensor_of_iso` `CategoryTheory.Limits.HasZeroObject.hasInitial` `CategoryTheory.GradedObject.Monoidal.instHasMapProdObjFunctorMapBifunctorCurriedTensorSingle₀TensorUnit`
`instHasTensorXTensorUnit_1` 📖	mathematical	`CategoryTheory.Limits.PreservesColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.empty` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.MonoidalCategory.curriedTensor`	`CategoryTheory.GradedObject.HasTensor` `X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `tensorUnit`	—	`CategoryTheory.GradedObject.hasTensor_of_iso` `CategoryTheory.Limits.HasZeroObject.hasInitial` `CategoryTheory.GradedObject.Monoidal.instHasMapProdObjFunctorMapBifunctorCurriedTensorSingle₀TensorUnit_1`
`leftUnitor'_inv` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.MonoidalCategory.curriedTensor` `CategoryTheory.Limits.PreservesColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.empty` `CategoryTheory.Functor.flip`	`CategoryTheory.Iso.inv` `CategoryTheory.pi` `X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `tensorObj` `tensorUnit` `instHasTensorTensorUnit` `leftUnitor'` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategoryStruct.leftUnitor` `HomologicalComplex` `instCategory` `single` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `CategoryTheory.MonoidalCategoryStruct.whiskerRight` `singleObjXSelf` `ιTensorObj` `zero_add`	—	`instHasTensorTensorUnit` `zero_add` `CategoryTheory.Limits.HasZeroObject.hasInitial` `instHasTensorXTensorUnit` `CategoryTheory.GradedObject.Monoidal.instHasTensorTensorUnit` `CategoryTheory.GradedObject.Monoidal.leftUnitor_inv_apply` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.cancel_iso_inv_left` `CategoryTheory.GradedObject.Monoidal.ι_tensorHom` `CategoryTheory.MonoidalCategory.tensorHom_id` `CategoryTheory.MonoidalCategory.comp_whiskerRight_assoc` `CategoryTheory.cancel_epi` `CategoryTheory.epi_of_strongEpi` `CategoryTheory.strongEpi_of_isIso` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.Iso.hom_inv_id_assoc`
`leftUnitor'_inv_comm` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.MonoidalCategory.curriedTensor` `CategoryTheory.Limits.PreservesColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.empty` `CategoryTheory.Functor.flip`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `tensorObj` `tensorUnit` `instHasTensorTensorUnit` `CategoryTheory.Iso.inv` `CategoryTheory.pi` `leftUnitor'` `d`	—	`instHasTensorTensorUnit` `zero_add` `leftUnitor'_inv` `CategoryTheory.Preadditive.comp_add` `CategoryTheory.Category.assoc` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `mapBifunctor.ι_D₁` `unit_tensor_d₁` `CategoryTheory.Limits.comp_zero` `mapBifunctor.ι_D₂` `mapBifunctor.d₂_eq` `ComplexShape.ε_zero` `one_smul` `CategoryTheory.MonoidalCategory.id_whiskerLeft` `CategoryTheory.Iso.inv_hom_id_assoc` `shape` `CategoryTheory.Limits.zero_comp`
`leftUnitor'_inv_comm_assoc` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.MonoidalCategory.curriedTensor` `CategoryTheory.Limits.PreservesColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.empty` `CategoryTheory.Functor.flip`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `tensorObj` `tensorUnit` `instHasTensorTensorUnit` `CategoryTheory.Iso.inv` `CategoryTheory.pi` `leftUnitor'` `d`	—	`instHasTensorTensorUnit` `CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `leftUnitor'_inv_comm`
`rightUnitor'_inv` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.MonoidalCategory.curriedTensor` `CategoryTheory.Limits.PreservesColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.empty`	`CategoryTheory.Iso.inv` `CategoryTheory.pi` `X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `tensorObj` `tensorUnit` `instHasTensorTensorUnit_1` `rightUnitor'` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategoryStruct.rightUnitor` `HomologicalComplex` `instCategory` `single` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `singleObjXSelf` `ιTensorObj` `add_zero`	—	`instHasTensorTensorUnit_1` `add_zero` `CategoryTheory.Limits.HasZeroObject.hasInitial` `instHasTensorXTensorUnit_1` `CategoryTheory.GradedObject.Monoidal.instHasTensorTensorUnit_1` `CategoryTheory.GradedObject.Monoidal.rightUnitor_inv_apply` `CategoryTheory.Category.assoc` `CategoryTheory.Iso.cancel_iso_inv_left` `CategoryTheory.GradedObject.Monoidal.ι_tensorHom` `CategoryTheory.MonoidalCategory.id_tensorHom` `CategoryTheory.MonoidalCategory.whiskerLeft_comp_assoc` `CategoryTheory.cancel_epi` `CategoryTheory.epi_of_strongEpi` `CategoryTheory.strongEpi_of_isIso` `CategoryTheory.Iso.isIso_hom` `CategoryTheory.Iso.hom_inv_id_assoc`
`rightUnitor'_inv_comm` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.MonoidalCategory.curriedTensor` `CategoryTheory.Limits.PreservesColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.empty`	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `X` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `tensorObj` `tensorUnit` `instHasTensorTensorUnit_1` `CategoryTheory.Iso.inv` `CategoryTheory.pi` `rightUnitor'` `d`	—	`instHasTensorTensorUnit_1` `add_zero` `rightUnitor'_inv` `CategoryTheory.Preadditive.comp_add` `CategoryTheory.Category.assoc` `mapBifunctor.ι_D₁` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `mapBifunctor.ι_D₂` `tensor_unit_d₂` `CategoryTheory.Limits.comp_zero` `mapBifunctor.d₁_eq` `one_smul` `CategoryTheory.MonoidalCategory.whisker_exchange_assoc` `CategoryTheory.MonoidalCategory.whiskerRight_id` `CategoryTheory.Iso.inv_hom_id_assoc` `shape` `CategoryTheory.Limits.zero_comp`
`tensor_unit_d₂` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.MonoidalCategory.curriedTensor` `CategoryTheory.Limits.PreservesColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.empty`	`mapBifunctor.d₂` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `tensorUnit` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `CategoryTheory.functorCategoryPreadditive` `ComplexShape.instTotalComplexShape` `instHasTensorTensorUnit_1` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `X` `mapBifunctor` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `instHasTensorTensorUnit_1` `mapBifunctor.d₂_eq` `single_obj_d` `CategoryTheory.Functor.map_zero` `CategoryTheory.Limits.zero_comp` `smul_zero` `mapBifunctor.d₂_eq_zero'` `mapBifunctor.d₂_eq_zero`
`unit_tensor_d₁` 📖	mathematical	`CategoryTheory.Functor.Additive` `CategoryTheory.Functor.obj` `CategoryTheory.Functor` `CategoryTheory.Functor.category` `CategoryTheory.MonoidalCategory.curriedTensor` `CategoryTheory.Limits.PreservesColimit` `CategoryTheory.Discrete` `CategoryTheory.discreteCategory` `CategoryTheory.Functor.empty` `CategoryTheory.Functor.flip`	`mapBifunctor.d₁` `CategoryTheory.Preadditive.preadditiveHasZeroMorphisms` `tensorUnit` `CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `CategoryTheory.functorCategoryPreadditive` `ComplexShape.instTotalComplexShape` `instHasTensorTensorUnit` `Quiver.Hom` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `X` `mapBifunctor` `CategoryTheory.Limits.HasZeroMorphisms.zero`	—	`CategoryTheory.Functor.preservesZeroMorphisms_of_additive` `instHasTensorTensorUnit` `mapBifunctor.d₁_eq` `single_obj_d` `CategoryTheory.Functor.map_zero` `CategoryTheory.Limits.zero_app` `CategoryTheory.Limits.zero_comp` `smul_zero` `mapBifunctor.d₁_eq_zero'` `mapBifunctor.d₁_eq_zero`

HomologicalComplex.Monoidal

Definitions

Name	Category	Theorems
`inducingFunctorData` 📖	CompOp	—

---

← Back to Index