Documentation Verification Report

LinearFunctor

📁 Source: Mathlib/CategoryTheory/Monoidal/Action/LinearFunctor.lean

Statistics

Metric	Count
Definitions `LaxLeftLinear`, `μₗ`, `LaxRightLinear`, `μᵣ`, `LeftLinear`, `toLaxLeftLinear`, `toOplaxLeftLinear`, `μₗIso`, `OplaxLeftLinear`, `δₗ`, `OplaxRightLinear`, `δᵣ`, `RightLinear`, `toLaxRightLinear`, `toOplaxRightLinear`, `μᵣIso`	16
Theorems `μₗ_associativity`, `μₗ_associativity_assoc`, `μₗ_associativity_inv`, `μₗ_associativity_inv_assoc`, `μₗ_naturality_left`, `μₗ_naturality_left_assoc`, `μₗ_naturality_right`, `μₗ_naturality_right_assoc`, `μₗ_unitality`, `μₗ_unitality_assoc`, `μₗ_unitality_inv`, `μₗ_unitality_inv_assoc`, `μᵣ_associativity`, `μᵣ_associativity_assoc`, `μᵣ_associativity_inv`, `μᵣ_associativity_inv_assoc`, `μᵣ_naturality_left`, `μᵣ_naturality_left_assoc`, `μᵣ_naturality_right`, `μᵣ_naturality_right_assoc`, `μᵣ_unitality`, `μᵣ_unitality_assoc`, `μᵣ_unitality_inv`, `μᵣ_unitality_inv_assoc`, `instIsIsoδₗ`, `instIsIsoμₗ`, `inv_δₗ`, `inv_μₗ`, `δₗ_comp_μₗ`, `δₗ_comp_μₗ_assoc`, `μₗ_comp_δₗ`, `μₗ_comp_δₗ_assoc`, `δₗ_associativity`, `δₗ_associativity_assoc`, `δₗ_associativity_inv`, `δₗ_associativity_inv_assoc`, `δₗ_naturality_left`, `δₗ_naturality_left_assoc`, `δₗ_naturality_right`, `δₗ_naturality_right_assoc`, `δₗ_unitality_hom`, `δₗ_unitality_hom_assoc`, `δₗ_unitality_inv`, `δₗ_unitality_inv_assoc`, `δᵣ_associativity`, `δᵣ_associativity_assoc`, `δᵣ_associativity_inv`, `δᵣ_associativity_inv_assoc`, `δᵣ_naturality_left`, `δᵣ_naturality_left_assoc`, `δᵣ_naturality_right`, `δᵣ_naturality_right_assoc`, `δᵣ_unitality_hom`, `δᵣ_unitality_hom_assoc`, `δᵣ_unitality_inv`, `δᵣ_unitality_inv_assoc`, `instIsIsoδᵣ`, `instIsIsoμᵣ`, `inv_δᵣ`, `inv_μᵣ`, `δᵣ_comp_μᵣ`, `δᵣ_comp_μᵣ_assoc`, `μᵣ_comp_δᵣ`, `μᵣ_comp_δᵣ_assoc`	64
Total	80

CategoryTheory.Functor

Definitions

Name	Category	Theorems
`LaxLeftLinear` 📖	CompData	—
`LaxRightLinear` 📖	CompData	—
`LeftLinear` 📖	CompData	—
`OplaxLeftLinear` 📖	CompData	—
`OplaxRightLinear` 📖	CompData	—
`RightLinear` 📖	CompData	—

CategoryTheory.Functor.LaxLeftLinear

Definitions

