Bimod

📁 Source: Mathlib/CategoryTheory/Monoidal/Bimod.lean

Statistics

Metric	Count
Definitions Bimod, hom, homAux, inv, invAux, hom, hom, inv, hom, inv, X, actLeft, actRight, X, actLeft, actRight, associatorBimod, comp, forget, homInhabited, id', instCategory, instInhabited, isoOfIso, leftUnitorBimod, monBicategory, regular, rightUnitorBimod, tensorBimod, whiskerLeft, whiskerRight	31
Theorems hom_inv_id, hom_left_act_hom', hom_right_act_hom', inv_hom_id, ext, ext_iff, left_act_hom, left_act_hom_assoc, right_act_hom, right_act_hom_assoc, hom_inv_id, hom_left_act_hom', hom_right_act_hom', inv_hom_id, hom_inv_id, hom_left_act_hom', hom_right_act_hom', inv_hom_id, actRight_one', left_assoc', middle_assoc', one_act_left', right_assoc', whiskerLeft_π_actLeft, π_tensor_id_actRight, actRight_one, actRight_one_assoc, comp_hom, comp_hom', comp_whiskerLeft_bimod, comp_whiskerRight_bimod, hom_ext, hom_ext_iff, id'_hom, id_hom', id_whiskerLeft_bimod, id_whiskerRight_bimod, isoOfIso_hom_hom, isoOfIso_inv_hom, left_assoc, left_assoc_assoc, middle_assoc, middle_assoc_assoc, one_actLeft, one_actLeft_assoc, pentagon_bimod, regular_X, regular_actLeft, regular_actRight, right_assoc, right_assoc_assoc, tensorBimod_X, tensorBimod_actLeft, tensorBimod_actRight, triangle_bimod, whiskerLeft_comp_bimod, whiskerLeft_hom, whiskerLeft_id_bimod, whiskerRight_comp_bimod, whiskerRight_hom, whiskerRight_id_bimod, whisker_assoc_bimod, whisker_exchange_bimod, id_tensor_π_preserves_coequalizer_inv_colimMap_desc, id_tensor_π_preserves_coequalizer_inv_desc, π_tensor_id_preserves_coequalizer_inv_colimMap_desc, π_tensor_id_preserves_coequalizer_inv_desc	67
Total	98

Bimod

Definitions

