Trifunctor

📁 Source: Mathlib/CategoryTheory/GradedObject/Trifunctor.lean

Statistics

Metric	Count
Definitions BifunctorComp₁₂IndexData, I₁₂, p, q, BifunctorComp₂₃IndexData, I₂₃, p, q, HasGoodTrifunctor₁₂Obj, HasGoodTrifunctor₂₃Obj, cofan₃MapBifunctorBifunctor₂₃MapObj, cofan₃MapBifunctor₁₂BifunctorMapObj, isColimitCofan₃MapBifunctorBifunctor₂₃MapObj, isColimitCofan₃MapBifunctor₁₂BifunctorMapObj, mapBifunctorBifunctor₂₃Desc, mapBifunctorComp₁₂MapObjIso, mapBifunctorComp₂₃MapObjIso, mapBifunctor₁₂BifunctorDesc, mapTrifunctor, mapTrifunctorMap, mapTrifunctorMapFunctorObj, mapTrifunctorMapIso, mapTrifunctorMapMap, mapTrifunctorMapNatTrans, mapTrifunctorMapObj, mapTrifunctorObj, ιMapBifunctorBifunctor₂₃MapObj, ιMapBifunctor₁₂BifunctorMapObj, ιMapTrifunctorMapObj	29
Theorems hpq, hpq, hasMap, hasMap, instHasMapProdObjFunctorMapTrifunctorObjOfMapTrifunctor, mapBifunctorBifunctor₂₃MapObj_ext, mapBifunctorBifunctor₂₃MapObj_ext_iff, mapBifunctor₁₂BifunctorMapObj_ext, mapBifunctor₁₂BifunctorMapObj_ext_iff, mapTrifunctorMapFunctorObj_map_app, mapTrifunctorMapFunctorObj_obj_map, mapTrifunctorMapFunctorObj_obj_obj, mapTrifunctorMapIso_hom, mapTrifunctorMapIso_inv, mapTrifunctorMapNatTrans_app_app_app, mapTrifunctorMapObj_ext, mapTrifunctorMapObj_ext_iff, mapTrifunctorMap_map_app_app, mapTrifunctorMap_obj, mapTrifunctorObj_map_app, mapTrifunctorObj_obj_map, mapTrifunctorObj_obj_obj, mapTrifunctor_map_app_app, mapTrifunctor_obj, ιMapBifunctorBifunctor₂₃MapObj_eq, ιMapBifunctorBifunctor₂₃MapObj_eq_assoc, ιMapBifunctor₁₂BifunctorMapObj_eq, ιMapBifunctor₁₂BifunctorMapObj_eq_assoc, ι_mapBifunctorBifunctor₂₃Desc, ι_mapBifunctorBifunctor₂₃Desc_assoc, ι_mapBifunctorComp₁₂MapObjIso_hom, ι_mapBifunctorComp₁₂MapObjIso_hom_assoc, ι_mapBifunctorComp₁₂MapObjIso_inv, ι_mapBifunctorComp₁₂MapObjIso_inv_assoc, ι_mapBifunctorComp₂₃MapObjIso_hom, ι_mapBifunctorComp₂₃MapObjIso_hom_assoc, ι_mapBifunctorComp₂₃MapObjIso_inv, ι_mapBifunctorComp₂₃MapObjIso_inv_assoc, ι_mapBifunctor₁₂BifunctorDesc, ι_mapBifunctor₁₂BifunctorDesc_assoc, ι_mapTrifunctorMapMap, ι_mapTrifunctorMapMap_assoc	42
Total	71

CategoryTheory.GradedObject

Definitions

