Documentation Verification Report

Monoidal

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

Statistics

Metric	Count
Definitions `inducingFunctorData`, `instMonoidalAlgCatForget₂BialgHomCarrierAlgHomCarrier`, `instMonoidalCategory`, `instMonoidalCategoryStruct`, `instMonoidalCoalgCatForget₂BialgHomCarrierCoalgHomCarrier`	5
Theorems `inducingFunctorData_εIso`, `inducingFunctorData_μIso`, `associator_def`, `leftUnitor_def`, `rightUnitor_def`, `tensorHom_def`, `tensorObj_def`, `tensorUnit_def`, `whiskerLeft_def`, `whiskerRight_def`	10
Total	15

BialgCat

Definitions

Name	Category	Theorems
`instMonoidalAlgCatForget₂BialgHomCarrierAlgHomCarrier` 📖	CompOp	—
`instMonoidalCategory` 📖	CompOp	2 math math: `HopfAlgCat.MonoidalCategory.inducingFunctorData_εIso`, `HopfAlgCat.MonoidalCategory.inducingFunctorData_μIso`
`instMonoidalCategoryStruct` 📖	CompOp	10 math math: `rightUnitor_def`, `associator_def`, `whiskerLeft_def`, `tensorUnit_def`, `tensorHom_def`, `whiskerRight_def`, `tensorObj_def`, `MonoidalCategory.inducingFunctorData_μIso`, `leftUnitor_def`, `MonoidalCategory.inducingFunctorData_εIso`
`instMonoidalCoalgCatForget₂BialgHomCarrierCoalgHomCarrier` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`associator_def` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.associator` `BialgCat` `category` `instMonoidalCategoryStruct` `BialgEquiv.toBialgIso` `TensorProduct` `CommRing.toCommSemiring` `carrier` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `instRing` `Algebra.toModule` `Bialgebra.toAlgebra` `instBialgebra` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `CommSemiring.toSemiring` `Algebra.TensorProduct.instRing` `Algebra.TensorProduct.instAlgebra` `Algebra.TensorProduct.instSemiring` `TensorProduct.instBialgebra` `Algebra.id` `Bialgebra.TensorProduct.assoc`	—	—
`leftUnitor_def` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.leftUnitor` `BialgCat` `category` `instMonoidalCategoryStruct` `BialgEquiv.toBialgIso` `TensorProduct` `CommRing.toCommSemiring` `carrier` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Ring.toSemiring` `instRing` `Semiring.toModule` `Algebra.toModule` `Bialgebra.toAlgebra` `instBialgebra` `Algebra.TensorProduct.instRing` `CommRing.toRing` `Algebra.id` `TensorProduct.instBialgebra` `CommSemiring.toBialgebra` `Bialgebra.TensorProduct.lid`	—	—
`rightUnitor_def` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.rightUnitor` `BialgCat` `category` `instMonoidalCategoryStruct` `BialgEquiv.toBialgIso` `TensorProduct` `CommRing.toCommSemiring` `carrier` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `instRing` `CommSemiring.toSemiring` `Algebra.toModule` `Bialgebra.toAlgebra` `instBialgebra` `Semiring.toModule` `Algebra.TensorProduct.instRing` `Algebra.id` `TensorProduct.instBialgebra` `CommSemiring.toBialgebra` `Bialgebra.TensorProduct.rid`	—	—
`tensorHom_def` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.tensorHom` `BialgCat` `category` `instMonoidalCategoryStruct` `ofHom` `TensorProduct` `CommRing.toCommSemiring` `carrier` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRing` `Algebra.toModule` `Ring.toSemiring` `Bialgebra.toAlgebra` `instBialgebra` `Algebra.TensorProduct.instRing` `TensorProduct.instBialgebra` `Algebra.id` `Bialgebra.TensorProduct.map` `Hom.toBialgHom'`	—	—
`tensorObj_def` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.tensorObj` `BialgCat` `category` `instMonoidalCategoryStruct` `of` `TensorProduct` `CommRing.toCommSemiring` `carrier` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRing` `Algebra.toModule` `Ring.toSemiring` `Bialgebra.toAlgebra` `instBialgebra` `Algebra.TensorProduct.instRing` `TensorProduct.instBialgebra` `Algebra.id`	—	—
`tensorUnit_def` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.tensorUnit` `BialgCat` `category` `instMonoidalCategoryStruct` `of` `CommRing.toRing` `CommSemiring.toBialgebra` `CommRing.toCommSemiring`	—	—
`whiskerLeft_def` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `BialgCat` `category` `instMonoidalCategoryStruct` `ofHom` `TensorProduct` `CommRing.toCommSemiring` `carrier` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRing` `Algebra.toModule` `Ring.toSemiring` `Bialgebra.toAlgebra` `instBialgebra` `Algebra.TensorProduct.instRing` `TensorProduct.instBialgebra` `Algebra.id` `BialgHom.lTensor` `Hom.toBialgHom'`	—	—
`whiskerRight_def` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.whiskerRight` `BialgCat` `category` `instMonoidalCategoryStruct` `ofHom` `TensorProduct` `CommRing.toCommSemiring` `carrier` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRing` `Algebra.toModule` `Ring.toSemiring` `Bialgebra.toAlgebra` `instBialgebra` `Algebra.TensorProduct.instRing` `TensorProduct.instBialgebra` `Algebra.id` `BialgHom.rTensor` `Hom.toBialgHom'`	—	—