Name	Category	Theorems
X 📖	CompOp	36 math math: TensorBimod.π_tensor_id_actRight, AssociatorBimod.hom_left_act_hom', RightUnitorBimod.hom_right_act_hom', RightUnitorBimod.inv_hom_id, LeftUnitorBimod.hom_right_act_hom', whiskerLeft_hom, TensorBimod.whiskerLeft_π_actLeft, actRight_one, left_assoc_assoc, right_assoc, LeftUnitorBimod.inv_hom_id, right_assoc_assoc, Hom.left_act_hom, comp_hom, middle_assoc_assoc, one_actLeft_assoc, comp_hom', AssociatorBimod.hom_inv_id, regular_X, id'_hom, one_actLeft, left_assoc, Hom.left_act_hom_assoc, RightUnitorBimod.hom_left_act_hom', actRight_one_assoc, middle_assoc, AssociatorBimod.inv_hom_id, id_hom', tensorBimod_X, whiskerRight_hom, Hom.right_act_hom, Hom.right_act_hom_assoc, RightUnitorBimod.hom_inv_id, AssociatorBimod.hom_right_act_hom', LeftUnitorBimod.hom_inv_id, LeftUnitorBimod.hom_left_act_hom'
actLeft 📖	CompOp	17 math math: TensorBimod.π_tensor_id_actRight, AssociatorBimod.hom_left_act_hom', whiskerLeft_hom, TensorBimod.whiskerLeft_π_actLeft, left_assoc_assoc, Hom.left_act_hom, middle_assoc_assoc, one_actLeft_assoc, one_actLeft, tensorBimod_actLeft, left_assoc, Hom.left_act_hom_assoc, RightUnitorBimod.hom_left_act_hom', middle_assoc, whiskerRight_hom, regular_actLeft, LeftUnitorBimod.hom_left_act_hom'
actRight 📖	CompOp	17 math math: TensorBimod.π_tensor_id_actRight, RightUnitorBimod.hom_right_act_hom', LeftUnitorBimod.hom_right_act_hom', whiskerLeft_hom, TensorBimod.whiskerLeft_π_actLeft, actRight_one, right_assoc, right_assoc_assoc, middle_assoc_assoc, tensorBimod_actRight, regular_actRight, actRight_one_assoc, middle_assoc, whiskerRight_hom, Hom.right_act_hom, Hom.right_act_hom_assoc, AssociatorBimod.hom_right_act_hom'
associatorBimod 📖	CompOp	5 math math: whisker_assoc_bimod, comp_whiskerLeft_bimod, triangle_bimod, pentagon_bimod, whiskerRight_comp_bimod
comp 📖	CompOp	1 math math: comp_hom
forget 📖	CompOp	—
homInhabited 📖	CompOp	—
id' 📖	CompOp	1 math math: id'_hom
instCategory 📖	CompOp	16 math math: id_whiskerLeft_bimod, comp_hom', comp_whiskerRight_bimod, whisker_assoc_bimod, comp_whiskerLeft_bimod, whiskerRight_id_bimod, triangle_bimod, id_whiskerRight_bimod, id_hom', whisker_exchange_bimod, pentagon_bimod, whiskerLeft_id_bimod, isoOfIso_hom_hom, isoOfIso_inv_hom, whiskerLeft_comp_bimod, whiskerRight_comp_bimod
instInhabited 📖	CompOp	—
isoOfIso 📖	CompOp	2 math math: isoOfIso_hom_hom, isoOfIso_inv_hom
leftUnitorBimod 📖	CompOp	2 math math: id_whiskerLeft_bimod, triangle_bimod
monBicategory 📖	CompOp	—
regular 📖	CompOp	14 math math: RightUnitorBimod.hom_right_act_hom', RightUnitorBimod.inv_hom_id, LeftUnitorBimod.hom_right_act_hom', id_whiskerLeft_bimod, LeftUnitorBimod.inv_hom_id, regular_X, regular_actRight, whiskerRight_id_bimod, triangle_bimod, RightUnitorBimod.hom_left_act_hom', regular_actLeft, RightUnitorBimod.hom_inv_id, LeftUnitorBimod.hom_inv_id, LeftUnitorBimod.hom_left_act_hom'
rightUnitorBimod 📖	CompOp	2 math math: whiskerRight_id_bimod, triangle_bimod
tensorBimod 📖	CompOp	25 math math: AssociatorBimod.hom_left_act_hom', RightUnitorBimod.hom_right_act_hom', LeftUnitorBimod.hom_right_act_hom', whiskerLeft_hom, id_whiskerLeft_bimod, AssociatorBimod.hom_inv_id, comp_whiskerRight_bimod, tensorBimod_actRight, whisker_assoc_bimod, tensorBimod_actLeft, comp_whiskerLeft_bimod, whiskerRight_id_bimod, triangle_bimod, RightUnitorBimod.hom_left_act_hom', id_whiskerRight_bimod, AssociatorBimod.inv_hom_id, tensorBimod_X, whisker_exchange_bimod, whiskerRight_hom, pentagon_bimod, whiskerLeft_id_bimod, whiskerLeft_comp_bimod, AssociatorBimod.hom_right_act_hom', whiskerRight_comp_bimod, LeftUnitorBimod.hom_left_act_hom'
whiskerLeft 📖	CompOp	9 math math: whiskerLeft_hom, id_whiskerLeft_bimod, whisker_assoc_bimod, comp_whiskerLeft_bimod, triangle_bimod, whisker_exchange_bimod, pentagon_bimod, whiskerLeft_id_bimod, whiskerLeft_comp_bimod
whiskerRight 📖	CompOp	9 math math: comp_whiskerRight_bimod, whisker_assoc_bimod, whiskerRight_id_bimod, triangle_bimod, id_whiskerRight_bimod, whisker_exchange_bimod, whiskerRight_hom, pentagon_bimod, whiskerRight_comp_bimod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
actRight_one 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct X CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Mon.X CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonObj.one CategoryTheory.Mon.mon actRight CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor	—	—
actRight_one_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct X CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Mon.X CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonObj.one CategoryTheory.Mon.mon actRight CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' actRight_one
comp_hom 📖	mathematical	—	Hom.hom comp CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct X	—	—
comp_hom' 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.comp Bimod CategoryTheory.Category.toCategoryStruct instCategory X	—	—
comp_whiskerLeft_bimod 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight	whiskerLeft tensorBimod CategoryTheory.CategoryStruct.comp Bimod CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Iso.hom associatorBimod CategoryTheory.Iso.inv	—	hom_ext TensorBimod.one_act_left' TensorBimod.left_assoc' TensorBimod.actRight_one' TensorBimod.right_assoc' TensorBimod.middle_assoc' AssociatorBimod.hom_inv_id AssociatorBimod.inv_hom_id AssociatorBimod.hom_left_act_hom' AssociatorBimod.hom_right_act_hom' CategoryTheory.Limits.coequalizer.hom_ext CategoryTheory.Limits.ι_colimMap CategoryTheory.Limits.parallelPairHom_app_one CategoryTheory.Category.assoc CategoryTheory.Limits.coequalizer.π_desc CategoryTheory.cancel_epi CategoryTheory.Limits.map_π_epi CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape π_tensor_id_preserves_coequalizer_inv_desc CategoryTheory.MonoidalCategory.whiskerLeft_comp id_tensor_π_preserves_coequalizer_inv_desc CategoryTheory.MonoidalCategory.associator_inv_naturality_right CategoryTheory.Iso.hom_inv_id_assoc CategoryTheory.MonoidalCategory.whisker_exchange
comp_whiskerRight_bimod 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight	whiskerRight CategoryTheory.CategoryStruct.comp Bimod CategoryTheory.Category.toCategoryStruct instCategory tensorBimod	—	hom_ext CategoryTheory.Limits.coequalizer.hom_ext CategoryTheory.MonoidalCategory.comp_whiskerRight CategoryTheory.Limits.parallelPairHom.congr_simp CategoryTheory.Limits.ι_colimMap CategoryTheory.Category.assoc CategoryTheory.Limits.ι_colimMap_assoc
hom_ext 📖	—	Hom.hom	—	—	Hom.ext
hom_ext_iff 📖	mathematical	—	Hom.hom	—	hom_ext
id'_hom 📖	mathematical	—	Hom.hom id' CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct X	—	—
id_hom' 📖	mathematical	—	Hom.hom CategoryTheory.CategoryStruct.id Bimod CategoryTheory.Category.toCategoryStruct instCategory X	—	—
id_whiskerLeft_bimod 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight	whiskerLeft regular CategoryTheory.CategoryStruct.comp Bimod CategoryTheory.Category.toCategoryStruct instCategory tensorBimod CategoryTheory.Iso.hom leftUnitorBimod CategoryTheory.Iso.inv	—	hom_ext LeftUnitorBimod.hom_inv_id LeftUnitorBimod.inv_hom_id LeftUnitorBimod.hom_left_act_hom' LeftUnitorBimod.hom_right_act_hom' CategoryTheory.Limits.coequalizer.hom_ext CategoryTheory.Limits.ι_colimMap CategoryTheory.Limits.parallelPairHom_app_one CategoryTheory.Category.assoc CategoryTheory.Limits.coequalizer.π_desc Hom.left_act_hom CategoryTheory.MonoidalCategory.leftUnitor_inv_naturality CategoryTheory.MonoidalCategory.whisker_exchange CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.Limits.coequalizer.condition CategoryTheory.MonoidalCategory.associator_inv_naturality_left CategoryTheory.MonoidalCategory.comp_whiskerRight CategoryTheory.MonObj.one_mul Mathlib.Tactic.BicategoryLike.mk_eq Mathlib.Tactic.Monoidal.eval_comp Mathlib.Tactic.Monoidal.eval_whiskerRight Mathlib.Tactic.Monoidal.evalWhiskerRight_nil Mathlib.Tactic.Monoidal.evalComp_nil_nil Mathlib.Tactic.Monoidal.mk_eq_of_naturality Mathlib.Tactic.Monoidal.naturality_comp Mathlib.Tactic.Monoidal.naturality_inv Mathlib.Tactic.Monoidal.naturality_leftUnitor Mathlib.Tactic.Monoidal.naturality_associator Mathlib.Tactic.Monoidal.naturality_whiskerRight Mathlib.Tactic.Monoidal.naturality_id
id_whiskerRight_bimod 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight	whiskerRight CategoryTheory.CategoryStruct.id Bimod CategoryTheory.Category.toCategoryStruct instCategory tensorBimod	—	hom_ext CategoryTheory.Limits.coequalizer.hom_ext CategoryTheory.MonoidalCategory.id_whiskerRight CategoryTheory.Limits.parallelPairHom.congr_simp CategoryTheory.Limits.ι_colimMap CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
isoOfIso_hom_hom 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Mon.X X actLeft CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.whiskerLeft actRight CategoryTheory.MonoidalCategoryStruct.whiskerRight	Hom.hom Bimod instCategory isoOfIso	—	—
isoOfIso_inv_hom 📖	mathematical	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Mon.X X actLeft CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.whiskerLeft actRight CategoryTheory.MonoidalCategoryStruct.whiskerRight	Hom.hom CategoryTheory.Iso.inv Bimod instCategory isoOfIso	—	—
left_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Mon.X X CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul CategoryTheory.Mon.mon actLeft CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	—
left_assoc_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Mon.X X CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul CategoryTheory.Mon.mon actLeft CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' left_assoc
middle_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Mon.X X CategoryTheory.MonoidalCategoryStruct.whiskerRight actLeft actRight CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	—
middle_assoc_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Mon.X X CategoryTheory.MonoidalCategoryStruct.whiskerRight actLeft actRight CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' middle_assoc
one_actLeft 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit X CategoryTheory.Mon.X CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one CategoryTheory.Mon.mon actLeft CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor	—	—
one_actLeft_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit X CategoryTheory.Mon.X CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one CategoryTheory.Mon.mon actLeft CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' one_actLeft
pentagon_bimod 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight	CategoryTheory.CategoryStruct.comp Bimod CategoryTheory.Category.toCategoryStruct instCategory tensorBimod whiskerRight CategoryTheory.Iso.hom associatorBimod whiskerLeft	—	hom_ext AssociatorBimod.hom_inv_id AssociatorBimod.inv_hom_id AssociatorBimod.hom_left_act_hom' AssociatorBimod.hom_right_act_hom' CategoryTheory.Limits.coequalizer.hom_ext CategoryTheory.Category.assoc CategoryTheory.Limits.ι_colimMap CategoryTheory.Limits.parallelPairHom_app_one CategoryTheory.Limits.coequalizer.π_desc CategoryTheory.cancel_epi CategoryTheory.Limits.map_π_epi CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape CategoryTheory.MonoidalCategory.comp_whiskerRight π_tensor_id_preserves_coequalizer_inv_desc CategoryTheory.Limits.comp_preservesColimit CategoryTheory.MonoidalCategory.associator_naturality_middle CategoryTheory.MonoidalCategory.whiskerLeft_comp CategoryTheory.MonoidalCategory.associator_naturality_left CategoryTheory.MonoidalCategory.whisker_exchange CategoryTheory.MonoidalCategory.associator_naturality_right Mathlib.Tactic.BicategoryLike.mk_eq Mathlib.Tactic.Monoidal.eval_comp Mathlib.Tactic.Monoidal.eval_whiskerRight Mathlib.Tactic.Monoidal.evalWhiskerRight_nil Mathlib.Tactic.Monoidal.eval_whiskerLeft Mathlib.Tactic.Monoidal.evalWhiskerLeft_nil Mathlib.Tactic.Monoidal.eval_of Mathlib.Tactic.Monoidal.evalWhiskerLeft_of_cons Mathlib.Tactic.Monoidal.evalComp_cons Mathlib.Tactic.Monoidal.evalComp_nil_cons Mathlib.Tactic.BicategoryLike.mk_eq_of_cons Mathlib.Tactic.Monoidal.mk_eq_of_naturality Mathlib.Tactic.Monoidal.naturality_comp Mathlib.Tactic.Monoidal.naturality_whiskerRight Mathlib.Tactic.Monoidal.naturality_associator Mathlib.Tactic.Monoidal.naturality_whiskerLeft Mathlib.Tactic.Monoidal.naturality_id
regular_X 📖	mathematical	—	X regular CategoryTheory.Mon.X	—	—
regular_actLeft 📖	mathematical	—	actLeft regular CategoryTheory.MonObj.mul CategoryTheory.Mon.X CategoryTheory.Mon.mon	—	—
regular_actRight 📖	mathematical	—	actRight regular CategoryTheory.MonObj.mul CategoryTheory.Mon.X CategoryTheory.Mon.mon	—	—
right_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct X CategoryTheory.Mon.X CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonObj.mul CategoryTheory.Mon.mon actRight CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	—
right_assoc_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct X CategoryTheory.Mon.X CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonObj.mul CategoryTheory.Mon.mon actRight CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' right_assoc
tensorBimod_X 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight	X tensorBimod TensorBimod.X	—	—
tensorBimod_actLeft 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight	actLeft tensorBimod TensorBimod.actLeft	—	—
tensorBimod_actRight 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight	actRight tensorBimod TensorBimod.actRight	—	—
triangle_bimod 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight	CategoryTheory.CategoryStruct.comp Bimod CategoryTheory.Category.toCategoryStruct instCategory tensorBimod regular CategoryTheory.Iso.hom associatorBimod whiskerLeft leftUnitorBimod whiskerRight rightUnitorBimod	—	hom_ext AssociatorBimod.hom_inv_id AssociatorBimod.inv_hom_id AssociatorBimod.hom_left_act_hom' AssociatorBimod.hom_right_act_hom' LeftUnitorBimod.hom_inv_id LeftUnitorBimod.inv_hom_id LeftUnitorBimod.hom_left_act_hom' LeftUnitorBimod.hom_right_act_hom' RightUnitorBimod.hom_inv_id RightUnitorBimod.inv_hom_id RightUnitorBimod.hom_left_act_hom' RightUnitorBimod.hom_right_act_hom' CategoryTheory.Limits.coequalizer.hom_ext CategoryTheory.Category.assoc CategoryTheory.Limits.coequalizer.π_desc CategoryTheory.Limits.ι_colimMap CategoryTheory.Limits.parallelPairHom_app_one CategoryTheory.cancel_epi CategoryTheory.Limits.map_π_epi CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape π_tensor_id_preserves_coequalizer_inv_desc CategoryTheory.MonoidalCategory.whiskerLeft_comp CategoryTheory.MonoidalCategory.comp_whiskerRight CategoryTheory.Limits.coequalizer.condition
whiskerLeft_comp_bimod 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight	whiskerLeft CategoryTheory.CategoryStruct.comp Bimod CategoryTheory.Category.toCategoryStruct instCategory tensorBimod	—	hom_ext CategoryTheory.Limits.coequalizer.hom_ext CategoryTheory.MonoidalCategory.whiskerLeft_comp CategoryTheory.MonoidalCategory.tensor_whiskerLeft CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.Limits.parallelPairHom.congr_simp CategoryTheory.Limits.ι_colimMap CategoryTheory.Limits.ι_colimMap_assoc
whiskerLeft_hom 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight	Hom.hom tensorBimod whiskerLeft CategoryTheory.Limits.colimMap CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct X CategoryTheory.Mon.X CategoryTheory.MonoidalCategoryStruct.whiskerRight actRight CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft actLeft CategoryTheory.Limits.parallelPairHom	—	—
whiskerLeft_id_bimod 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight	whiskerLeft CategoryTheory.CategoryStruct.id Bimod CategoryTheory.Category.toCategoryStruct instCategory tensorBimod	—	hom_ext CategoryTheory.Limits.coequalizer.hom_ext CategoryTheory.MonoidalCategory.whiskerLeft_id CategoryTheory.Limits.parallelPairHom.congr_simp CategoryTheory.Limits.ι_colimMap CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id
whiskerRight_comp_bimod 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight	whiskerRight tensorBimod CategoryTheory.CategoryStruct.comp Bimod CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Iso.inv associatorBimod CategoryTheory.Iso.hom	—	hom_ext TensorBimod.one_act_left' TensorBimod.left_assoc' TensorBimod.actRight_one' TensorBimod.right_assoc' TensorBimod.middle_assoc' AssociatorBimod.hom_inv_id AssociatorBimod.inv_hom_id AssociatorBimod.hom_left_act_hom' AssociatorBimod.hom_right_act_hom' CategoryTheory.Limits.coequalizer.hom_ext CategoryTheory.Limits.ι_colimMap CategoryTheory.Limits.parallelPairHom_app_one CategoryTheory.Category.assoc CategoryTheory.Limits.coequalizer.π_desc CategoryTheory.cancel_epi CategoryTheory.Limits.map_π_epi CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape id_tensor_π_preserves_coequalizer_inv_desc CategoryTheory.MonoidalCategory.comp_whiskerRight π_tensor_id_preserves_coequalizer_inv_desc CategoryTheory.MonoidalCategory.associator_naturality_left CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.MonoidalCategory.whisker_exchange
whiskerRight_hom 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight	Hom.hom tensorBimod whiskerRight CategoryTheory.Limits.colimMap CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct X CategoryTheory.Mon.X CategoryTheory.MonoidalCategoryStruct.whiskerRight actRight CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft actLeft CategoryTheory.Limits.parallelPairHom	—	—
whiskerRight_id_bimod 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight	whiskerRight regular CategoryTheory.CategoryStruct.comp Bimod CategoryTheory.Category.toCategoryStruct instCategory tensorBimod CategoryTheory.Iso.hom rightUnitorBimod CategoryTheory.Iso.inv	—	hom_ext RightUnitorBimod.hom_inv_id RightUnitorBimod.inv_hom_id RightUnitorBimod.hom_left_act_hom' RightUnitorBimod.hom_right_act_hom' CategoryTheory.Limits.coequalizer.hom_ext CategoryTheory.Limits.ι_colimMap CategoryTheory.Limits.parallelPairHom_app_one CategoryTheory.Category.assoc CategoryTheory.Limits.coequalizer.π_desc Hom.right_act_hom CategoryTheory.MonoidalCategory.rightUnitor_inv_naturality CategoryTheory.MonoidalCategory.whisker_exchange CategoryTheory.Limits.coequalizer.condition CategoryTheory.MonoidalCategory.associator_naturality_right CategoryTheory.MonoidalCategory.whiskerLeft_comp CategoryTheory.MonObj.mul_one CategoryTheory.MonoidalCategory.whiskerLeft_rightUnitor CategoryTheory.Iso.hom_inv_id_assoc CategoryTheory.Iso.inv_hom_id_assoc
whisker_assoc_bimod 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight	whiskerRight tensorBimod whiskerLeft CategoryTheory.CategoryStruct.comp Bimod CategoryTheory.Category.toCategoryStruct instCategory CategoryTheory.Iso.hom associatorBimod CategoryTheory.Iso.inv	—	hom_ext TensorBimod.one_act_left' TensorBimod.left_assoc' TensorBimod.actRight_one' TensorBimod.right_assoc' TensorBimod.middle_assoc' AssociatorBimod.hom_inv_id AssociatorBimod.inv_hom_id AssociatorBimod.hom_left_act_hom' AssociatorBimod.hom_right_act_hom' CategoryTheory.Limits.coequalizer.hom_ext CategoryTheory.Limits.ι_colimMap CategoryTheory.Limits.parallelPairHom_app_one CategoryTheory.Category.assoc CategoryTheory.Limits.coequalizer.π_desc CategoryTheory.cancel_epi CategoryTheory.Limits.map_π_epi CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape CategoryTheory.MonoidalCategory.comp_whiskerRight π_tensor_id_preserves_coequalizer_inv_desc CategoryTheory.MonoidalCategory.whiskerLeft_comp id_tensor_π_preserves_coequalizer_inv_desc CategoryTheory.MonoidalCategory.whisker_assoc
whisker_exchange_bimod 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight	CategoryTheory.CategoryStruct.comp Bimod CategoryTheory.Category.toCategoryStruct instCategory tensorBimod whiskerLeft whiskerRight	—	hom_ext CategoryTheory.Limits.coequalizer.hom_ext CategoryTheory.Category.assoc CategoryTheory.Limits.ι_colimMap CategoryTheory.Limits.parallelPairHom_app_one CategoryTheory.MonoidalCategory.whisker_exchange CategoryTheory.MonoidalCategory.tensor_whiskerLeft CategoryTheory.Limits.parallelPairHom.congr_simp CategoryTheory.Limits.ι_colimMap_assoc