Name	Category	Theorems
`μₗ` 📖	CompOp	19 math math: `μₗ_naturality_right`, `CategoryTheory.Functor.LeftLinear.μₗ_comp_δₗ_assoc`, `μₗ_associativity_inv_assoc`, `CategoryTheory.Functor.LeftLinear.inv_μₗ`, `μₗ_naturality_right_assoc`, `CategoryTheory.Functor.LeftLinear.δₗ_comp_μₗ`, `μₗ_unitality_assoc`, `μₗ_associativity`, `μₗ_naturality_left`, `μₗ_associativity_inv`, `μₗ_unitality_inv`, `μₗ_unitality`, `μₗ_unitality_inv_assoc`, `μₗ_naturality_left_assoc`, `CategoryTheory.Functor.LeftLinear.inv_δₗ`, `CategoryTheory.Functor.LeftLinear.μₗ_comp_δₗ`, `CategoryTheory.Functor.LeftLinear.instIsIsoμₗ`, `μₗ_associativity_assoc`, `CategoryTheory.Functor.LeftLinear.δₗ_comp_μₗ_assoc`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`μₗ_associativity` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Functor.obj` `μₗ` `CategoryTheory.Functor.map` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight`	—	—
`μₗ_associativity_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Functor.obj` `μₗ` `CategoryTheory.Functor.map` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `μₗ_associativity`
`μₗ_associativity_inv` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight` `μₗ` `CategoryTheory.Functor.map` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Iso.inv_hom_id_assoc` `CategoryTheory.Iso.map_hom_inv_id` `CategoryTheory.Category.comp_id` `CategoryTheory.whisker_eq` `CategoryTheory.eq_whisker` `μₗ_associativity`
`μₗ_associativity_inv_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight` `μₗ` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Functor.map` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `μₗ_associativity_inv`
`μₗ_naturality_left` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft` `μₗ` `CategoryTheory.Functor.map`	—	—
`μₗ_naturality_left_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft` `μₗ` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `μₗ_naturality_left`
`μₗ_naturality_right` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight` `CategoryTheory.Functor.map` `μₗ`	—	—
`μₗ_naturality_right_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight` `CategoryTheory.Functor.map` `μₗ`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `μₗ_naturality_right`
`μₗ_unitality` 📖	mathematical	—	`CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `μₗ` `CategoryTheory.Functor.map`	—	—
`μₗ_unitality_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Functor.obj` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso` `μₗ` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `μₗ_unitality`
`μₗ_unitality_inv` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso` `μₗ` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Iso.map_hom_inv_id` `CategoryTheory.Category.comp_id` `CategoryTheory.Iso.inv_hom_id_assoc` `CategoryTheory.whisker_eq` `CategoryTheory.eq_whisker` `μₗ_unitality`
`μₗ_unitality_inv_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso` `μₗ` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `μₗ_unitality_inv`

CategoryTheory.Functor.LaxRightLinear

Definitions

Name	Category	Theorems
`μᵣ` 📖	CompOp	19 math math: `μᵣ_naturality_right_assoc`, `μᵣ_unitality_inv_assoc`, `μᵣ_associativity_inv_assoc`, `CategoryTheory.Functor.RightLinear.μᵣ_comp_δᵣ`, `μᵣ_associativity_inv`, `CategoryTheory.Functor.RightLinear.δᵣ_comp_μᵣ`, `CategoryTheory.Functor.RightLinear.inv_μᵣ`, `μᵣ_naturality_right`, `CategoryTheory.Functor.RightLinear.instIsIsoμᵣ`, `μᵣ_associativity_assoc`, `μᵣ_unitality`, `μᵣ_naturality_left_assoc`, `μᵣ_associativity`, `μᵣ_unitality_assoc`, `μᵣ_naturality_left`, `CategoryTheory.Functor.RightLinear.δᵣ_comp_μᵣ_assoc`, `CategoryTheory.Functor.RightLinear.inv_δᵣ`, `μᵣ_unitality_inv`, `CategoryTheory.Functor.RightLinear.μᵣ_comp_δᵣ_assoc`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`μᵣ_associativity` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `μᵣ` `CategoryTheory.Functor.map` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft`	—	—
`μᵣ_associativity_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `μᵣ` `CategoryTheory.Functor.map` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `μᵣ_associativity`
`μᵣ_associativity_inv` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft` `μᵣ` `CategoryTheory.Functor.map` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Iso.inv_hom_id_assoc` `CategoryTheory.Iso.map_hom_inv_id` `CategoryTheory.Category.comp_id` `CategoryTheory.whisker_eq` `CategoryTheory.eq_whisker` `μᵣ_associativity`
`μᵣ_associativity_inv_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft` `μᵣ` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Functor.map` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `μᵣ_associativity_inv`
`μᵣ_naturality_left` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft` `CategoryTheory.Functor.map` `μᵣ`	—	—
`μᵣ_naturality_left_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft` `CategoryTheory.Functor.map` `μᵣ`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `μᵣ_naturality_left`
`μᵣ_naturality_right` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight` `μᵣ` `CategoryTheory.Functor.map`	—	—
`μᵣ_naturality_right_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight` `μᵣ` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `μᵣ_naturality_right`
`μᵣ_unitality` 📖	mathematical	—	`CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `μᵣ` `CategoryTheory.Functor.map`	—	—
`μᵣ_unitality_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso` `μᵣ` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `μᵣ_unitality`
`μᵣ_unitality_inv` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso` `μᵣ` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Iso.map_hom_inv_id` `CategoryTheory.Category.comp_id` `CategoryTheory.Iso.inv_hom_id_assoc` `CategoryTheory.whisker_eq` `CategoryTheory.eq_whisker` `μᵣ_unitality`
`μᵣ_unitality_inv_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso` `μᵣ` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `μᵣ_unitality_inv`

CategoryTheory.Functor.LeftLinear

Definitions

Name	Category	Theorems
`toLaxLeftLinear` 📖	CompOp	7 math math: `μₗ_comp_δₗ_assoc`, `inv_μₗ`, `δₗ_comp_μₗ`, `inv_δₗ`, `μₗ_comp_δₗ`, `instIsIsoμₗ`, `δₗ_comp_μₗ_assoc`
`toOplaxLeftLinear` 📖	CompOp	7 math math: `instIsIsoδₗ`, `μₗ_comp_δₗ_assoc`, `inv_μₗ`, `δₗ_comp_μₗ`, `inv_δₗ`, `μₗ_comp_δₗ`, `δₗ_comp_μₗ_assoc`
`μₗIso` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsIsoδₗ` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.Functor.OplaxLeftLinear.δₗ` `toOplaxLeftLinear`	—	`CategoryTheory.Iso.isIso_inv`
`instIsIsoμₗ` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.LaxLeftLinear.μₗ` `toLaxLeftLinear`	—	`CategoryTheory.Iso.isIso_hom`
`inv_δₗ` 📖	mathematical	—	`CategoryTheory.inv` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.Functor.OplaxLeftLinear.δₗ` `toOplaxLeftLinear` `instIsIsoδₗ` `CategoryTheory.Functor.LaxLeftLinear.μₗ` `toLaxLeftLinear`	—	`instIsIsoδₗ` `CategoryTheory.IsIso.eq_inv_of_hom_inv_id` `δₗ_comp_μₗ`
`inv_μₗ` 📖	mathematical	—	`CategoryTheory.inv` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.LaxLeftLinear.μₗ` `toLaxLeftLinear` `instIsIsoμₗ` `CategoryTheory.Functor.OplaxLeftLinear.δₗ` `toOplaxLeftLinear`	—	`instIsIsoμₗ` `CategoryTheory.IsIso.eq_inv_of_hom_inv_id` `μₗ_comp_δₗ`
`δₗ_comp_μₗ` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.Functor.OplaxLeftLinear.δₗ` `toOplaxLeftLinear` `CategoryTheory.Functor.LaxLeftLinear.μₗ` `toLaxLeftLinear` `CategoryTheory.CategoryStruct.id`	—	—
`δₗ_comp_μₗ_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.Functor.OplaxLeftLinear.δₗ` `toOplaxLeftLinear` `CategoryTheory.Functor.LaxLeftLinear.μₗ` `toLaxLeftLinear`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `δₗ_comp_μₗ`
`μₗ_comp_δₗ` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.LaxLeftLinear.μₗ` `toLaxLeftLinear` `CategoryTheory.Functor.OplaxLeftLinear.δₗ` `toOplaxLeftLinear` `CategoryTheory.CategoryStruct.id`	—	—
`μₗ_comp_δₗ_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.LaxLeftLinear.μₗ` `toLaxLeftLinear` `CategoryTheory.Functor.OplaxLeftLinear.δₗ` `toOplaxLeftLinear`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `μₗ_comp_δₗ`