BialgCat.MonoidalCategory

Definitions

Name	Category	Theorems
`inducingFunctorData` 📖	CompOp	2 math math: `inducingFunctorData_μIso`, `inducingFunctorData_εIso`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`inducingFunctorData_εIso` 📖	mathematical	—	`CategoryTheory.Monoidal.InducingFunctorData.εIso` `AlgCat` `AlgCat.instCategory` `AlgCat.instMonoidalCategory` `BialgCat` `BialgCat.category` `BialgCat.instMonoidalCategoryStruct` `CategoryTheory.forget₂` `BialgHom` `BialgCat.carrier` `CommRing.toCommSemiring` `Ring.toSemiring` `BialgCat.instRing` `Bialgebra.toAlgebra` `BialgCat.instBialgebra` `Coalgebra.toCoalgebraStruct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toCoalgebra` `BialgHom.funLike` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `BialgCat.concreteCategory` `AlgHom` `AlgCat.carrier` `AlgCat.isRing` `AlgCat.isAlgebra` `AlgHom.funLike` `AlgCat.instConcreteCategoryAlgHomCarrier` `BialgCat.hasForgetToAlgebra` `inducingFunctorData` `CategoryTheory.Iso.refl` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct`	—	—
`inducingFunctorData_μIso` 📖	mathematical	—	`CategoryTheory.Monoidal.InducingFunctorData.μIso` `AlgCat` `AlgCat.instCategory` `AlgCat.instMonoidalCategory` `BialgCat` `BialgCat.category` `BialgCat.instMonoidalCategoryStruct` `CategoryTheory.forget₂` `BialgHom` `BialgCat.carrier` `CommRing.toCommSemiring` `Ring.toSemiring` `BialgCat.instRing` `Bialgebra.toAlgebra` `BialgCat.instBialgebra` `Coalgebra.toCoalgebraStruct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toCoalgebra` `BialgHom.funLike` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `BialgCat.concreteCategory` `AlgHom` `AlgCat.carrier` `AlgCat.isRing` `AlgCat.isAlgebra` `AlgHom.funLike` `AlgCat.instConcreteCategoryAlgHomCarrier` `BialgCat.hasForgetToAlgebra` `inducingFunctorData` `CategoryTheory.Iso.refl` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Functor.obj`	—	—

---

← Back to Index