Bimod.AssociatorBimod

Definitions

Name	Category	Theorems
hom 📖	CompOp	4 math math: hom_left_act_hom', hom_inv_id, inv_hom_id, hom_right_act_hom'
homAux 📖	CompOp	—
inv 📖	CompOp	2 math math: hom_inv_id, inv_hom_id
invAux 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hom_inv_id 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Bimod.X Bimod.tensorBimod hom inv CategoryTheory.CategoryStruct.id	—	CategoryTheory.Limits.coequalizer.hom_ext CategoryTheory.Category.assoc CategoryTheory.Limits.coequalizer.π_desc CategoryTheory.cancel_epi CategoryTheory.Limits.map_π_epi CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape π_tensor_id_preserves_coequalizer_inv_desc id_tensor_π_preserves_coequalizer_inv_desc CategoryTheory.Iso.hom_inv_id_assoc CategoryTheory.Category.comp_id
hom_left_act_hom' 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Mon.X Bimod.X Bimod.tensorBimod Bimod.actLeft hom CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.cancel_epi CategoryTheory.Limits.map_π_epi CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape CategoryTheory.Category.assoc Bimod.TensorBimod.whiskerLeft_π_actLeft CategoryTheory.Limits.coequalizer.π_desc CategoryTheory.MonoidalCategory.whiskerLeft_comp CategoryTheory.Limits.comp_preservesColimit CategoryTheory.MonoidalCategory.associator_inv_naturality_middle CategoryTheory.MonoidalCategory.comp_whiskerRight π_tensor_id_preserves_coequalizer_inv_desc CategoryTheory.MonoidalCategory.associator_naturality_left CategoryTheory.MonoidalCategory.associator_inv_naturality_right CategoryTheory.MonoidalCategory.whisker_exchange Mathlib.Tactic.BicategoryLike.mk_eq Mathlib.Tactic.Monoidal.eval_comp Mathlib.Tactic.Monoidal.eval_whiskerRight Mathlib.Tactic.Monoidal.evalWhiskerRight_nil Mathlib.Tactic.Monoidal.eval_of Mathlib.Tactic.Monoidal.evalWhiskerRight_comp Mathlib.Tactic.Monoidal.evalWhiskerRight_cons_of_of Mathlib.Tactic.Monoidal.evalWhiskerRightAux_of Mathlib.Tactic.Monoidal.evalComp_cons Mathlib.Tactic.Monoidal.evalComp_nil_nil Mathlib.Tactic.Monoidal.evalComp_nil_cons Mathlib.Tactic.Monoidal.eval_whiskerLeft Mathlib.Tactic.Monoidal.evalWhiskerLeft_of_cons Mathlib.Tactic.Monoidal.evalWhiskerLeft_nil Mathlib.Tactic.BicategoryLike.mk_eq_of_cons Mathlib.Tactic.Monoidal.mk_eq_of_naturality Mathlib.Tactic.Monoidal.naturality_comp Mathlib.Tactic.Monoidal.naturality_inv Mathlib.Tactic.Monoidal.naturality_associator Mathlib.Tactic.Monoidal.naturality_whiskerRight Mathlib.Tactic.Monoidal.naturality_id Mathlib.Tactic.Monoidal.naturality_whiskerLeft
hom_right_act_hom' 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Bimod.X Bimod.tensorBimod CategoryTheory.Mon.X Bimod.actRight hom CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	CategoryTheory.cancel_epi CategoryTheory.Limits.map_π_epi CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape CategoryTheory.Category.assoc Bimod.TensorBimod.π_tensor_id_actRight CategoryTheory.Limits.coequalizer.π_desc CategoryTheory.MonoidalCategory.comp_whiskerRight CategoryTheory.Limits.comp_preservesColimit CategoryTheory.MonoidalCategory.associator_naturality_left CategoryTheory.MonoidalCategory.whisker_exchange π_tensor_id_preserves_coequalizer_inv_desc CategoryTheory.MonoidalCategory.associator_naturality_right CategoryTheory.MonoidalCategory.associator_naturality_middle CategoryTheory.MonoidalCategory.whiskerLeft_comp Mathlib.Tactic.BicategoryLike.mk_eq Mathlib.Tactic.Monoidal.eval_comp Mathlib.Tactic.Monoidal.eval_whiskerLeft Mathlib.Tactic.Monoidal.eval_of Mathlib.Tactic.Monoidal.evalWhiskerLeft_of_cons Mathlib.Tactic.Monoidal.evalWhiskerLeft_nil Mathlib.Tactic.Monoidal.evalComp_nil_cons Mathlib.Tactic.Monoidal.evalComp_cons Mathlib.Tactic.Monoidal.eval_whiskerRight Mathlib.Tactic.Monoidal.evalWhiskerRight_nil Mathlib.Tactic.BicategoryLike.mk_eq_of_cons Mathlib.Tactic.Monoidal.mk_eq_of_naturality Mathlib.Tactic.Monoidal.naturality_comp Mathlib.Tactic.Monoidal.naturality_associator Mathlib.Tactic.Monoidal.naturality_whiskerLeft Mathlib.Tactic.Monoidal.naturality_id Mathlib.Tactic.Monoidal.naturality_whiskerRight
inv_hom_id 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Bimod.X Bimod.tensorBimod inv hom CategoryTheory.CategoryStruct.id	—	CategoryTheory.Limits.coequalizer.hom_ext CategoryTheory.Category.assoc CategoryTheory.Limits.coequalizer.π_desc CategoryTheory.cancel_epi CategoryTheory.Limits.map_π_epi CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape id_tensor_π_preserves_coequalizer_inv_desc π_tensor_id_preserves_coequalizer_inv_desc CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.Category.comp_id

