Commit 2025-01-02 12:06 4e190ae6

View on Github →

feat(CategoryTheory): whiskering and curryfication of functors in three variables (#20197)

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/Functor/CurryingThree.lean

added def CategoryTheory.bifunctorComp₁₂Iso

added def CategoryTheory.bifunctorComp₂₃Iso

added def CategoryTheory.currying₃

added theorem CategoryTheory.currying₃_unitIso_hom_app_app_app_app

added theorem CategoryTheory.currying₃_unitIso_inv_app_app_app_app

added def CategoryTheory.curry₃ObjProdComp

added theorem CategoryTheory.curry₃_map_app_app_app

added theorem CategoryTheory.curry₃_obj_map_app_app

added theorem CategoryTheory.curry₃_obj_obj_map_app

added theorem CategoryTheory.curry₃_obj_obj_obj_map

added def CategoryTheory.fullyFaithfulUncurry₃

Modified Mathlib/CategoryTheory/Functor/Trifunctor.lean

modified def CategoryTheory.bifunctorComp₁₂

added def CategoryTheory.bifunctorComp₁₂Functor

added def CategoryTheory.bifunctorComp₁₂FunctorMap

added def CategoryTheory.bifunctorComp₁₂FunctorObj

modified def CategoryTheory.bifunctorComp₁₂Obj

modified def CategoryTheory.bifunctorComp₂₃

added def CategoryTheory.bifunctorComp₂₃Functor

added def CategoryTheory.bifunctorComp₂₃FunctorMap

added def CategoryTheory.bifunctorComp₂₃FunctorObj

modified def CategoryTheory.bifunctorComp₂₃Obj

Modified Mathlib/CategoryTheory/NatIso.lean

added theorem CategoryTheory.Iso.hom_inv_id_app_app_app

added theorem CategoryTheory.Iso.inv_hom_id_app_app_app

Modified Mathlib/CategoryTheory/Whiskering.lean

added def CategoryTheory.Functor.postcompose₃

added def CategoryTheory.whiskeringLeft₃

added def CategoryTheory.whiskeringLeft₃Map

added def CategoryTheory.whiskeringLeft₃Obj

added def CategoryTheory.whiskeringLeft₃ObjMap

added def CategoryTheory.whiskeringLeft₃ObjObj

added def CategoryTheory.whiskeringLeft₃ObjObjMap

added def CategoryTheory.whiskeringLeft₃ObjObjObj