Documentation Verification Report

Monoidal

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

Statistics

Metric	Count
Definitions `inducingFunctorData`, `instMonoidalBialgCatForget₂BialgHomCarrierCarrier`, `instMonoidalCategory`, `instMonoidalCategoryStruct`	4
Theorems `inducingFunctorData_εIso`, `inducingFunctorData_μIso`, `associator_def`, `leftUnitor_def`, `rightUnitor_def`, `tensorHom_def`, `tensorObj_carrier`, `tensorObj_instHopfAlgebra`, `tensorObj_instRing`, `tensorUnit_carrier`, `tensorUnit_instHopfAlgebra`, `tensorUnit_instRing`, `whiskerLeft_def`, `whiskerRight_def`	14
Total	18

HopfAlgCat

Definitions

Name	Category	Theorems
`instMonoidalBialgCatForget₂BialgHomCarrierCarrier` 📖	CompOp	—
`instMonoidalCategory` 📖	CompOp	—
`instMonoidalCategoryStruct` 📖	CompOp	14 math math: `rightUnitor_def`, `tensorObj_instRing`, `whiskerLeft_def`, `tensorObj_instHopfAlgebra`, `MonoidalCategory.inducingFunctorData_εIso`, `whiskerRight_def`, `MonoidalCategory.inducingFunctorData_μIso`, `associator_def`, `tensorHom_def`, `tensorObj_carrier`, `leftUnitor_def`, `tensorUnit_instRing`, `tensorUnit_instHopfAlgebra`, `tensorUnit_carrier`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`associator_def` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.associator` `HopfAlgCat` `category` `instMonoidalCategoryStruct` `BialgEquiv.toHopfAlgIso` `TensorProduct` `CommRing.toCommSemiring` `carrier` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `instRing` `Algebra.toModule` `Bialgebra.toAlgebra` `HopfAlgebraStruct.toBialgebra` `HopfAlgebra.toHopfAlgebraStruct` `instHopfAlgebra` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `CommSemiring.toSemiring` `Algebra.TensorProduct.instRing` `Algebra.TensorProduct.instAlgebra` `Algebra.TensorProduct.instSemiring` `TensorProduct.instHopfAlgebra` `Algebra.id` `Bialgebra.TensorProduct.assoc`	—	—
`leftUnitor_def` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.leftUnitor` `HopfAlgCat` `category` `instMonoidalCategoryStruct` `BialgEquiv.toHopfAlgIso` `TensorProduct` `CommRing.toCommSemiring` `carrier` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Ring.toSemiring` `instRing` `Semiring.toModule` `Algebra.toModule` `Bialgebra.toAlgebra` `HopfAlgebraStruct.toBialgebra` `HopfAlgebra.toHopfAlgebraStruct` `instHopfAlgebra` `Algebra.TensorProduct.instRing` `CommRing.toRing` `Algebra.id` `TensorProduct.instHopfAlgebra` `CommSemiring.toHopfAlgebra` `Bialgebra.TensorProduct.lid`	—	—
`rightUnitor_def` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.rightUnitor` `HopfAlgCat` `category` `instMonoidalCategoryStruct` `BialgEquiv.toHopfAlgIso` `TensorProduct` `CommRing.toCommSemiring` `carrier` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `instRing` `CommSemiring.toSemiring` `Algebra.toModule` `Bialgebra.toAlgebra` `HopfAlgebraStruct.toBialgebra` `HopfAlgebra.toHopfAlgebraStruct` `instHopfAlgebra` `Semiring.toModule` `Algebra.TensorProduct.instRing` `Algebra.id` `TensorProduct.instHopfAlgebra` `CommSemiring.toHopfAlgebra` `Bialgebra.TensorProduct.rid`	—	—
`tensorHom_def` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.tensorHom` `HopfAlgCat` `category` `instMonoidalCategoryStruct` `ofHom` `TensorProduct` `CommRing.toCommSemiring` `carrier` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRing` `Algebra.toModule` `Ring.toSemiring` `Bialgebra.toAlgebra` `HopfAlgebraStruct.toBialgebra` `HopfAlgebra.toHopfAlgebraStruct` `instHopfAlgebra` `Algebra.TensorProduct.instRing` `TensorProduct.instHopfAlgebra` `Algebra.id` `Bialgebra.TensorProduct.map` `Hom.toBialgHom'`	—	—
`tensorObj_carrier` 📖	mathematical	—	`carrier` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `HopfAlgCat` `category` `instMonoidalCategoryStruct` `TensorProduct` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRing` `Algebra.toModule` `Ring.toSemiring` `Bialgebra.toAlgebra` `HopfAlgebraStruct.toBialgebra` `HopfAlgebra.toHopfAlgebraStruct` `instHopfAlgebra`	—	—
`tensorObj_instHopfAlgebra` 📖	mathematical	—	`instHopfAlgebra` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `HopfAlgCat` `category` `instMonoidalCategoryStruct` `TensorProduct.instHopfAlgebra` `carrier` `CommRing.toCommSemiring` `Ring.toSemiring` `instRing` `Algebra.id` `Bialgebra.toAlgebra` `HopfAlgebraStruct.toBialgebra` `HopfAlgebra.toHopfAlgebraStruct`	—	—
`tensorObj_instRing` 📖	mathematical	—	`instRing` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `HopfAlgCat` `category` `instMonoidalCategoryStruct` `Algebra.TensorProduct.instRing` `carrier` `CommRing.toCommSemiring` `Bialgebra.toAlgebra` `Ring.toSemiring` `HopfAlgebraStruct.toBialgebra` `HopfAlgebra.toHopfAlgebraStruct` `instHopfAlgebra`	—	—
`tensorUnit_carrier` 📖	mathematical	—	`carrier` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `HopfAlgCat` `category` `instMonoidalCategoryStruct`	—	—
`tensorUnit_instHopfAlgebra` 📖	mathematical	—	`instHopfAlgebra` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `HopfAlgCat` `category` `instMonoidalCategoryStruct` `CommSemiring.toHopfAlgebra` `CommRing.toCommSemiring`	—	—
`tensorUnit_instRing` 📖	mathematical	—	`instRing` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `HopfAlgCat` `category` `instMonoidalCategoryStruct` `CommRing.toRing`	—	—
`whiskerLeft_def` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `HopfAlgCat` `category` `instMonoidalCategoryStruct` `ofHom` `TensorProduct` `CommRing.toCommSemiring` `carrier` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRing` `Algebra.toModule` `Ring.toSemiring` `Bialgebra.toAlgebra` `HopfAlgebraStruct.toBialgebra` `HopfAlgebra.toHopfAlgebraStruct` `instHopfAlgebra` `Algebra.TensorProduct.instRing` `TensorProduct.instHopfAlgebra` `Algebra.id` `BialgHom.lTensor` `Hom.toBialgHom'`	—	—
`whiskerRight_def` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.whiskerRight` `HopfAlgCat` `category` `instMonoidalCategoryStruct` `ofHom` `TensorProduct` `CommRing.toCommSemiring` `carrier` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `instRing` `Algebra.toModule` `Ring.toSemiring` `Bialgebra.toAlgebra` `HopfAlgebraStruct.toBialgebra` `HopfAlgebra.toHopfAlgebraStruct` `instHopfAlgebra` `Algebra.TensorProduct.instRing` `TensorProduct.instHopfAlgebra` `Algebra.id` `BialgHom.rTensor` `Hom.toBialgHom'`	—	—