Bimod.Hom

Definitions

Name	Category	Theorems
hom 📖	CompOp	14 math math: Bimod.whiskerLeft_hom, left_act_hom, Bimod.comp_hom, Bimod.hom_ext_iff, Bimod.comp_hom', Bimod.id'_hom, left_act_hom_assoc, Bimod.id_hom', Bimod.whiskerRight_hom, right_act_hom, Bimod.isoOfIso_hom_hom, Bimod.isoOfIso_inv_hom, right_act_hom_assoc, ext_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	hom	—	—	—
ext_iff 📖	mathematical	—	hom	—	ext
left_act_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Mon.X Bimod.X Bimod.actLeft hom CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	—
left_act_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Mon.X Bimod.X Bimod.actLeft hom CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' left_act_hom
right_act_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Bimod.X CategoryTheory.Mon.X Bimod.actRight hom CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	—
right_act_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Bimod.X CategoryTheory.Mon.X Bimod.actRight hom CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' right_act_hom

Bimod.LeftUnitorBimod

Definitions

Name	Category	Theorems
hom 📖	CompOp	4 math math: hom_right_act_hom', inv_hom_id, hom_inv_id, hom_left_act_hom'
inv 📖	CompOp	2 math math: inv_hom_id, hom_inv_id

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hom_inv_id 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Bimod.TensorBimod.X Bimod.regular Bimod.X hom inv CategoryTheory.CategoryStruct.id	—	CategoryTheory.Limits.coequalizer.hom_ext CategoryTheory.Category.assoc CategoryTheory.Limits.coequalizer.π_desc CategoryTheory.MonoidalCategory.leftUnitor_inv_naturality CategoryTheory.MonoidalCategory.whisker_exchange CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.Limits.coequalizer.condition CategoryTheory.MonoidalCategory.associator_inv_naturality_left CategoryTheory.MonoidalCategory.comp_whiskerRight CategoryTheory.MonObj.one_mul CategoryTheory.Category.comp_id Mathlib.Tactic.BicategoryLike.mk_eq Mathlib.Tactic.Monoidal.eval_comp Mathlib.Tactic.Monoidal.eval_whiskerRight Mathlib.Tactic.Monoidal.evalWhiskerRight_nil Mathlib.Tactic.Monoidal.eval_of Mathlib.Tactic.Monoidal.evalComp_nil_cons Mathlib.Tactic.BicategoryLike.mk_eq_of_cons Mathlib.Tactic.Monoidal.mk_eq_of_naturality Mathlib.Tactic.Monoidal.naturality_comp Mathlib.Tactic.Monoidal.naturality_inv Mathlib.Tactic.Monoidal.naturality_leftUnitor Mathlib.Tactic.Monoidal.naturality_associator Mathlib.Tactic.Monoidal.naturality_whiskerRight Mathlib.Tactic.Monoidal.naturality_id
hom_left_act_hom' 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Mon.X Bimod.X Bimod.tensorBimod Bimod.regular Bimod.actLeft hom Bimod.TensorBimod.X CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.cancel_epi CategoryTheory.Limits.map_π_epi CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape CategoryTheory.Category.assoc id_tensor_π_preserves_coequalizer_inv_colimMap_desc Bimod.left_assoc CategoryTheory.MonoidalCategory.whiskerLeft_comp CategoryTheory.Limits.coequalizer.π_desc CategoryTheory.Iso.inv_hom_id_assoc
hom_right_act_hom' 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Bimod.X Bimod.tensorBimod Bimod.regular CategoryTheory.Mon.X Bimod.actRight hom Bimod.TensorBimod.X CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	CategoryTheory.cancel_epi CategoryTheory.Limits.map_π_epi CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape CategoryTheory.Category.assoc π_tensor_id_preserves_coequalizer_inv_colimMap_desc CategoryTheory.MonoidalCategory.comp_whiskerRight CategoryTheory.Limits.coequalizer.π_desc Bimod.middle_assoc
inv_hom_id 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Bimod.X Bimod.TensorBimod.X Bimod.regular inv hom CategoryTheory.CategoryStruct.id	—	CategoryTheory.Category.assoc CategoryTheory.Limits.coequalizer.π_desc Bimod.one_actLeft CategoryTheory.Iso.inv_hom_id

