Documentation Verification Report

Monoidal

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

Statistics

Metric	Count
Definitions `inducingFunctorData`, `instMonoidalCategory`, `instMonoidalCategoryStruct`	3
Theorems `inducingFunctorData_εIso`, `inducingFunctorData_μIso`, `associator_def`, `leftUnitor_def`, `rightUnitor_def`, `tensorHom_def`, `tensorObj_carrier`, `tensorObj_instCoalgebra`, `tensorObj_isAddCommGroup`, `tensorObj_isModule`, `tensorUnit_carrier`, `tensorUnit_instCoalgebra`, `tensorUnit_isAddCommGroup`, `tensorUnit_isModule`, `whiskerLeft_def`, `whiskerRight_def`	16
Total	19

CoalgCat

Definitions

Name	Category	Theorems
`instMonoidalCategory` 📖	CompOp	—
`instMonoidalCategoryStruct` 📖	CompOp	16 math math: `tensorObj_isAddCommGroup`, `tensorHom_def`, `associator_def`, `MonoidalCategory.inducingFunctorData_μIso`, `whiskerRight_def`, `MonoidalCategory.inducingFunctorData_εIso`, `tensorUnit_instCoalgebra`, `tensorUnit_carrier`, `tensorUnit_isAddCommGroup`, `whiskerLeft_def`, `rightUnitor_def`, `tensorObj_carrier`, `tensorObj_instCoalgebra`, `tensorObj_isModule`, `tensorUnit_isModule`, `leftUnitor_def`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`associator_def` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.associator` `CoalgCat` `category` `instMonoidalCategoryStruct` `CoalgEquiv.toCoalgIso` `TensorProduct` `CommRing.toCommSemiring` `ModuleCat.carrier` `CommRing.toRing` `toModuleCat` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `TensorProduct.addCommMonoid` `TensorProduct.leftModule` `CommSemiring.toSemiring` `TensorProduct.addCommGroup` `TensorProduct.instModule` `TensorProduct.instCoalgebra` `Algebra.id` `instCoalgebra` `Coalgebra.TensorProduct.assoc`	—	—
`leftUnitor_def` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.leftUnitor` `CoalgCat` `category` `instMonoidalCategoryStruct` `CoalgEquiv.toCoalgIso` `TensorProduct` `CommRing.toCommSemiring` `ModuleCat.carrier` `CommRing.toRing` `toModuleCat` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `Semiring.toModule` `ModuleCat.isModule` `TensorProduct.addCommGroup` `Ring.toAddCommGroup` `TensorProduct.instModule` `TensorProduct.instCoalgebra` `Algebra.id` `instCoalgebra` `CommSemiring.toCoalgebra` `Coalgebra.TensorProduct.lid`	—	—
`rightUnitor_def` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.rightUnitor` `CoalgCat` `category` `instMonoidalCategoryStruct` `CoalgEquiv.toCoalgIso` `TensorProduct` `CommRing.toCommSemiring` `ModuleCat.carrier` `CommRing.toRing` `toModuleCat` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `ModuleCat.isModule` `Semiring.toModule` `TensorProduct.addCommGroup` `TensorProduct.leftModule` `TensorProduct.instCoalgebra` `Algebra.id` `CommSemiring.toCoalgebra` `instCoalgebra` `Coalgebra.TensorProduct.rid`	—	—
`tensorHom_def` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.tensorHom` `CoalgCat` `category` `instMonoidalCategoryStruct` `ofHom` `TensorProduct` `CommRing.toCommSemiring` `ModuleCat.carrier` `CommRing.toRing` `toModuleCat` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `TensorProduct.addCommGroup` `TensorProduct.instModule` `TensorProduct.instCoalgebra` `Algebra.id` `instCoalgebra` `Coalgebra.TensorProduct.map` `Hom.toCoalgHom'`	—	—
`tensorObj_carrier` 📖	mathematical	—	`ModuleCat.carrier` `CommRing.toRing` `toModuleCat` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CoalgCat` `category` `instMonoidalCategoryStruct` `TensorProduct` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule`	—	—
`tensorObj_instCoalgebra` 📖	mathematical	—	`instCoalgebra` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CoalgCat` `category` `instMonoidalCategoryStruct` `Coalgebra` `TensorProduct` `CommRing.toCommSemiring` `ModuleCat.carrier` `CommRing.toRing` `toModuleCat` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `TensorProduct.addCommGroup` `TensorProduct.instModule` `TensorProduct.instCoalgebra` `Algebra.id`	—	—
`tensorObj_isAddCommGroup` 📖	mathematical	—	`ModuleCat.isAddCommGroup` `CommRing.toRing` `toModuleCat` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CoalgCat` `category` `instMonoidalCategoryStruct` `TensorProduct.addCommGroup` `CommRing.toCommSemiring` `ModuleCat.carrier` `AddCommGroup.toAddCommMonoid` `ModuleCat.isModule`	—	—
`tensorObj_isModule` 📖	mathematical	—	`ModuleCat.isModule` `CommRing.toRing` `toModuleCat` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CoalgCat` `category` `instMonoidalCategoryStruct` `TensorProduct.instModule` `CommRing.toCommSemiring` `ModuleCat.carrier` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup`	—	—
`tensorUnit_carrier` 📖	mathematical	—	`ModuleCat.carrier` `CommRing.toRing` `toModuleCat` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CoalgCat` `category` `instMonoidalCategoryStruct`	—	—
`tensorUnit_instCoalgebra` 📖	mathematical	—	`instCoalgebra` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CoalgCat` `category` `instMonoidalCategoryStruct` `Coalgebra` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `Ring.toAddCommGroup` `CommRing.toRing` `Semiring.toModule` `CommSemiring.toSemiring` `CommSemiring.toCoalgebra`	—	—
`tensorUnit_isAddCommGroup` 📖	mathematical	—	`ModuleCat.isAddCommGroup` `CommRing.toRing` `toModuleCat` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CoalgCat` `category` `instMonoidalCategoryStruct` `Ring.toAddCommGroup`	—	—
`tensorUnit_isModule` 📖	mathematical	—	`ModuleCat.isModule` `CommRing.toRing` `toModuleCat` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CoalgCat` `category` `instMonoidalCategoryStruct` `Semiring.toModule` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	—	—
`whiskerLeft_def` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.whiskerLeft` `CoalgCat` `category` `instMonoidalCategoryStruct` `ofHom` `TensorProduct` `CommRing.toCommSemiring` `ModuleCat.carrier` `CommRing.toRing` `toModuleCat` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `TensorProduct.addCommGroup` `TensorProduct.instModule` `TensorProduct.instCoalgebra` `Algebra.id` `instCoalgebra` `CoalgHom.lTensor` `Hom.toCoalgHom'`	—	—
`whiskerRight_def` 📖	mathematical	—	`CategoryTheory.MonoidalCategoryStruct.whiskerRight` `CoalgCat` `category` `instMonoidalCategoryStruct` `ofHom` `TensorProduct` `CommRing.toCommSemiring` `ModuleCat.carrier` `CommRing.toRing` `toModuleCat` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `TensorProduct.addCommGroup` `TensorProduct.instModule` `TensorProduct.instCoalgebra` `Algebra.id` `instCoalgebra` `CoalgHom.rTensor` `Hom.toCoalgHom'`	—	—