CategoryTheory.Functor.OplaxLeftLinear

Definitions

Name	Category	Theorems
`δₗ` 📖	CompOp	19 math math: `CategoryTheory.Functor.LeftLinear.instIsIsoδₗ`, `δₗ_associativity_inv`, `CategoryTheory.Functor.LeftLinear.μₗ_comp_δₗ_assoc`, `CategoryTheory.Functor.LeftLinear.inv_μₗ`, `δₗ_naturality_left_assoc`, `δₗ_unitality_hom_assoc`, `δₗ_unitality_inv`, `δₗ_associativity`, `CategoryTheory.Functor.LeftLinear.δₗ_comp_μₗ`, `δₗ_unitality_hom`, `δₗ_naturality_right`, `δₗ_associativity_assoc`, `δₗ_unitality_inv_assoc`, `δₗ_naturality_left`, `δₗ_naturality_right_assoc`, `CategoryTheory.Functor.LeftLinear.inv_δₗ`, `CategoryTheory.Functor.LeftLinear.μₗ_comp_δₗ`, `CategoryTheory.Functor.LeftLinear.δₗ_comp_μₗ_assoc`, `δₗ_associativity_inv_assoc`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`δₗ_associativity` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `δₗ` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso` `CategoryTheory.Functor.map` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight`	—	—
`δₗ_associativity_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `δₗ` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso` `CategoryTheory.Functor.map` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `δₗ_associativity`
`δₗ_associativity_inv` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `δₗ` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Iso.map_inv_hom_id_assoc` `CategoryTheory.Iso.hom_inv_id` `CategoryTheory.Category.comp_id` `CategoryTheory.whisker_eq` `CategoryTheory.eq_whisker` `δₗ_associativity`
`δₗ_associativity_inv_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `δₗ` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `δₗ_associativity_inv`
`δₗ_naturality_left` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.Functor.map` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft` `δₗ`	—	—
`δₗ_naturality_left_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.Functor.map` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft` `δₗ`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `δₗ_naturality_left`
`δₗ_naturality_right` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.Functor.map` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight` `δₗ`	—	—
`δₗ_naturality_right_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.Functor.map` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight` `δₗ`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `δₗ_naturality_right`
`δₗ_unitality_hom` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `δₗ` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Iso.map_hom_inv_id_assoc` `CategoryTheory.Iso.inv_hom_id` `CategoryTheory.Category.comp_id` `CategoryTheory.whisker_eq` `CategoryTheory.eq_whisker` `δₗ_unitality_inv`
`δₗ_unitality_hom_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `δₗ` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `δₗ_unitality_hom`
`δₗ_unitality_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.map` `δₗ`	—	—
`δₗ_unitality_inv_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalLeftAction.toMonoidalLeftActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso` `CategoryTheory.Functor.map` `δₗ`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `δₗ_unitality_inv`