Bimod.RightUnitorBimod

Definitions

Name	Category	Theorems
hom 📖	CompOp	4 math math: hom_right_act_hom', inv_hom_id, hom_left_act_hom', hom_inv_id
inv 📖	CompOp	2 math math: inv_hom_id, hom_inv_id

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hom_inv_id 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Bimod.TensorBimod.X Bimod.regular Bimod.X hom inv CategoryTheory.CategoryStruct.id	—	CategoryTheory.Limits.coequalizer.hom_ext CategoryTheory.Category.assoc CategoryTheory.Limits.coequalizer.π_desc CategoryTheory.MonoidalCategory.rightUnitor_inv_naturality CategoryTheory.MonoidalCategory.whisker_exchange CategoryTheory.Limits.coequalizer.condition CategoryTheory.MonoidalCategory.associator_naturality_right CategoryTheory.MonoidalCategory.whiskerLeft_comp CategoryTheory.MonObj.mul_one CategoryTheory.Category.comp_id Mathlib.Tactic.BicategoryLike.mk_eq Mathlib.Tactic.Monoidal.eval_comp Mathlib.Tactic.Monoidal.eval_whiskerLeft Mathlib.Tactic.Monoidal.evalWhiskerLeft_nil Mathlib.Tactic.Monoidal.eval_of Mathlib.Tactic.Monoidal.evalComp_nil_cons Mathlib.Tactic.BicategoryLike.mk_eq_of_cons Mathlib.Tactic.Monoidal.mk_eq_of_naturality Mathlib.Tactic.Monoidal.naturality_comp Mathlib.Tactic.Monoidal.naturality_inv Mathlib.Tactic.Monoidal.naturality_rightUnitor Mathlib.Tactic.Monoidal.naturality_associator Mathlib.Tactic.Monoidal.naturality_whiskerLeft Mathlib.Tactic.Monoidal.naturality_id
hom_left_act_hom' 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Mon.X Bimod.X Bimod.tensorBimod Bimod.regular Bimod.actLeft hom Bimod.TensorBimod.X CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.cancel_epi CategoryTheory.Limits.map_π_epi CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape CategoryTheory.Category.assoc id_tensor_π_preserves_coequalizer_inv_colimMap_desc Bimod.middle_assoc CategoryTheory.MonoidalCategory.whiskerLeft_comp CategoryTheory.Limits.coequalizer.π_desc CategoryTheory.Iso.inv_hom_id_assoc
hom_right_act_hom' 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Bimod.X Bimod.tensorBimod Bimod.regular CategoryTheory.Mon.X Bimod.actRight hom Bimod.TensorBimod.X CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	CategoryTheory.cancel_epi CategoryTheory.Limits.map_π_epi CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape CategoryTheory.Category.assoc π_tensor_id_preserves_coequalizer_inv_colimMap_desc Bimod.right_assoc CategoryTheory.MonoidalCategory.comp_whiskerRight CategoryTheory.Limits.coequalizer.π_desc CategoryTheory.Iso.hom_inv_id_assoc
inv_hom_id 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Bimod.X Bimod.TensorBimod.X Bimod.regular inv hom CategoryTheory.CategoryStruct.id	—	CategoryTheory.Category.assoc CategoryTheory.Limits.coequalizer.π_desc Bimod.actRight_one CategoryTheory.Iso.inv_hom_id

