CurryingThree

📁 Source: Mathlib/CategoryTheory/Functor/CurryingThree.lean

Statistics

Metric	Count
Definitions bifunctorComp₁₂Iso, bifunctorComp₂₃Iso, currying₃, curry₃, curry₃ObjProdComp, flip₁₃, flip₁₃Functor, flip₂₃, flip₂₃Functor, fullyFaithfulCurry₃, fullyFaithfulUncurry₃, uncurry₃	12
Theorems bifunctorComp₁₂Iso_hom_app_app_app, bifunctorComp₁₂Iso_inv_app_app_app, bifunctorComp₂₃Iso_hom_app_app_app, bifunctorComp₂₃Iso_inv_app_app_app, currying₃_unitIso_hom_app_app_app_app, currying₃_unitIso_inv_app_app_app_app, curry₃ObjProdComp_hom_app_app_app, curry₃ObjProdComp_inv_app_app_app, curry₃_map_app_app_app, curry₃_obj_map_app_app, curry₃_obj_obj_map_app, curry₃_obj_obj_obj_map, flip₁₃Functor_map_app_app_app, flip₁₃Functor_obj_map_app_app, flip₁₃Functor_obj_obj_map_app, flip₁₃Functor_obj_obj_obj_map, flip₁₃Functor_obj_obj_obj_obj, flip₁₃_map_app_app, flip₁₃_obj_map_app, flip₁₃_obj_obj_map, flip₁₃_obj_obj_obj, flip₂₃Functor_map_app_app_app, flip₂₃Functor_obj_map_app_app, flip₂₃Functor_obj_obj_map_app, flip₂₃Functor_obj_obj_obj_map, flip₂₃Functor_obj_obj_obj_obj, flip₂₃_map_app_app, flip₂₃_obj_map_app, flip₂₃_obj_obj_map, flip₂₃_obj_obj_obj, instFaithfulProdCurry₃, instFaithfulProdUncurry₃, instFullProdCurry₃, instFullProdUncurry₃	34
Total	46

CategoryTheory.Functor

Definitions