CategoryTheory.Functor.OplaxRightLinear

Definitions

Name	Category	Theorems
`δᵣ` 📖	CompOp	19 math math: `δᵣ_unitality_inv`, `δᵣ_naturality_right_assoc`, `δᵣ_associativity_inv`, `δᵣ_unitality_hom_assoc`, `δᵣ_naturality_left`, `CategoryTheory.Functor.RightLinear.μᵣ_comp_δᵣ`, `δᵣ_associativity`, `CategoryTheory.Functor.RightLinear.δᵣ_comp_μᵣ`, `CategoryTheory.Functor.RightLinear.inv_μᵣ`, `δᵣ_unitality_hom`, `CategoryTheory.Functor.RightLinear.instIsIsoδᵣ`, `δᵣ_associativity_inv_assoc`, `δᵣ_naturality_left_assoc`, `δᵣ_associativity_assoc`, `δᵣ_unitality_inv_assoc`, `CategoryTheory.Functor.RightLinear.δᵣ_comp_μᵣ_assoc`, `δᵣ_naturality_right`, `CategoryTheory.Functor.RightLinear.inv_δᵣ`, `CategoryTheory.Functor.RightLinear.μᵣ_comp_δᵣ_assoc`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`δᵣ_associativity` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `δᵣ` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso` `CategoryTheory.Functor.map` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft`	—	—
`δᵣ_associativity_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `δᵣ` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso` `CategoryTheory.Functor.map` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `δᵣ_associativity`
`δᵣ_associativity_inv` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `δᵣ` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Iso.map_inv_hom_id_assoc` `CategoryTheory.Iso.hom_inv_id` `CategoryTheory.Category.comp_id` `CategoryTheory.whisker_eq` `CategoryTheory.eq_whisker` `δᵣ_associativity`
`δᵣ_associativity_inv_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct` `δᵣ` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft` `CategoryTheory.MonoidalCategoryStruct.tensorObj` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `δᵣ_associativity_inv`
`δᵣ_naturality_left` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct` `CategoryTheory.Functor.map` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft` `δᵣ`	—	—
`δᵣ_naturality_left_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct` `CategoryTheory.Functor.map` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft` `δᵣ`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `δᵣ_naturality_left`
`δᵣ_naturality_right` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct` `CategoryTheory.Functor.map` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight` `δᵣ`	—	—
`δᵣ_naturality_right_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct` `CategoryTheory.Functor.map` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight` `δᵣ`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `δᵣ_naturality_right`
`δᵣ_unitality_hom` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `δᵣ` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Iso.map_hom_inv_id_assoc` `CategoryTheory.Iso.inv_hom_id` `CategoryTheory.Category.comp_id` `CategoryTheory.whisker_eq` `CategoryTheory.eq_whisker` `δᵣ_unitality_inv`
`δᵣ_unitality_hom_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `δᵣ` `CategoryTheory.Iso.hom` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso` `CategoryTheory.Functor.map`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `δᵣ_unitality_hom`
`δᵣ_unitality_inv` 📖	mathematical	—	`CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso` `CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.map` `δᵣ`	—	—
`δᵣ_unitality_inv_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct` `CategoryTheory.MonoidalCategoryStruct.tensorUnit` `CategoryTheory.Iso.inv` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionUnitIso` `CategoryTheory.Functor.map` `δᵣ`	—	`CategoryTheory.Category.assoc` `Mathlib.Tactic.Reassoc.eq_whisker'` `δᵣ_unitality_inv`

