Documentation Verification Report

MonoidalComp

📁 Source: Mathlib/Tactic/CategoryTheory/MonoidalComp.lean

Statistics

Metric	Count
Definitions `«term_≪⊗≫_»`, `«term_⊗≫_»`, `«term⊗𝟙»`, `MonoidalCoherence`, `assoc`, `assoc'`, `iso`, `left`, `left'`, `refl`, `right`, `right'`, `tensor_right`, `tensor_right'`, `whiskerLeft`, `whiskerRight`, `monoidalComp`, `monoidalIso`, `monoidalIsoComp`	19
Theorems `assoc'_iso`, `assoc_iso`, `left'_iso`, `left_iso`, `refl_iso`, `right'_iso`, `right_iso`, `tensor_right'_iso`, `tensor_right_iso`, `whiskerLeft_iso`, `whiskerRight_iso`, `monoidalComp_refl`	12
Total	31

CategoryTheory

Definitions

Name	Category	Theorems
`MonoidalCoherence` 📖	CompData	—
`monoidalComp` 📖	CompOp	5 math math: `BraidedCategory.yang_baxter'`, `ExactPairing.coevaluation_evaluation''`, `monoidalComp_refl`, `ExactPairing.evaluation_coevaluation''`, `Mathlib.Tactic.Monoidal.StructuralOfExpr_monoidalComp`
`monoidalIso` 📖	CompOp	—
`monoidalIsoComp` 📖	CompOp	1 math math: `Mathlib.Tactic.Monoidal.StructuralOfExpr_monoidalComp`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`monoidalComp_refl` 📖	mathematical	—	`monoidalComp` `MonoidalCoherence.refl` `CategoryStruct.comp` `Category.toCategoryStruct`	—	`Category.id_comp`

CategoryTheory.MonoidalCategory

Definitions

Name	Category	Theorems
`«term_≪⊗≫_»` 📖	CompOp	—
`«term_⊗≫_»` 📖	CompOp	—
`«term⊗𝟙»` 📖	CompOp	—

CategoryTheory.MonoidalCoherence

Definitions

Name	Category	Theorems
`assoc` 📖	CompOp	3 math math: `CategoryTheory.BraidedCategory.yang_baxter'`, `CategoryTheory.ExactPairing.evaluation_coevaluation''`, `assoc_iso`
`assoc'` 📖	CompOp	3 math math: `CategoryTheory.BraidedCategory.yang_baxter'`, `CategoryTheory.ExactPairing.coevaluation_evaluation''`, `assoc'_iso`
`iso` 📖	CompOp	13 math math: `CategoryTheory.ExactPairing.coevaluation_evaluation''`, `assoc'_iso`, `left_iso`, `tensor_right_iso`, `right'_iso`, `whiskerRight_iso`, `CategoryTheory.ExactPairing.evaluation_coevaluation''`, `whiskerLeft_iso`, `refl_iso`, `left'_iso`, `assoc_iso`, `right_iso`, `tensor_right'_iso`
`left` 📖	CompOp	2 math math: `left_iso`, `CategoryTheory.ExactPairing.evaluation_coevaluation''`
`left'` 📖	CompOp	2 math math: `CategoryTheory.ExactPairing.coevaluation_evaluation''`, `left'_iso`
`refl` 📖	CompOp	5 math math: `CategoryTheory.BraidedCategory.yang_baxter'`, `CategoryTheory.ExactPairing.coevaluation_evaluation''`, `CategoryTheory.monoidalComp_refl`, `CategoryTheory.ExactPairing.evaluation_coevaluation''`, `refl_iso`
`right` 📖	CompOp	2 math math: `CategoryTheory.ExactPairing.coevaluation_evaluation''`, `right_iso`
`right'` 📖	CompOp	2 math math: `right'_iso`, `CategoryTheory.ExactPairing.evaluation_coevaluation''`
`tensor_right` 📖	CompOp	1 math math: `tensor_right_iso`
`tensor_right'` 📖	CompOp	1 math math: `tensor_right'_iso`
`whiskerLeft` 📖	CompOp	1 math math: `whiskerLeft_iso`
`whiskerRight` 📖	CompOp	4 math math: `CategoryTheory.BraidedCategory.yang_baxter'`, `CategoryTheory.ExactPairing.coevaluation_evaluation''`, `whiskerRight_iso`, `CategoryTheory.ExactPairing.evaluation_coevaluation''`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`assoc'_iso` 📖	mathematical	—	`iso` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `assoc'` `CategoryTheory.Iso.trans` `CategoryTheory.Iso.symm` `CategoryTheory.MonoidalCategoryStruct.associator`	—	—
`assoc_iso` 📖	mathematical	—	`iso` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `assoc` `CategoryTheory.Iso.trans` `CategoryTheory.MonoidalCategoryStruct.associator`	—	—
`left'_iso` 📖	mathematical	—	`iso` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `left'` `CategoryTheory.Iso.trans` `CategoryTheory.Iso.symm` `CategoryTheory.MonoidalCategoryStruct.leftUnitor`	—	—
`left_iso` 📖	mathematical	—	`iso` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `left` `CategoryTheory.Iso.trans` `CategoryTheory.MonoidalCategoryStruct.leftUnitor`	—	—
`refl_iso` 📖	mathematical	—	`iso` `refl` `CategoryTheory.Iso.refl`	—	—
`right'_iso` 📖	mathematical	—	`iso` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `right'` `CategoryTheory.Iso.trans` `CategoryTheory.Iso.symm` `CategoryTheory.MonoidalCategoryStruct.rightUnitor`	—	—
`right_iso` 📖	mathematical	—	`iso` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `right` `CategoryTheory.Iso.trans` `CategoryTheory.MonoidalCategoryStruct.rightUnitor`	—	—
`tensor_right'_iso` 📖	mathematical	—	`iso` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `tensor_right'` `CategoryTheory.Iso.trans` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.whiskerLeftIso` `CategoryTheory.MonoidalCategoryStruct.rightUnitor`	—	—
`tensor_right_iso` 📖	mathematical	—	`iso` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `tensor_right` `CategoryTheory.Iso.trans` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.symm` `CategoryTheory.MonoidalCategoryStruct.rightUnitor` `CategoryTheory.MonoidalCategory.whiskerLeftIso`	—	—
`whiskerLeft_iso` 📖	mathematical	—	`iso` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `whiskerLeft` `CategoryTheory.MonoidalCategory.whiskerLeftIso`	—	—
`whiskerRight_iso` 📖	mathematical	—	`iso` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `whiskerRight` `CategoryTheory.MonoidalCategory.whiskerRightIso`	—	—

---

← Back to Index