Name	Category	Theorems
bifunctorComp₁₂Iso 📖	CompOp	2 math math: bifunctorComp₁₂Iso_inv_app_app_app, bifunctorComp₁₂Iso_hom_app_app_app
bifunctorComp₂₃Iso 📖	CompOp	2 math math: bifunctorComp₂₃Iso_hom_app_app_app, bifunctorComp₂₃Iso_inv_app_app_app
currying₃ 📖	CompOp	2 math math: currying₃_unitIso_hom_app_app_app_app, currying₃_unitIso_inv_app_app_app_app
curry₃ 📖	CompOp	8 math math: curry₃_obj_obj_map_app, curry₃ObjProdComp_inv_app_app_app, instFullProdCurry₃, curry₃_obj_map_app_app, curry₃ObjProdComp_hom_app_app_app, curry₃_obj_obj_obj_map, curry₃_map_app_app_app, instFaithfulProdCurry₃
curry₃ObjProdComp 📖	CompOp	2 math math: curry₃ObjProdComp_inv_app_app_app, curry₃ObjProdComp_hom_app_app_app
flip₁₃ 📖	CompOp	6 math math: flip₁₃_map_app_app, CategoryTheory.BraidedCategory.ofBifunctor.Forward.secondMap₃_app_app_app, flip₁₃_obj_map_app, flip₁₃_obj_obj_map, flip₁₃_obj_obj_obj, flip₁₃Functor_map_app_app_app
flip₁₃Functor 📖	CompOp	5 math math: flip₁₃Functor_obj_obj_obj_obj, flip₁₃Functor_obj_map_app_app, flip₁₃Functor_obj_obj_map_app, flip₁₃Functor_map_app_app_app, flip₁₃Functor_obj_obj_obj_map
flip₂₃ 📖	CompOp	8 math math: flip₂₃_obj_obj_map, flip₂₃_obj_obj_obj, CategoryTheory.BraidedCategory.ofBifunctor.Reverse.firstMap₂_app_app_app, flip₂₃Functor_map_app_app_app, CategoryTheory.BraidedCategory.ofBifunctor.Reverse.secondMap₃_app_app_app, flip₂₃_obj_map_app, flip₂₃_map_app_app, CategoryTheory.BraidedCategory.ofBifunctor.Reverse.firstMap₃_app_app_app
flip₂₃Functor 📖	CompOp	5 math math: flip₂₃Functor_obj_obj_obj_obj, flip₂₃Functor_obj_obj_obj_map, flip₂₃Functor_obj_obj_map_app, flip₂₃Functor_map_app_app_app, flip₂₃Functor_obj_map_app_app
fullyFaithfulCurry₃ 📖	CompOp	—
fullyFaithfulUncurry₃ 📖	CompOp	—
uncurry₃ 📖	CompOp	2 math math: instFaithfulProdUncurry₃, instFullProdUncurry₃

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bifunctorComp₁₂Iso_hom_app_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor category CategoryTheory.bifunctorComp₁₂ CategoryTheory.prod' curry comp uncurry CategoryTheory.Iso.hom bifunctorComp₁₂Iso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
bifunctorComp₁₂Iso_inv_app_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor category CategoryTheory.prod' curry comp uncurry CategoryTheory.bifunctorComp₁₂ CategoryTheory.Iso.inv bifunctorComp₁₂Iso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
bifunctorComp₂₃Iso_hom_app_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor category CategoryTheory.bifunctorComp₂₃ CategoryTheory.prod' curry comp CategoryTheory.prod.associator uncurry flip CategoryTheory.Iso.hom bifunctorComp₂₃Iso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
bifunctorComp₂₃Iso_inv_app_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor category CategoryTheory.prod' curry comp CategoryTheory.prod.associator uncurry flip CategoryTheory.bifunctorComp₂₃ CategoryTheory.Iso.inv bifunctorComp₂₃Iso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
currying₃_unitIso_hom_app_app_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor category id comp CategoryTheory.prod' CategoryTheory.Equivalence.functor currying₃ CategoryTheory.Equivalence.inverse CategoryTheory.Iso.hom CategoryTheory.Equivalence.unitIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	isoWhiskerRight_trans CategoryTheory.Iso.trans_assoc map_id CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Equivalence.funInvIdAssoc_inv_app
currying₃_unitIso_inv_app_app_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor category comp CategoryTheory.prod' CategoryTheory.Equivalence.functor currying₃ CategoryTheory.Equivalence.inverse id CategoryTheory.Iso.inv CategoryTheory.Equivalence.unitIso CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	isoWhiskerRight_trans CategoryTheory.Iso.trans_assoc CategoryTheory.Category.assoc map_id CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id CategoryTheory.Equivalence.funInvIdAssoc_hom_app
curry₃ObjProdComp_hom_app_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor category CategoryTheory.prod' curry₃ comp prod whiskeringLeft₂ CategoryTheory.Iso.hom curry₃ObjProdComp CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
curry₃ObjProdComp_inv_app_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor category comp CategoryTheory.prod' curry₃ whiskeringLeft₂ prod CategoryTheory.Iso.inv curry₃ObjProdComp CategoryTheory.CategoryStruct.id CategoryTheory.Category.toCategoryStruct	—	—
curry₃_map_app_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor category CategoryTheory.prod' curry₃ map	—	—
curry₃_obj_map_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor category CategoryTheory.prod' curry₃ map CategoryTheory.Equivalence.functor CategoryTheory.prod.associativity Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	—	—
curry₃_obj_obj_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor category CategoryTheory.prod' curry₃ map CategoryTheory.Equivalence.functor CategoryTheory.prod.associativity Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	—	—
curry₃_obj_obj_obj_map 📖	mathematical	—	map obj CategoryTheory.Functor category CategoryTheory.prod' curry₃ CategoryTheory.Equivalence.functor CategoryTheory.prod.associativity Quiver.Hom CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.CategoryStruct.id	—	—
flip₁₃Functor_map_app_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor category flip₁₃ map flip₁₃Functor	—	—
flip₁₃Functor_obj_map_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor category map flip₁₃Functor	—	—
flip₁₃Functor_obj_obj_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor category map flip₁₃Functor	—	—
flip₁₃Functor_obj_obj_obj_map 📖	mathematical	—	map obj CategoryTheory.Functor category flip₁₃Functor CategoryTheory.NatTrans.app	—	—
flip₁₃Functor_obj_obj_obj_obj 📖	mathematical	—	obj CategoryTheory.Functor category flip₁₃Functor	—	—
flip₁₃_map_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor category map flip₁₃	—	—
flip₁₃_obj_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor category map flip₁₃	—	—
flip₁₃_obj_obj_map 📖	mathematical	—	map obj CategoryTheory.Functor category flip₁₃ CategoryTheory.NatTrans.app	—	—
flip₁₃_obj_obj_obj 📖	mathematical	—	obj CategoryTheory.Functor category flip₁₃	—	—
flip₂₃Functor_map_app_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor category flip₂₃ map flip₂₃Functor	—	—
flip₂₃Functor_obj_map_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor category flip CategoryTheory.flipFunctor map flip₂₃Functor	—	—
flip₂₃Functor_obj_obj_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor category map flip₂₃Functor	—	—
flip₂₃Functor_obj_obj_obj_map 📖	mathematical	—	map obj CategoryTheory.Functor category flip₂₃Functor CategoryTheory.NatTrans.app	—	—
flip₂₃Functor_obj_obj_obj_obj 📖	mathematical	—	obj CategoryTheory.Functor category flip₂₃Functor	—	—
flip₂₃_map_app_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor category flip CategoryTheory.flipFunctor map flip₂₃	—	—
flip₂₃_obj_map_app 📖	mathematical	—	CategoryTheory.NatTrans.app obj CategoryTheory.Functor category map flip₂₃	—	—
flip₂₃_obj_obj_map 📖	mathematical	—	map obj CategoryTheory.Functor category flip₂₃ CategoryTheory.NatTrans.app	—	—
flip₂₃_obj_obj_obj 📖	mathematical	—	obj CategoryTheory.Functor category flip₂₃	—	—
instFaithfulProdCurry₃ 📖	mathematical	—	Faithful CategoryTheory.Functor CategoryTheory.prod' category curry₃	—	FullyFaithful.faithful
instFaithfulProdUncurry₃ 📖	mathematical	—	Faithful CategoryTheory.Functor category CategoryTheory.prod' uncurry₃	—	FullyFaithful.faithful
instFullProdCurry₃ 📖	mathematical	—	Full CategoryTheory.Functor CategoryTheory.prod' category curry₃	—	FullyFaithful.full
instFullProdUncurry₃ 📖	mathematical	—	Full CategoryTheory.Functor category CategoryTheory.prod' uncurry₃	—	FullyFaithful.full

---

← Back to Index