CategoryTheory.Functor.RightLinear

Definitions

Name	Category	Theorems
`toLaxRightLinear` 📖	CompOp	7 math math: `μᵣ_comp_δᵣ`, `δᵣ_comp_μᵣ`, `inv_μᵣ`, `instIsIsoμᵣ`, `δᵣ_comp_μᵣ_assoc`, `inv_δᵣ`, `μᵣ_comp_δᵣ_assoc`
`toOplaxRightLinear` 📖	CompOp	7 math math: `μᵣ_comp_δᵣ`, `δᵣ_comp_μᵣ`, `inv_μᵣ`, `instIsIsoδᵣ`, `δᵣ_comp_μᵣ_assoc`, `inv_δᵣ`, `μᵣ_comp_δᵣ_assoc`
`μᵣIso` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsIsoδᵣ` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct` `CategoryTheory.Functor.OplaxRightLinear.δᵣ` `toOplaxRightLinear`	—	`CategoryTheory.Iso.isIso_inv`
`instIsIsoμᵣ` 📖	mathematical	—	`CategoryTheory.IsIso` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.LaxRightLinear.μᵣ` `toLaxRightLinear`	—	`CategoryTheory.Iso.isIso_hom`
`inv_δᵣ` 📖	mathematical	—	`CategoryTheory.inv` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct` `CategoryTheory.Functor.OplaxRightLinear.δᵣ` `toOplaxRightLinear` `instIsIsoδᵣ` `CategoryTheory.Functor.LaxRightLinear.μᵣ` `toLaxRightLinear`	—	`instIsIsoδᵣ` `CategoryTheory.IsIso.eq_inv_of_hom_inv_id` `δᵣ_comp_μᵣ`
`inv_μᵣ` 📖	mathematical	—	`CategoryTheory.inv` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.LaxRightLinear.μᵣ` `toLaxRightLinear` `instIsIsoμᵣ` `CategoryTheory.Functor.OplaxRightLinear.δᵣ` `toOplaxRightLinear`	—	`instIsIsoμᵣ` `CategoryTheory.IsIso.eq_inv_of_hom_inv_id` `μᵣ_comp_δᵣ`
`δᵣ_comp_μᵣ` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct` `CategoryTheory.Functor.OplaxRightLinear.δᵣ` `toOplaxRightLinear` `CategoryTheory.Functor.LaxRightLinear.μᵣ` `toLaxRightLinear` `CategoryTheory.CategoryStruct.id`	—	—
`δᵣ_comp_μᵣ_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.Functor.obj` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct` `CategoryTheory.Functor.OplaxRightLinear.δᵣ` `toOplaxRightLinear` `CategoryTheory.Functor.LaxRightLinear.μᵣ` `toLaxRightLinear`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `δᵣ_comp_μᵣ`
`μᵣ_comp_δᵣ` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.LaxRightLinear.μᵣ` `toLaxRightLinear` `CategoryTheory.Functor.OplaxRightLinear.δᵣ` `toOplaxRightLinear` `CategoryTheory.CategoryStruct.id`	—	—
`μᵣ_comp_δᵣ_assoc` 📖	mathematical	—	`CategoryTheory.CategoryStruct.comp` `CategoryTheory.Category.toCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj` `CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct` `CategoryTheory.MonoidalCategory.MonoidalRightAction.toMonoidalRightActionStruct` `CategoryTheory.Functor.obj` `CategoryTheory.Functor.LaxRightLinear.μᵣ` `toLaxRightLinear` `CategoryTheory.Functor.OplaxRightLinear.δᵣ` `toOplaxRightLinear`	—	`CategoryTheory.Category.assoc` `CategoryTheory.Category.id_comp` `Mathlib.Tactic.Reassoc.eq_whisker'` `μᵣ_comp_δᵣ`

---

← Back to Index