Associator

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

Statistics

Metric	Count
Definitions mapBifunctorAssociator	1
Theorems ι_mapBifunctorAssociator_hom, ι_mapBifunctorAssociator_hom_assoc, ι_mapBifunctorAssociator_inv, ι_mapBifunctorAssociator_inv_assoc	4
Total	5

CategoryTheory.GradedObject

Definitions

Name	Category	Theorems
mapBifunctorAssociator 📖	CompOp	5 math math: mapBifunctor_triangle, ι_mapBifunctorAssociator_hom_assoc, ι_mapBifunctorAssociator_hom, ι_mapBifunctorAssociator_inv_assoc, ι_mapBifunctorAssociator_inv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ι_mapBifunctorAssociator_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 BifunctorComp₂₃IndexData.I₂₃ BifunctorComp₂₃IndexData.p BifunctorComp₂₃IndexData.q HasGoodTrifunctor₁₂Obj HasGoodTrifunctor₂₃Obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct ιMapBifunctor₁₂BifunctorMapObj CategoryTheory.Iso.hom mapBifunctorAssociator CategoryTheory.bifunctorComp₁₂ CategoryTheory.bifunctorComp₂₃ CategoryTheory.NatTrans.app ιMapBifunctorBifunctor₂₃MapObj	—	HasGoodTrifunctor₁₂Obj.hasMap HasGoodTrifunctor₂₃Obj.hasMap ι_mapBifunctorComp₁₂MapObjIso_inv_assoc ιMapTrifunctorMapObj.eq_1 ι_mapMap_assoc mapTrifunctorMapNatTrans_app_app_app ι_mapBifunctorComp₂₃MapObjIso_hom
ι_mapBifunctorAssociator_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 BifunctorComp₂₃IndexData.I₂₃ BifunctorComp₂₃IndexData.p BifunctorComp₂₃IndexData.q HasGoodTrifunctor₁₂Obj HasGoodTrifunctor₂₃Obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct ιMapBifunctor₁₂BifunctorMapObj CategoryTheory.Iso.hom mapBifunctorAssociator CategoryTheory.bifunctorComp₂₃ CategoryTheory.NatTrans.app CategoryTheory.bifunctorComp₁₂ ιMapBifunctorBifunctor₂₃MapObj	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_mapBifunctorAssociator_hom
ι_mapBifunctorAssociator_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 BifunctorComp₂₃IndexData.I₂₃ BifunctorComp₂₃IndexData.p BifunctorComp₂₃IndexData.q HasGoodTrifunctor₁₂Obj HasGoodTrifunctor₂₃Obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct ιMapBifunctorBifunctor₂₃MapObj CategoryTheory.Iso.inv mapBifunctorAssociator CategoryTheory.bifunctorComp₂₃ CategoryTheory.bifunctorComp₁₂ CategoryTheory.NatTrans.app ιMapBifunctor₁₂BifunctorMapObj	—	CategoryTheory.cancel_mono CategoryTheory.mono_of_strongMono CategoryTheory.strongMono_of_isIso isIso_apply_of_isIso CategoryTheory.Iso.isIso_hom CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id_eval CategoryTheory.Category.comp_id ι_mapBifunctorAssociator_hom CategoryTheory.NatTrans.comp_app_assoc CategoryTheory.NatTrans.comp_app CategoryTheory.Iso.inv_hom_id_app CategoryTheory.NatTrans.id_app CategoryTheory.Category.id_comp
ι_mapBifunctorAssociator_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 BifunctorComp₂₃IndexData.I₂₃ BifunctorComp₂₃IndexData.p BifunctorComp₂₃IndexData.q HasGoodTrifunctor₁₂Obj HasGoodTrifunctor₂₃Obj	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct ιMapBifunctorBifunctor₂₃MapObj CategoryTheory.Iso.inv mapBifunctorAssociator CategoryTheory.bifunctorComp₁₂ CategoryTheory.NatTrans.app CategoryTheory.bifunctorComp₂₃ ιMapBifunctor₁₂BifunctorMapObj	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_mapBifunctorAssociator_inv

---

← Back to Index