Documentation Verification Report

Monoidal

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

Statistics

Metric	Count
Definitions `binaryCofan`, `binaryCofanIsColimit`, `instBraidedCategory`, `instCartesianMonoidalCategoryOpposite`, `instMonoidalCategory`, `isInitialSelf`	6
Theorems `associator_hom_hom`, `associator_inv_hom`, `binaryCofan_inl`, `binaryCofan_inr`, `binaryCofan_pt`, `braiding_hom_hom`, `braiding_inv_hom`, `coe_tensorObj`, `coe_tensorUnit`, `fst_unop_hom`, `lift_unop_hom`, `snd_unop_hom`, `tensorHom_hom`, `toUnit_unop_hom`, `whiskerLeft_hom`, `whiskerRight_hom`, `unop_inj_iff`	17
Total	23

CommAlgCat

Definitions

Name	Category	Theorems
`binaryCofan` 📖	CompOp	3 math math: `binaryCofan_pt`, `binaryCofan_inl`, `binaryCofan_inr`
`binaryCofanIsColimit` 📖	CompOp	—
`instBraidedCategory` 📖	CompOp	4 math math: `braiding_hom_hom`, `instIsCommMonObjOppositeCommAlgCatXUnopMonObjCommBialgCatFunctorCommBialgCatEquivComonCommAlgCatOfIsCocommCarrier`, `braiding_inv_hom`, `instIsCommMonObjOppositeCommAlgCatOpOfOfIsCocomm`
`instCartesianMonoidalCategoryOpposite` 📖	CompOp	4 math math: `lift_unop_hom`, `fst_unop_hom`, `snd_unop_hom`, `toUnit_unop_hom`
`instMonoidalCategory` 📖	CompOp	22 math math: `commBialgCatEquivComonCommAlgCat_unitIso_inv_app`, `braiding_hom_hom`, `commBialgCatEquivComonCommAlgCat_unitIso_hom_app`, `commBialgCatEquivComonCommAlgCat_functor_obj_unop_X`, `mul_op_of_unop_hom`, `instIsMonHomOppositeCommAlgCatOpOfHomToAlgHomBialgHom`, `tensorHom_hom`, `coe_tensorObj`, `coe_tensorUnit`, `whiskerLeft_hom`, `whiskerRight_hom`, `instIsCommMonObjOppositeCommAlgCatXUnopMonObjCommBialgCatFunctorCommBialgCatEquivComonCommAlgCatOfIsCocommCarrier`, `braiding_inv_hom`, `associator_inv_hom`, `one_op_of_unop_hom`, `commBialgCatEquivComonCommAlgCat_inverse_obj`, `associator_hom_hom`, `commBialgCatEquivComonCommAlgCat_inverse_map_unop_hom`, `instIsCommMonObjOppositeCommAlgCatOpOfOfIsCocomm`, `commBialgCatEquivComonCommAlgCat_counitIso_hom_app`, `commBialgCatEquivComonCommAlgCat_functor_map_unop_hom`, `commBialgCatEquivComonCommAlgCat_counitIso_inv_app`
`isInitialSelf` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`associator_hom_hom` 📖	mathematical	—	`Hom.hom` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CommAlgCat` `instCategory` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `instMonoidalCategory` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategoryStruct.associator` `AlgEquiv.toAlgHom` `TensorProduct` `CommRing.toCommSemiring` `carrier` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commRing` `Algebra.toModule` `algebra` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `IsScalarTower.to_smulCommClass'` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `IsScalarTower.to_smulCommClass` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.leftAlgebra` `TensorProduct.smulCommClass_left` `Algebra.TensorProduct.assoc`	—	—
`associator_inv_hom` 📖	mathematical	—	`Hom.hom` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CommAlgCat` `instCategory` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `instMonoidalCategory` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategoryStruct.associator` `AlgEquiv.toAlgHom` `TensorProduct` `CommRing.toCommSemiring` `carrier` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commRing` `Algebra.toModule` `algebra` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `IsScalarTower.to_smulCommClass` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `IsScalarTower.to_smulCommClass'` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.leftAlgebra` `TensorProduct.smulCommClass_left` `AlgEquiv.symm` `Algebra.TensorProduct.assoc`	—	—
`binaryCofan_inl` 📖	mathematical	—	`CategoryTheory.Limits.BinaryCofan.inl` `CommAlgCat` `instCategory` `binaryCofan` `ofHom` `carrier` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commRing` `Algebra.toModule` `algebra` `Algebra.TensorProduct.instCommRing` `Algebra.TensorProduct.instAlgebra` `Algebra.TensorProduct.includeLeft`	—	—
`binaryCofan_inr` 📖	mathematical	—	`CategoryTheory.Limits.BinaryCofan.inr` `CommAlgCat` `instCategory` `binaryCofan` `ofHom` `carrier` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commRing` `Algebra.toModule` `algebra` `Algebra.TensorProduct.instCommRing` `Algebra.TensorProduct.instAlgebra` `Algebra.TensorProduct.includeRight`	—	—
`binaryCofan_pt` 📖	mathematical	—	`CategoryTheory.Limits.Cocone.pt` `CategoryTheory.Discrete` `CategoryTheory.Limits.WalkingPair` `CategoryTheory.discreteCategory` `CommAlgCat` `instCategory` `CategoryTheory.Limits.pair` `binaryCofan` `of` `TensorProduct` `CommRing.toCommSemiring` `carrier` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `Algebra.toModule` `CommSemiring.toSemiring` `algebra` `Algebra.TensorProduct.instCommRing` `Algebra.TensorProduct.instAlgebra`	—	—
`braiding_hom_hom` 📖	mathematical	—	`Hom.hom` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CommAlgCat` `instCategory` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `instMonoidalCategory` `CategoryTheory.Iso.hom` `CategoryTheory.BraidedCategory.braiding` `instBraidedCategory` `AlgEquiv.toAlgHom` `TensorProduct` `CommRing.toCommSemiring` `carrier` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commRing` `Algebra.toModule` `algebra` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.instAlgebra` `Algebra.TensorProduct.comm`	—	—
`braiding_inv_hom` 📖	mathematical	—	`Hom.hom` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CommAlgCat` `instCategory` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `instMonoidalCategory` `CategoryTheory.Iso.inv` `CategoryTheory.BraidedCategory.braiding` `instBraidedCategory` `AlgEquiv.toAlgHom` `TensorProduct` `CommRing.toCommSemiring` `carrier` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `commRing` `Algebra.toModule` `algebra` `Algebra.TensorProduct.instSemiring` `Algebra.TensorProduct.instAlgebra` `Algebra.TensorProduct.comm`	—	—
`coe_tensorObj` 📖	mathematical	—	`carrier` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CommAlgCat` `instCategory` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `instMonoidalCategory` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `Algebra.toModule` `CommSemiring.toSemiring` `algebra`	—	—
`coe_tensorUnit` 📖	mathematical	—	`carrier` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CommAlgCat` `instCategory` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `instMonoidalCategory`	—	—
`fst_unop_hom` 📖	mathematical	—	`Hom.hom` `Opposite.unop` `CommAlgCat` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `Opposite` `CategoryTheory.Category.opposite` `instCategory` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `instCartesianMonoidalCategoryOpposite` `Quiver.Hom.unop` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.SemiCartesianMonoidalCategory.fst` `Algebra.TensorProduct.includeLeft` `carrier` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `commRing` `algebra`	—	—
`lift_unop_hom` 📖	mathematical	—	`Hom.hom` `Opposite.unop` `CommAlgCat` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `Opposite` `CategoryTheory.Category.opposite` `instCategory` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `instCartesianMonoidalCategoryOpposite` `Quiver.Hom.unop` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.CartesianMonoidalCategory.lift` `Algebra.TensorProduct.lift` `carrier` `CommRing.toCommSemiring` `Algebra.id` `CommSemiring.toSemiring` `commRing` `algebra` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Algebra.toModule` `Commute.all` `NonUnitalNonAssocCommSemiring.toCommMagma` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocCommSemiring` `DFunLike.coe` `AlgHom` `AlgHom.funLike`	—	—
`snd_unop_hom` 📖	mathematical	—	`Hom.hom` `Opposite.unop` `CommAlgCat` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `Opposite` `CategoryTheory.Category.opposite` `instCategory` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `instCartesianMonoidalCategoryOpposite` `Quiver.Hom.unop` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.SemiCartesianMonoidalCategory.snd` `Algebra.TensorProduct.includeRight` `carrier` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `commRing` `algebra`	—	—
`tensorHom_hom` 📖	mathematical	—	`Hom.hom` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CommAlgCat` `instCategory` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `instMonoidalCategory` `CategoryTheory.MonoidalCategoryStruct.tensorHom` `Algebra.TensorProduct.map` `carrier` `CommRing.toCommSemiring` `Algebra.id` `CommSemiring.toSemiring` `commRing` `algebra` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Algebra.toModule`	—	—
`toUnit_unop_hom` 📖	mathematical	—	`Hom.hom` `Opposite.unop` `CommAlgCat` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `Opposite` `CategoryTheory.Category.opposite` `instCategory` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toMonoidalCategory` `CategoryTheory.CartesianMonoidalCategory.toSemiCartesianMonoidalCategory` `instCartesianMonoidalCategoryOpposite` `Quiver.Hom.unop` `CategoryTheory.CategoryStruct.toQuiver` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.SemiCartesianMonoidalCategory.toUnit` `Algebra.ofId` `carrier` `CommRing.toCommSemiring` `CommSemiring.toSemiring` `commRing` `algebra`	—	—
`whiskerLeft_hom` 📖	mathematical	—	`Hom.hom` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CommAlgCat` `instCategory` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `instMonoidalCategory` `CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `Algebra.TensorProduct.map` `carrier` `CommRing.toCommSemiring` `Algebra.id` `CommSemiring.toSemiring` `commRing` `algebra` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Algebra.toModule` `AlgHom.id`	—	—
`whiskerRight_hom` 📖	mathematical	—	`Hom.hom` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CommAlgCat` `instCategory` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `instMonoidalCategory` `CategoryTheory.MonoidalCategoryStruct.whiskerRight` `Algebra.TensorProduct.map` `carrier` `CommRing.toCommSemiring` `Algebra.id` `CommSemiring.toSemiring` `commRing` `algebra` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DistribMulAction.toMulAction` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Algebra.toModule` `AlgHom.id`	—	—

Quiver.Hom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`unop_inj_iff` 📖	mathematical	—	`unop`	—	—

---

← Back to Index