CoalgCat.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` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `ModuleCat.monoidalCategory` `CoalgCat` `CoalgCat.category` `CoalgCat.instMonoidalCategoryStruct` `CategoryTheory.forget₂` `CoalgHom` `ModuleCat.carrier` `CoalgCat.toModuleCat` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `Coalgebra.toCoalgebraStruct` `CoalgCat.instCoalgebra` `CoalgHom.funLike` `CoalgCat.concreteCategory` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `CoalgCat.hasForgetToModule` `inducingFunctorData` `CategoryTheory.Iso.refl` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct`	—	—
`inducingFunctorData_μIso` 📖	mathematical	—	`CategoryTheory.Monoidal.InducingFunctorData.μIso` `ModuleCat` `CommRing.toRing` `ModuleCat.moduleCategory` `ModuleCat.monoidalCategory` `CoalgCat` `CoalgCat.category` `CoalgCat.instMonoidalCategoryStruct` `CategoryTheory.forget₂` `CoalgHom` `ModuleCat.carrier` `CoalgCat.toModuleCat` `CommRing.toCommSemiring` `AddCommGroup.toAddCommMonoid` `ModuleCat.isAddCommGroup` `ModuleCat.isModule` `Coalgebra.toCoalgebraStruct` `CoalgCat.instCoalgebra` `CoalgHom.funLike` `CoalgCat.concreteCategory` `LinearMap` `Ring.toSemiring` `RingHom.id` `Semiring.toNonAssocSemiring` `LinearMap.instFunLike` `ModuleCat.instConcreteCategoryLinearMapIdCarrier` `CoalgCat.hasForgetToModule` `inducingFunctorData` `CategoryTheory.Iso.refl` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.Functor.obj`	—	—

---

← Back to Index