Bimod.TensorBimod

Definitions

Name	Category	Theorems
X 📖	CompOp	16 math math: π_tensor_id_actRight, Bimod.RightUnitorBimod.hom_right_act_hom', Bimod.RightUnitorBimod.inv_hom_id, Bimod.LeftUnitorBimod.hom_right_act_hom', right_assoc', whiskerLeft_π_actLeft, actRight_one', middle_assoc', Bimod.LeftUnitorBimod.inv_hom_id, left_assoc', Bimod.RightUnitorBimod.hom_left_act_hom', Bimod.tensorBimod_X, one_act_left', Bimod.RightUnitorBimod.hom_inv_id, Bimod.LeftUnitorBimod.hom_inv_id, Bimod.LeftUnitorBimod.hom_left_act_hom'
actLeft 📖	CompOp	5 math math: whiskerLeft_π_actLeft, middle_assoc', left_assoc', Bimod.tensorBimod_actLeft, one_act_left'
actRight 📖	CompOp	5 math math: π_tensor_id_actRight, right_assoc', actRight_one', middle_assoc', Bimod.tensorBimod_actRight

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
actRight_one' 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.MonoidalCategory.tensorRight	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct X CategoryTheory.MonoidalCategoryStruct.tensorUnit CategoryTheory.Mon.X CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonObj.one CategoryTheory.Mon.mon actRight CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.rightUnitor	—	CategoryTheory.cancel_epi CategoryTheory.Limits.map_π_epi CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape CategoryTheory.Category.assoc CategoryTheory.MonoidalCategory.whisker_exchange π_tensor_id_actRight CategoryTheory.MonoidalCategory.associator_naturality_right CategoryTheory.MonoidalCategory.whiskerLeft_comp Bimod.actRight_one CategoryTheory.MonoidalCategory.whiskerLeft_rightUnitor CategoryTheory.Iso.hom_inv_id_assoc CategoryTheory.MonoidalCategory.whiskerRight_id CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.comp_id
left_assoc' 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.MonoidalCategory.tensorLeft	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Mon.X X CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul CategoryTheory.Mon.mon actLeft CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.cancel_epi CategoryTheory.Limits.map_π_epi CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape CategoryTheory.Category.assoc CategoryTheory.MonoidalCategory.whisker_exchange whiskerLeft_π_actLeft CategoryTheory.MonoidalCategory.associator_inv_naturality_left CategoryTheory.MonoidalCategory.comp_whiskerRight Bimod.left_assoc CategoryTheory.MonoidalCategory.associator_naturality_right CategoryTheory.MonoidalCategory.whiskerLeft_comp CategoryTheory.MonoidalCategory.associator_inv_naturality_middle Mathlib.Tactic.BicategoryLike.mk_eq Mathlib.Tactic.Monoidal.eval_comp Mathlib.Tactic.Monoidal.eval_whiskerRight Mathlib.Tactic.Monoidal.evalWhiskerRight_nil Mathlib.Tactic.Monoidal.eval_whiskerLeft Mathlib.Tactic.Monoidal.eval_of Mathlib.Tactic.Monoidal.evalWhiskerLeft_of_cons Mathlib.Tactic.Monoidal.evalWhiskerLeft_nil Mathlib.Tactic.Monoidal.evalWhiskerRight_cons_whisker Mathlib.Tactic.Monoidal.evalWhiskerRight_cons_of_of Mathlib.Tactic.Monoidal.evalWhiskerRightAux_of Mathlib.Tactic.Monoidal.evalComp_cons Mathlib.Tactic.Monoidal.evalComp_nil_nil Mathlib.Tactic.Monoidal.evalComp_nil_cons Mathlib.Tactic.BicategoryLike.mk_eq_of_cons Mathlib.Tactic.Monoidal.mk_eq_of_naturality Mathlib.Tactic.Monoidal.naturality_comp Mathlib.Tactic.Monoidal.naturality_inv Mathlib.Tactic.Monoidal.naturality_associator Mathlib.Tactic.Monoidal.naturality_whiskerRight Mathlib.Tactic.Monoidal.naturality_whiskerLeft Mathlib.Tactic.Monoidal.naturality_id
middle_assoc' 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.MonoidalCategory.tensorRight	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Mon.X X CategoryTheory.MonoidalCategoryStruct.whiskerRight actLeft actRight CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft	—	CategoryTheory.cancel_epi CategoryTheory.Limits.map_π_epi CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.comp_preservesColimit CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape CategoryTheory.Category.assoc CategoryTheory.MonoidalCategory.comp_whiskerRight whiskerLeft_π_actLeft π_tensor_id_actRight CategoryTheory.MonoidalCategory.associator_naturality_left CategoryTheory.MonoidalCategory.associator_naturality_middle CategoryTheory.MonoidalCategory.whiskerLeft_comp CategoryTheory.MonoidalCategory.associator_inv_naturality_right CategoryTheory.MonoidalCategory.whisker_exchange CategoryTheory.MonoidalCategory.whiskerRight_tensor CategoryTheory.Iso.hom_inv_id_assoc CategoryTheory.MonoidalCategory.pentagon_hom_inv_inv_inv_inv_assoc
one_act_left' 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.MonoidalCategory.tensorLeft	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorUnit X CategoryTheory.Mon.X CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.one CategoryTheory.Mon.mon actLeft CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.leftUnitor	—	CategoryTheory.cancel_epi CategoryTheory.Limits.map_π_epi CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape CategoryTheory.Category.assoc CategoryTheory.MonoidalCategory.whisker_exchange whiskerLeft_π_actLeft CategoryTheory.MonoidalCategory.associator_inv_naturality_left CategoryTheory.MonoidalCategory.comp_whiskerRight Bimod.one_actLeft CategoryTheory.MonoidalCategory.leftUnitor_naturality Mathlib.Tactic.BicategoryLike.mk_eq Mathlib.Tactic.Monoidal.eval_comp Mathlib.Tactic.Monoidal.eval_whiskerRight Mathlib.Tactic.Monoidal.evalWhiskerRight_nil Mathlib.Tactic.Monoidal.eval_of Mathlib.Tactic.Monoidal.evalComp_nil_cons Mathlib.Tactic.BicategoryLike.mk_eq_of_cons Mathlib.Tactic.Monoidal.mk_eq_of_naturality Mathlib.Tactic.Monoidal.naturality_comp Mathlib.Tactic.Monoidal.naturality_inv Mathlib.Tactic.Monoidal.naturality_associator Mathlib.Tactic.Monoidal.naturality_whiskerRight Mathlib.Tactic.Monoidal.naturality_leftUnitor Mathlib.Tactic.Monoidal.naturality_id
right_assoc' 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.MonoidalCategory.tensorRight	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct X CategoryTheory.Mon.X CategoryTheory.MonoidalCategoryStruct.whiskerLeft CategoryTheory.MonObj.mul CategoryTheory.Mon.mon actRight CategoryTheory.Iso.inv CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerRight	—	CategoryTheory.cancel_epi CategoryTheory.Limits.map_π_epi CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape CategoryTheory.Category.assoc CategoryTheory.MonoidalCategory.whisker_exchange π_tensor_id_actRight CategoryTheory.MonoidalCategory.associator_naturality_right CategoryTheory.MonoidalCategory.whiskerLeft_comp Bimod.right_assoc CategoryTheory.MonoidalCategory.associator_inv_naturality_left CategoryTheory.MonoidalCategory.comp_whiskerRight CategoryTheory.MonoidalCategory.whisker_assoc CategoryTheory.Iso.inv_hom_id_assoc CategoryTheory.MonoidalCategory.pentagon_inv_hom_hom_hom_inv_assoc
whiskerLeft_π_actLeft 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.MonoidalCategory.tensorLeft	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.Mon.X Bimod.X CategoryTheory.Limits.coequalizer CategoryTheory.MonoidalCategoryStruct.whiskerRight Bimod.actRight CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft Bimod.actLeft X CategoryTheory.Limits.coequalizer.π actLeft CategoryTheory.Iso.inv	—	CategoryTheory.Limits.map_π_preserves_coequalizer_inv_colimMap CategoryTheory.Category.assoc
π_tensor_id_actRight 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.MonoidalCategory.tensorRight	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct Bimod.X CategoryTheory.Mon.X CategoryTheory.Limits.coequalizer CategoryTheory.MonoidalCategoryStruct.whiskerRight Bimod.actRight CategoryTheory.Iso.hom CategoryTheory.MonoidalCategoryStruct.associator CategoryTheory.MonoidalCategoryStruct.whiskerLeft Bimod.actLeft X CategoryTheory.Limits.coequalizer.π actRight	—	CategoryTheory.Limits.map_π_preserves_coequalizer_inv_colimMap CategoryTheory.Category.assoc

