Documentation Verification Report

Monoidal

📁 Source: Mathlib/Algebra/Category/AlgCat/Monoidal.lean

Statistics

Metric	Count
Definitions `instMonoidalCategory`, `tensorHom`, `tensorObj`, `instMonoidalCategoryStruct`	4
Theorems `hom_hom_associator`, `hom_hom_leftUnitor`, `hom_hom_rightUnitor`, `hom_inv_associator`, `hom_inv_leftUnitor`, `hom_inv_rightUnitor`, `hom_tensorHom`, `hom_whiskerLeft`, `hom_whiskerRight`, `tensorObj_carrier`	10
Total	14

AlgCat

Definitions

Name	Category	Theorems
`instMonoidalCategory` 📖	CompOp	2 math math: `BialgCat.MonoidalCategory.inducingFunctorData_μIso`, `BialgCat.MonoidalCategory.inducingFunctorData_εIso`
`instMonoidalCategoryStruct` 📖	CompOp	9 math math: `hom_inv_associator`, `hom_inv_rightUnitor`, `hom_hom_associator`, `hom_hom_rightUnitor`, `hom_inv_leftUnitor`, `hom_hom_leftUnitor`, `hom_whiskerLeft`, `hom_tensorHom`, `hom_whiskerRight`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hom_hom_associator` 📖	mathematical	—	`Hom.hom` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `AlgCat` `instCategory` `instMonoidalCategoryStruct` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.associator` `AlgEquiv.toAlgHom` `TensorProduct` `CommRing.toCommSemiring` `carrier` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `isRing` `Algebra.toModule` `isAlgebra` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `CommSemiring.toSemiring` `IsScalarTower.to_smulCommClass'` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Module.toDistribMulAction` `IsScalarTower.to_smulCommClass` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.leftAlgebra` `TensorProduct.smulCommClass_left` `Algebra.TensorProduct.assoc`	—	—
`hom_hom_leftUnitor` 📖	mathematical	—	`Hom.hom` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `AlgCat` `instCategory` `instMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.leftUnitor` `AlgEquiv.toAlgHom` `TensorProduct` `CommRing.toCommSemiring` `carrier` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Ring.toSemiring` `isRing` `Semiring.toModule` `Algebra.toModule` `isAlgebra` `Algebra.TensorProduct.instSemiring` `Algebra.id` `Algebra.TensorProduct.instAlgebra` `Algebra.TensorProduct.lid`	—	—
`hom_hom_rightUnitor` 📖	mathematical	—	`Hom.hom` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `AlgCat` `instCategory` `instMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.rightUnitor` `AlgEquiv.toAlgHom` `TensorProduct` `carrier` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `isRing` `CommSemiring.toSemiring` `Algebra.toModule` `isAlgebra` `Semiring.toModule` `Algebra.TensorProduct.instSemiring` `Algebra.id` `Algebra.TensorProduct.leftAlgebra` `IsScalarTower.to_smulCommClass` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Module.toDistribMulAction` `Algebra.TensorProduct.rid`	—	—
`hom_inv_associator` 📖	mathematical	—	`Hom.hom` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `AlgCat` `instCategory` `instMonoidalCategoryStruct` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategoryStruct.associator` `AlgEquiv.toAlgHom` `TensorProduct` `CommRing.toCommSemiring` `carrier` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `isRing` `Algebra.toModule` `isAlgebra` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `CommSemiring.toSemiring` `IsScalarTower.to_smulCommClass` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Module.toDistribMulAction` `IsScalarTower.to_smulCommClass'` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.leftAlgebra` `TensorProduct.smulCommClass_left` `AlgEquiv.symm` `Algebra.TensorProduct.assoc`	—	—
`hom_inv_leftUnitor` 📖	mathematical	—	`Hom.hom` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `AlgCat` `instCategory` `instMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategoryStruct.leftUnitor` `AlgEquiv.toAlgHom` `carrier` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Ring.toSemiring` `isRing` `Semiring.toModule` `Algebra.toModule` `isAlgebra` `Algebra.TensorProduct.instSemiring` `Algebra.id` `Algebra.TensorProduct.instAlgebra` `AlgEquiv.symm` `Algebra.TensorProduct.lid`	—	—
`hom_inv_rightUnitor` 📖	mathematical	—	`Hom.hom` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `AlgCat` `instCategory` `instMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategoryStruct.rightUnitor` `AlgEquiv.toAlgHom` `carrier` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `isRing` `CommSemiring.toSemiring` `Algebra.toModule` `isAlgebra` `Semiring.toModule` `Algebra.TensorProduct.instSemiring` `Algebra.id` `Algebra.TensorProduct.leftAlgebra` `IsScalarTower.to_smulCommClass` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Module.toDistribMulAction` `AlgEquiv.symm` `Algebra.TensorProduct.rid`	—	—
`hom_tensorHom` 📖	mathematical	—	`Hom.hom` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `AlgCat` `instCategory` `instMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorHom` `Algebra.TensorProduct.map` `carrier` `CommRing.toCommSemiring` `Algebra.id` `Ring.toSemiring` `isRing` `isAlgebra` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Module.toDistribMulAction` `Algebra.toModule`	—	—
`hom_whiskerLeft` 📖	mathematical	—	`Hom.hom` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `AlgCat` `instCategory` `instMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `Algebra.TensorProduct.map` `carrier` `CommRing.toCommSemiring` `Algebra.id` `Ring.toSemiring` `isRing` `isAlgebra` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Module.toDistribMulAction` `Algebra.toModule` `AlgHom.id`	—	—
`hom_whiskerRight` 📖	mathematical	—	`Hom.hom` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `AlgCat` `instCategory` `instMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.whiskerRight` `Algebra.TensorProduct.map` `carrier` `CommRing.toCommSemiring` `Algebra.id` `Ring.toSemiring` `isRing` `isAlgebra` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Module.toDistribMulAction` `Algebra.toModule` `AlgHom.id`	—	—

AlgCat.instMonoidalCategory

Definitions

Name	Category	Theorems
`tensorHom` 📖	CompOp	—
`tensorObj` 📖	CompOp	1 math math: `tensorObj_carrier`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`tensorObj_carrier` 📖	mathematical	—	`AlgCat.carrier` `tensorObj` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `AlgCat.isRing` `Algebra.toModule` `Ring.toSemiring` `AlgCat.isAlgebra`	—	—

---

← Back to Index