Name	Category	Theorems
BifunctorComp₁₂IndexData 📖	CompData	—
BifunctorComp₂₃IndexData 📖	CompData	—
HasGoodTrifunctor₁₂Obj 📖	MathDef	—
HasGoodTrifunctor₂₃Obj 📖	MathDef	—
cofan₃MapBifunctorBifunctor₂₃MapObj 📖	CompOp	—
cofan₃MapBifunctor₁₂BifunctorMapObj 📖	CompOp	—
isColimitCofan₃MapBifunctorBifunctor₂₃MapObj 📖	CompOp	—
isColimitCofan₃MapBifunctor₁₂BifunctorMapObj 📖	CompOp	—
mapBifunctorBifunctor₂₃Desc 📖	CompOp	2 math math: ι_mapBifunctorBifunctor₂₃Desc, ι_mapBifunctorBifunctor₂₃Desc_assoc
mapBifunctorComp₁₂MapObjIso 📖	CompOp	4 math math: ι_mapBifunctorComp₁₂MapObjIso_hom_assoc, ι_mapBifunctorComp₁₂MapObjIso_inv, ι_mapBifunctorComp₁₂MapObjIso_hom, ι_mapBifunctorComp₁₂MapObjIso_inv_assoc
mapBifunctorComp₂₃MapObjIso 📖	CompOp	4 math math: ι_mapBifunctorComp₂₃MapObjIso_hom, ι_mapBifunctorComp₂₃MapObjIso_inv, ι_mapBifunctorComp₂₃MapObjIso_hom_assoc, ι_mapBifunctorComp₂₃MapObjIso_inv_assoc
mapBifunctor₁₂BifunctorDesc 📖	CompOp	2 math math: ι_mapBifunctor₁₂BifunctorDesc, ι_mapBifunctor₁₂BifunctorDesc_assoc
mapTrifunctor 📖	CompOp	7 math math: mapTrifunctor_map_app_app, mapTrifunctorMapIso_hom, HasGoodTrifunctor₁₂Obj.hasMap, HasGoodTrifunctor₂₃Obj.hasMap, mapTrifunctor_obj, mapTrifunctorMapNatTrans_app_app_app, mapTrifunctorMapIso_inv
mapTrifunctorMap 📖	CompOp	2 math math: mapTrifunctorMap_map_app_app, mapTrifunctorMap_obj
mapTrifunctorMapFunctorObj 📖	CompOp	5 math math: mapTrifunctorMapFunctorObj_obj_map, mapTrifunctorMapFunctorObj_map_app, mapTrifunctorMap_map_app_app, mapTrifunctorMapFunctorObj_obj_obj, mapTrifunctorMap_obj
mapTrifunctorMapIso 📖	CompOp	2 math math: mapTrifunctorMapIso_hom, mapTrifunctorMapIso_inv
mapTrifunctorMapMap 📖	CompOp	5 math math: mapTrifunctorMapFunctorObj_obj_map, mapTrifunctorMapFunctorObj_map_app, ι_mapTrifunctorMapMap_assoc, mapTrifunctorMap_map_app_app, ι_mapTrifunctorMapMap
mapTrifunctorMapNatTrans 📖	CompOp	3 math math: mapTrifunctorMapIso_hom, mapTrifunctorMapNatTrans_app_app_app, mapTrifunctorMapIso_inv
mapTrifunctorMapObj 📖	CompOp	13 math math: mapTrifunctorMapObj_ext_iff, ι_mapBifunctorComp₁₂MapObjIso_hom_assoc, mapTrifunctorMapFunctorObj_map_app, ι_mapTrifunctorMapMap_assoc, ι_mapBifunctorComp₂₃MapObjIso_hom, ι_mapBifunctorComp₁₂MapObjIso_inv, mapTrifunctorMapFunctorObj_obj_obj, ι_mapBifunctorComp₂₃MapObjIso_inv, ι_mapBifunctorComp₁₂MapObjIso_hom, ι_mapBifunctorComp₂₃MapObjIso_hom_assoc, ι_mapBifunctorComp₂₃MapObjIso_inv_assoc, ι_mapBifunctorComp₁₂MapObjIso_inv_assoc, ι_mapTrifunctorMapMap
mapTrifunctorObj 📖	CompOp	6 math math: mapTrifunctor_map_app_app, mapTrifunctorObj_obj_obj, mapTrifunctorObj_obj_map, mapTrifunctorObj_map_app, instHasMapProdObjFunctorMapTrifunctorObjOfMapTrifunctor, mapTrifunctor_obj
ιMapBifunctorBifunctor₂₃MapObj 📖	CompOp	13 math math: ιMapBifunctorBifunctor₂₃MapObj_eq_assoc, ι_mapBifunctorBifunctor₂₃Desc, ι_mapBifunctorComp₂₃MapObjIso_hom, ι_mapBifunctorAssociator_hom_assoc, ι_mapBifunctorAssociator_hom, ι_mapBifunctorBifunctor₂₃Desc_assoc, mapBifunctorBifunctor₂₃MapObj_ext_iff, ι_mapBifunctorComp₂₃MapObjIso_inv, ιMapBifunctorBifunctor₂₃MapObj_eq, ι_mapBifunctorAssociator_inv_assoc, ι_mapBifunctorAssociator_inv, ι_mapBifunctorComp₂₃MapObjIso_hom_assoc, ι_mapBifunctorComp₂₃MapObjIso_inv_assoc
ιMapBifunctor₁₂BifunctorMapObj 📖	CompOp	13 math math: ιMapBifunctor₁₂BifunctorMapObj_eq_assoc, ι_mapBifunctorComp₁₂MapObjIso_hom_assoc, ι_mapBifunctor₁₂BifunctorDesc, ι_mapBifunctorAssociator_hom_assoc, mapBifunctor₁₂BifunctorMapObj_ext_iff, ι_mapBifunctorComp₁₂MapObjIso_inv, ι_mapBifunctorAssociator_hom, ι_mapBifunctor₁₂BifunctorDesc_assoc, ιMapBifunctor₁₂BifunctorMapObj_eq, ι_mapBifunctorAssociator_inv_assoc, ι_mapBifunctorAssociator_inv, ι_mapBifunctorComp₁₂MapObjIso_hom, ι_mapBifunctorComp₁₂MapObjIso_inv_assoc
ιMapTrifunctorMapObj 📖	CompOp	11 math math: mapTrifunctorMapObj_ext_iff, ι_mapBifunctorComp₁₂MapObjIso_hom_assoc, ι_mapTrifunctorMapMap_assoc, ι_mapBifunctorComp₂₃MapObjIso_hom, ι_mapBifunctorComp₁₂MapObjIso_inv, ι_mapBifunctorComp₂₃MapObjIso_inv, ι_mapBifunctorComp₁₂MapObjIso_hom, ι_mapBifunctorComp₂₃MapObjIso_hom_assoc, ι_mapBifunctorComp₂₃MapObjIso_inv_assoc, ι_mapBifunctorComp₁₂MapObjIso_inv_assoc, ι_mapTrifunctorMapMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasMapProdObjFunctorMapTrifunctorObjOfMapTrifunctor 📖	mathematical	HasMap CategoryTheory.Functor.obj CategoryTheory.GradedObject categoryOfGradedObjects CategoryTheory.Functor CategoryTheory.Functor.category mapTrifunctor	mapTrifunctorObj	—	—
mapBifunctorBifunctor₂₃MapObj_ext 📖	—	HasMap BifunctorComp₂₃IndexData.I₂₃ CategoryTheory.Functor.obj CategoryTheory.GradedObject categoryOfGradedObjects CategoryTheory.Functor CategoryTheory.Functor.category mapBifunctor BifunctorComp₂₃IndexData.p mapBifunctorMapObj BifunctorComp₂₃IndexData.q HasGoodTrifunctor₂₃Obj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct ιMapBifunctorBifunctor₂₃MapObj	—	—	CategoryTheory.Limits.Cofan.IsColimit.hom_ext
mapBifunctorBifunctor₂₃MapObj_ext_iff 📖	mathematical	HasMap BifunctorComp₂₃IndexData.I₂₃ CategoryTheory.Functor.obj CategoryTheory.GradedObject categoryOfGradedObjects CategoryTheory.Functor CategoryTheory.Functor.category mapBifunctor BifunctorComp₂₃IndexData.p mapBifunctorMapObj BifunctorComp₂₃IndexData.q HasGoodTrifunctor₂₃Obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct ιMapBifunctorBifunctor₂₃MapObj	—	mapBifunctorBifunctor₂₃MapObj_ext
mapBifunctor₁₂BifunctorMapObj_ext 📖	—	HasMap BifunctorComp₁₂IndexData.I₁₂ CategoryTheory.Functor.obj CategoryTheory.GradedObject categoryOfGradedObjects CategoryTheory.Functor CategoryTheory.Functor.category mapBifunctor BifunctorComp₁₂IndexData.p mapBifunctorMapObj BifunctorComp₁₂IndexData.q HasGoodTrifunctor₁₂Obj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct ιMapBifunctor₁₂BifunctorMapObj	—	—	CategoryTheory.Limits.Cofan.IsColimit.hom_ext
mapBifunctor₁₂BifunctorMapObj_ext_iff 📖	mathematical	HasMap BifunctorComp₁₂IndexData.I₁₂ CategoryTheory.Functor.obj CategoryTheory.GradedObject categoryOfGradedObjects CategoryTheory.Functor CategoryTheory.Functor.category mapBifunctor BifunctorComp₁₂IndexData.p mapBifunctorMapObj BifunctorComp₁₂IndexData.q HasGoodTrifunctor₁₂Obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct ιMapBifunctor₁₂BifunctorMapObj	—	mapBifunctor₁₂BifunctorMapObj_ext
mapTrifunctorMapFunctorObj_map_app 📖	mathematical	HasMap CategoryTheory.Functor.obj CategoryTheory.GradedObject categoryOfGradedObjects CategoryTheory.Functor CategoryTheory.Functor.category mapTrifunctor	CategoryTheory.NatTrans.app mapTrifunctorMapObj mapTrifunctorMapMap CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map mapTrifunctorMapFunctorObj	—	—
mapTrifunctorMapFunctorObj_obj_map 📖	mathematical	HasMap CategoryTheory.Functor.obj CategoryTheory.GradedObject categoryOfGradedObjects CategoryTheory.Functor CategoryTheory.Functor.category mapTrifunctor	CategoryTheory.Functor.map mapTrifunctorMapFunctorObj mapTrifunctorMapMap CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
mapTrifunctorMapFunctorObj_obj_obj 📖	mathematical	HasMap CategoryTheory.Functor.obj CategoryTheory.GradedObject categoryOfGradedObjects CategoryTheory.Functor CategoryTheory.Functor.category mapTrifunctor	mapTrifunctorMapFunctorObj mapTrifunctorMapObj	—	—
mapTrifunctorMapIso_hom 📖	mathematical	—	CategoryTheory.Iso.hom CategoryTheory.Functor CategoryTheory.GradedObject categoryOfGradedObjects CategoryTheory.Functor.category mapTrifunctor mapTrifunctorMapIso mapTrifunctorMapNatTrans	—	—
mapTrifunctorMapIso_inv 📖	mathematical	—	CategoryTheory.Iso.inv CategoryTheory.Functor CategoryTheory.GradedObject categoryOfGradedObjects CategoryTheory.Functor.category mapTrifunctor mapTrifunctorMapIso mapTrifunctorMapNatTrans	—	—
mapTrifunctorMapNatTrans_app_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.GradedObject categoryOfGradedObjects CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category mapTrifunctor mapTrifunctorMapNatTrans	—	—
mapTrifunctorMapObj_ext 📖	—	HasMap CategoryTheory.Functor.obj CategoryTheory.GradedObject categoryOfGradedObjects CategoryTheory.Functor CategoryTheory.Functor.category mapTrifunctor CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct mapTrifunctorMapObj ιMapTrifunctorMapObj	—	—	mapObj_ext
mapTrifunctorMapObj_ext_iff 📖	mathematical	HasMap CategoryTheory.Functor.obj CategoryTheory.GradedObject categoryOfGradedObjects CategoryTheory.Functor CategoryTheory.Functor.category mapTrifunctor	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct mapTrifunctorMapObj ιMapTrifunctorMapObj	—	mapTrifunctorMapObj_ext
mapTrifunctorMap_map_app_app 📖	mathematical	HasMap CategoryTheory.Functor.obj CategoryTheory.GradedObject categoryOfGradedObjects CategoryTheory.Functor CategoryTheory.Functor.category mapTrifunctor	CategoryTheory.NatTrans.app mapTrifunctorMapFunctorObj CategoryTheory.Functor.map mapTrifunctorMap mapTrifunctorMapMap CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
mapTrifunctorMap_obj 📖	mathematical	HasMap CategoryTheory.Functor.obj CategoryTheory.GradedObject categoryOfGradedObjects CategoryTheory.Functor CategoryTheory.Functor.category mapTrifunctor	mapTrifunctorMap mapTrifunctorMapFunctorObj	—	—
mapTrifunctorObj_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.GradedObject categoryOfGradedObjects CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.map mapTrifunctorObj	—	—
mapTrifunctorObj_obj_map 📖	mathematical	—	CategoryTheory.Functor.map CategoryTheory.GradedObject categoryOfGradedObjects CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category mapTrifunctorObj	—	—
mapTrifunctorObj_obj_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.GradedObject categoryOfGradedObjects CategoryTheory.Functor CategoryTheory.Functor.category mapTrifunctorObj	—	—
mapTrifunctor_map_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.GradedObject categoryOfGradedObjects CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category mapTrifunctorObj CategoryTheory.Functor.map mapTrifunctor	—	—
mapTrifunctor_obj 📖	mathematical	—	CategoryTheory.Functor.obj CategoryTheory.GradedObject categoryOfGradedObjects CategoryTheory.Functor CategoryTheory.Functor.category mapTrifunctor mapTrifunctorObj	—	—
ιMapBifunctorBifunctor₂₃MapObj_eq 📖	mathematical	HasMap BifunctorComp₂₃IndexData.I₂₃ CategoryTheory.Functor.obj CategoryTheory.GradedObject categoryOfGradedObjects CategoryTheory.Functor CategoryTheory.Functor.category mapBifunctor BifunctorComp₂₃IndexData.p mapBifunctorMapObj BifunctorComp₂₃IndexData.q	ιMapBifunctorBifunctor₂₃MapObj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.map ιMapBifunctorMapObj	—	—
ιMapBifunctorBifunctor₂₃MapObj_eq_assoc 📖	mathematical	HasMap BifunctorComp₂₃IndexData.I₂₃ CategoryTheory.Functor.obj CategoryTheory.GradedObject categoryOfGradedObjects CategoryTheory.Functor CategoryTheory.Functor.category mapBifunctor BifunctorComp₂₃IndexData.p mapBifunctorMapObj BifunctorComp₂₃IndexData.q	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct ιMapBifunctorBifunctor₂₃MapObj CategoryTheory.Functor.map ιMapBifunctorMapObj	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ιMapBifunctorBifunctor₂₃MapObj_eq
ιMapBifunctor₁₂BifunctorMapObj_eq 📖	mathematical	HasMap BifunctorComp₁₂IndexData.I₁₂ CategoryTheory.Functor.obj CategoryTheory.GradedObject categoryOfGradedObjects CategoryTheory.Functor CategoryTheory.Functor.category mapBifunctor BifunctorComp₁₂IndexData.p mapBifunctorMapObj BifunctorComp₁₂IndexData.q	ιMapBifunctor₁₂BifunctorMapObj CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.NatTrans.app CategoryTheory.Functor.map ιMapBifunctorMapObj	—	—
ιMapBifunctor₁₂BifunctorMapObj_eq_assoc 📖	mathematical	HasMap BifunctorComp₁₂IndexData.I₁₂ CategoryTheory.Functor.obj CategoryTheory.GradedObject categoryOfGradedObjects CategoryTheory.Functor CategoryTheory.Functor.category mapBifunctor BifunctorComp₁₂IndexData.p mapBifunctorMapObj BifunctorComp₁₂IndexData.q	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct ιMapBifunctor₁₂BifunctorMapObj CategoryTheory.NatTrans.app CategoryTheory.Functor.map ιMapBifunctorMapObj	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ιMapBifunctor₁₂BifunctorMapObj_eq
ι_mapBifunctorBifunctor₂₃Desc 📖	mathematical	HasMap BifunctorComp₂₃IndexData.I₂₃ CategoryTheory.Functor.obj CategoryTheory.GradedObject categoryOfGradedObjects CategoryTheory.Functor CategoryTheory.Functor.category mapBifunctor BifunctorComp₂₃IndexData.p mapBifunctorMapObj BifunctorComp₂₃IndexData.q HasGoodTrifunctor₂₃Obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct ιMapBifunctorBifunctor₂₃MapObj mapBifunctorBifunctor₂₃Desc	—	CategoryTheory.Limits.Cofan.IsColimit.fac
ι_mapBifunctorBifunctor₂₃Desc_assoc 📖	mathematical	HasMap BifunctorComp₂₃IndexData.I₂₃ CategoryTheory.Functor.obj CategoryTheory.GradedObject categoryOfGradedObjects CategoryTheory.Functor CategoryTheory.Functor.category mapBifunctor BifunctorComp₂₃IndexData.p mapBifunctorMapObj BifunctorComp₂₃IndexData.q HasGoodTrifunctor₂₃Obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct ιMapBifunctorBifunctor₂₃MapObj mapBifunctorBifunctor₂₃Desc	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_mapBifunctorBifunctor₂₃Desc
ι_mapBifunctorComp₁₂MapObjIso_hom 📖	mathematical	HasMap BifunctorComp₁₂IndexData.I₁₂ CategoryTheory.Functor.obj CategoryTheory.GradedObject categoryOfGradedObjects CategoryTheory.Functor CategoryTheory.Functor.category mapBifunctor BifunctorComp₁₂IndexData.p mapBifunctorMapObj BifunctorComp₁₂IndexData.q HasGoodTrifunctor₁₂Obj mapTrifunctor CategoryTheory.bifunctorComp₁₂	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct mapTrifunctorMapObj ιMapTrifunctorMapObj CategoryTheory.Iso.hom mapBifunctorComp₁₂MapObjIso ιMapBifunctor₁₂BifunctorMapObj	—	CofanMapObjFun.ιMapObj_iso_inv
ι_mapBifunctorComp₁₂MapObjIso_hom_assoc 📖	mathematical	HasMap BifunctorComp₁₂IndexData.I₁₂ CategoryTheory.Functor.obj CategoryTheory.GradedObject categoryOfGradedObjects CategoryTheory.Functor CategoryTheory.Functor.category mapBifunctor BifunctorComp₁₂IndexData.p mapBifunctorMapObj BifunctorComp₁₂IndexData.q HasGoodTrifunctor₁₂Obj mapTrifunctor CategoryTheory.bifunctorComp₁₂	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct mapTrifunctorMapObj ιMapTrifunctorMapObj CategoryTheory.Iso.hom mapBifunctorComp₁₂MapObjIso ιMapBifunctor₁₂BifunctorMapObj	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_mapBifunctorComp₁₂MapObjIso_hom
ι_mapBifunctorComp₁₂MapObjIso_inv 📖	mathematical	HasMap BifunctorComp₁₂IndexData.I₁₂ CategoryTheory.Functor.obj CategoryTheory.GradedObject categoryOfGradedObjects CategoryTheory.Functor CategoryTheory.Functor.category mapBifunctor BifunctorComp₁₂IndexData.p mapBifunctorMapObj BifunctorComp₁₂IndexData.q HasGoodTrifunctor₁₂Obj mapTrifunctor CategoryTheory.bifunctorComp₁₂	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct mapTrifunctorMapObj ιMapBifunctor₁₂BifunctorMapObj CategoryTheory.Iso.inv mapBifunctorComp₁₂MapObjIso ιMapTrifunctorMapObj	—	CofanMapObjFun.inj_iso_hom
ι_mapBifunctorComp₁₂MapObjIso_inv_assoc 📖	mathematical	HasMap BifunctorComp₁₂IndexData.I₁₂ CategoryTheory.Functor.obj CategoryTheory.GradedObject categoryOfGradedObjects CategoryTheory.Functor CategoryTheory.Functor.category mapBifunctor BifunctorComp₁₂IndexData.p mapBifunctorMapObj BifunctorComp₁₂IndexData.q HasGoodTrifunctor₁₂Obj mapTrifunctor CategoryTheory.bifunctorComp₁₂	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct ιMapBifunctor₁₂BifunctorMapObj mapTrifunctorMapObj CategoryTheory.Iso.inv mapBifunctorComp₁₂MapObjIso ιMapTrifunctorMapObj	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_mapBifunctorComp₁₂MapObjIso_inv
ι_mapBifunctorComp₂₃MapObjIso_hom 📖	mathematical	HasMap BifunctorComp₂₃IndexData.I₂₃ CategoryTheory.Functor.obj CategoryTheory.GradedObject categoryOfGradedObjects CategoryTheory.Functor CategoryTheory.Functor.category mapBifunctor BifunctorComp₂₃IndexData.p mapBifunctorMapObj BifunctorComp₂₃IndexData.q HasGoodTrifunctor₂₃Obj mapTrifunctor CategoryTheory.bifunctorComp₂₃	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct mapTrifunctorMapObj ιMapTrifunctorMapObj CategoryTheory.Iso.hom mapBifunctorComp₂₃MapObjIso ιMapBifunctorBifunctor₂₃MapObj	—	CofanMapObjFun.ιMapObj_iso_inv
ι_mapBifunctorComp₂₃MapObjIso_hom_assoc 📖	mathematical	HasMap BifunctorComp₂₃IndexData.I₂₃ CategoryTheory.Functor.obj CategoryTheory.GradedObject categoryOfGradedObjects CategoryTheory.Functor CategoryTheory.Functor.category mapBifunctor BifunctorComp₂₃IndexData.p mapBifunctorMapObj BifunctorComp₂₃IndexData.q HasGoodTrifunctor₂₃Obj mapTrifunctor CategoryTheory.bifunctorComp₂₃	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct mapTrifunctorMapObj ιMapTrifunctorMapObj CategoryTheory.Iso.hom mapBifunctorComp₂₃MapObjIso ιMapBifunctorBifunctor₂₃MapObj	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_mapBifunctorComp₂₃MapObjIso_hom
ι_mapBifunctorComp₂₃MapObjIso_inv 📖	mathematical	HasMap BifunctorComp₂₃IndexData.I₂₃ CategoryTheory.Functor.obj CategoryTheory.GradedObject categoryOfGradedObjects CategoryTheory.Functor CategoryTheory.Functor.category mapBifunctor BifunctorComp₂₃IndexData.p mapBifunctorMapObj BifunctorComp₂₃IndexData.q HasGoodTrifunctor₂₃Obj mapTrifunctor CategoryTheory.bifunctorComp₂₃	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct mapTrifunctorMapObj ιMapBifunctorBifunctor₂₃MapObj CategoryTheory.Iso.inv mapBifunctorComp₂₃MapObjIso ιMapTrifunctorMapObj	—	CofanMapObjFun.inj_iso_hom
ι_mapBifunctorComp₂₃MapObjIso_inv_assoc 📖	mathematical	HasMap BifunctorComp₂₃IndexData.I₂₃ CategoryTheory.Functor.obj CategoryTheory.GradedObject categoryOfGradedObjects CategoryTheory.Functor CategoryTheory.Functor.category mapBifunctor BifunctorComp₂₃IndexData.p mapBifunctorMapObj BifunctorComp₂₃IndexData.q HasGoodTrifunctor₂₃Obj mapTrifunctor CategoryTheory.bifunctorComp₂₃	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct ιMapBifunctorBifunctor₂₃MapObj mapTrifunctorMapObj CategoryTheory.Iso.inv mapBifunctorComp₂₃MapObjIso ιMapTrifunctorMapObj	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_mapBifunctorComp₂₃MapObjIso_inv
ι_mapBifunctor₁₂BifunctorDesc 📖	mathematical	HasMap BifunctorComp₁₂IndexData.I₁₂ CategoryTheory.Functor.obj CategoryTheory.GradedObject categoryOfGradedObjects CategoryTheory.Functor CategoryTheory.Functor.category mapBifunctor BifunctorComp₁₂IndexData.p mapBifunctorMapObj BifunctorComp₁₂IndexData.q HasGoodTrifunctor₁₂Obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct ιMapBifunctor₁₂BifunctorMapObj mapBifunctor₁₂BifunctorDesc	—	CategoryTheory.Limits.Cofan.IsColimit.fac
ι_mapBifunctor₁₂BifunctorDesc_assoc 📖	mathematical	HasMap BifunctorComp₁₂IndexData.I₁₂ CategoryTheory.Functor.obj CategoryTheory.GradedObject categoryOfGradedObjects CategoryTheory.Functor CategoryTheory.Functor.category mapBifunctor BifunctorComp₁₂IndexData.p mapBifunctorMapObj BifunctorComp₁₂IndexData.q HasGoodTrifunctor₁₂Obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct ιMapBifunctor₁₂BifunctorMapObj mapBifunctor₁₂BifunctorDesc	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_mapBifunctor₁₂BifunctorDesc
ι_mapTrifunctorMapMap 📖	mathematical	HasMap CategoryTheory.Functor.obj CategoryTheory.GradedObject categoryOfGradedObjects CategoryTheory.Functor CategoryTheory.Functor.category mapTrifunctor	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct mapTrifunctorMapObj ιMapTrifunctorMapObj mapTrifunctorMapMap CategoryTheory.NatTrans.app CategoryTheory.Functor.map	—	ι_mapMap CategoryTheory.Category.assoc
ι_mapTrifunctorMapMap_assoc 📖	mathematical	HasMap CategoryTheory.Functor.obj CategoryTheory.GradedObject categoryOfGradedObjects CategoryTheory.Functor CategoryTheory.Functor.category mapTrifunctor	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct mapTrifunctorMapObj ιMapTrifunctorMapObj mapTrifunctorMapMap CategoryTheory.NatTrans.app CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_mapTrifunctorMapMap