(root)

Definitions

Name	Category	Theorems
Bimod 📖	CompData	16 math math: Bimod.id_whiskerLeft_bimod, Bimod.comp_hom', Bimod.comp_whiskerRight_bimod, Bimod.whisker_assoc_bimod, Bimod.comp_whiskerLeft_bimod, Bimod.whiskerRight_id_bimod, Bimod.triangle_bimod, Bimod.id_whiskerRight_bimod, Bimod.id_hom', Bimod.whisker_exchange_bimod, Bimod.pentagon_bimod, Bimod.whiskerLeft_id_bimod, Bimod.isoOfIso_hom_hom, Bimod.isoOfIso_inv_hom, Bimod.whiskerLeft_comp_bimod, Bimod.whiskerRight_comp_bimod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
id_tensor_π_preserves_coequalizer_inv_colimMap_desc 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerLeft	CategoryTheory.Limits.coequalizer CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair CategoryTheory.Limits.coequalizer.π CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Iso.inv CategoryTheory.Limits.PreservesCoequalizer.iso CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape CategoryTheory.Limits.colimit CategoryTheory.Limits.colimMap CategoryTheory.Limits.parallelPairHom CategoryTheory.Limits.coequalizer.desc	—	CategoryTheory.Limits.map_π_preserves_coequalizer_inv_colimMap_desc CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape
id_tensor_π_preserves_coequalizer_inv_desc 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.MonoidalCategory.tensorLeft CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerLeft	CategoryTheory.Limits.coequalizer CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair CategoryTheory.Limits.coequalizer.π CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Iso.inv CategoryTheory.Limits.PreservesCoequalizer.iso CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape CategoryTheory.Limits.coequalizer.desc	—	CategoryTheory.Limits.map_π_preserves_coequalizer_inv_desc CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape
π_tensor_id_preserves_coequalizer_inv_colimMap_desc 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.MonoidalCategory.tensorRight CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerRight	CategoryTheory.Limits.coequalizer CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair CategoryTheory.Limits.coequalizer.π CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Iso.inv CategoryTheory.Limits.PreservesCoequalizer.iso CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape CategoryTheory.Limits.colimit CategoryTheory.Limits.colimMap CategoryTheory.Limits.parallelPairHom CategoryTheory.Limits.coequalizer.desc	—	CategoryTheory.Limits.map_π_preserves_coequalizer_inv_colimMap_desc CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape
π_tensor_id_preserves_coequalizer_inv_desc 📖	mathematical	CategoryTheory.Limits.PreservesColimitsOfSize CategoryTheory.MonoidalCategory.tensorRight CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.MonoidalCategoryStruct.tensorObj CategoryTheory.MonoidalCategory.toMonoidalCategoryStruct CategoryTheory.MonoidalCategoryStruct.whiskerRight	CategoryTheory.Limits.coequalizer CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.WalkingParallelPair CategoryTheory.Limits.walkingParallelPairHomCategory CategoryTheory.Limits.parallelPair CategoryTheory.Limits.coequalizer.π CategoryTheory.Functor.obj CategoryTheory.Functor.map CategoryTheory.Iso.inv CategoryTheory.Limits.PreservesCoequalizer.iso CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape CategoryTheory.Limits.coequalizer.desc	—	CategoryTheory.Limits.map_π_preserves_coequalizer_inv_desc CategoryTheory.Limits.hasColimitOfHasColimitsOfShape CategoryTheory.Limits.PreservesColimitsOfShape.preservesColimit CategoryTheory.Limits.PreservesColimitsOfSize.preservesColimitsOfShape

---

← Back to Index