HopfAlgCat.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` `BialgCat` `BialgCat.category` `BialgCat.instMonoidalCategory` `HopfAlgCat` `HopfAlgCat.category` `HopfAlgCat.instMonoidalCategoryStruct` `CategoryTheory.forget₂` `BialgHom` `HopfAlgCat.carrier` `CommRing.toCommSemiring` `Ring.toSemiring` `HopfAlgCat.instRing` `Bialgebra.toAlgebra` `HopfAlgebraStruct.toBialgebra` `HopfAlgebra.toHopfAlgebraStruct` `HopfAlgCat.instHopfAlgebra` `Coalgebra.toCoalgebraStruct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toCoalgebra` `BialgHom.funLike` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `HopfAlgCat.concreteCategory` `BialgCat.carrier` `BialgCat.instRing` `BialgCat.instBialgebra` `BialgCat.concreteCategory` `HopfAlgCat.hasForgetToBialgebra` `inducingFunctorData` `CategoryTheory.Iso.refl` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct`	—	—
`inducingFunctorData_μIso` 📖	mathematical	—	`CategoryTheory.Monoidal.InducingFunctorData.μIso` `BialgCat` `BialgCat.category` `BialgCat.instMonoidalCategory` `HopfAlgCat` `HopfAlgCat.category` `HopfAlgCat.instMonoidalCategoryStruct` `CategoryTheory.forget₂` `BialgHom` `HopfAlgCat.carrier` `CommRing.toCommSemiring` `Ring.toSemiring` `HopfAlgCat.instRing` `Bialgebra.toAlgebra` `HopfAlgebraStruct.toBialgebra` `HopfAlgebra.toHopfAlgebraStruct` `HopfAlgCat.instHopfAlgebra` `Coalgebra.toCoalgebraStruct` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Algebra.toModule` `Bialgebra.toCoalgebra` `BialgHom.funLike` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `HopfAlgCat.concreteCategory` `BialgCat.carrier` `BialgCat.instRing` `BialgCat.instBialgebra` `BialgCat.concreteCategory` `HopfAlgCat.hasForgetToBialgebra` `inducingFunctorData` `CategoryTheory.Iso.refl` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Functor.obj`	—	—

---

← Back to Index