CategoryTheory.GradedObject.BifunctorComp₁₂IndexData

Definitions

Name	Category	Theorems
I₁₂ 📖	CompOp	2 math math: CategoryTheory.GradedObject.mapBifunctor_triangle, hpq
p 📖	CompOp	2 math math: CategoryTheory.GradedObject.mapBifunctor_triangle, hpq
q 📖	CompOp	2 math math: CategoryTheory.GradedObject.mapBifunctor_triangle, hpq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hpq 📖	mathematical	—	q I₁₂ p	—	—

CategoryTheory.GradedObject.BifunctorComp₂₃IndexData

Definitions

Name	Category	Theorems
I₂₃ 📖	CompOp	2 math math: CategoryTheory.GradedObject.mapBifunctor_triangle, hpq
p 📖	CompOp	2 math math: CategoryTheory.GradedObject.mapBifunctor_triangle, hpq
q 📖	CompOp	2 math math: CategoryTheory.GradedObject.mapBifunctor_triangle, hpq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hpq 📖	mathematical	—	q I₂₃ p	—	—

CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasMap 📖	mathematical	CategoryTheory.GradedObject.HasMap CategoryTheory.GradedObject.BifunctorComp₁₂IndexData.I₁₂ CategoryTheory.Functor.obj CategoryTheory.GradedObject CategoryTheory.GradedObject.categoryOfGradedObjects CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.GradedObject.mapBifunctor CategoryTheory.GradedObject.BifunctorComp₁₂IndexData.p CategoryTheory.GradedObject.mapBifunctorMapObj CategoryTheory.GradedObject.BifunctorComp₁₂IndexData.q CategoryTheory.GradedObject.HasGoodTrifunctor₁₂Obj	CategoryTheory.GradedObject.mapTrifunctor CategoryTheory.bifunctorComp₁₂	—	—

CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasMap 📖	mathematical	CategoryTheory.GradedObject.HasMap CategoryTheory.GradedObject.BifunctorComp₂₃IndexData.I₂₃ CategoryTheory.Functor.obj CategoryTheory.GradedObject CategoryTheory.GradedObject.categoryOfGradedObjects CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.GradedObject.mapBifunctor CategoryTheory.GradedObject.BifunctorComp₂₃IndexData.p CategoryTheory.GradedObject.mapBifunctorMapObj CategoryTheory.GradedObject.BifunctorComp₂₃IndexData.q CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj	CategoryTheory.GradedObject.mapTrifunctor CategoryTheory.bifunctorComp₂₃	—	—

---

← Back to Index