Bifunctor

📁 Source: Mathlib/CategoryTheory/Limits/Preserves/Bifunctor.lean

Statistics

Metric	Count
Definitions mapCocone₂, mapCone₂, PreservesColimit₂, isoColimitUncurryWhiskeringLeft₂, isoObjCoconePointsOfIsColimit, PreservesLimit₂, isoLimitUncurryWhiskeringLeft₂, isoObjConePointsOfIsLimit, isColimitOfPreserves₂, isLimitOfPreserves₂	10
Theorems mapCocone₂_pt, mapCocone₂_ι_app, mapCone₂_pt, mapCone₂_π_app, map_ι_comp_isoColimitUncurryWhiskeringLeft₂_inv, map_ι_comp_isoColimitUncurryWhiskeringLeft₂_inv_assoc, map_ι_comp_isoObjConePointsOfIsColimit_hom, map_ι_comp_isoObjConePointsOfIsColimit_hom_assoc, nonempty_isColimit_mapCocone₂, of_preservesColimits_in_each_variable, of_preservesColimit₂_flip, ι_comp_isoColimitUncurryWhiskeringLeft₂_hom, ι_comp_isoColimitUncurryWhiskeringLeft₂_hom_assoc, ι_comp_isoObjConePointsOfIsColimit_inv, ι_comp_isoObjConePointsOfIsColimit_inv_assoc, isoLimitUncurryWhiskeringLeft₂_hom_comp_map_π, isoLimitUncurryWhiskeringLeft₂_hom_comp_map_π_assoc, isoLimitUncurryWhiskeringLeft₂_inv_comp_π, isoLimitUncurryWhiskeringLeft₂_inv_comp_π_assoc, isoObjConePointsOfIsColimit_inv_comp_map_π, isoObjConePointsOfIsColimit_inv_comp_map_π_assoc, isoObjConePointsOfIsLimit_hom_comp_π, isoObjConePointsOfIsLimit_hom_comp_π_assoc, nonempty_isLimit_mapCone₂, of_preservesLimits_in_each_variable, of_preservesLimit₂_flip, instHasColimitProdObjFunctorUncurryWhiskeringLeft₂OfPreservesColimit₂, instHasLimitProdObjFunctorUncurryWhiskeringLeft₂OfPreservesLimit₂	28
Total	38

CategoryTheory.Functor

Definitions

Name	Category	Theorems
mapCocone₂ 📖	CompOp	3 math math: mapCocone₂_pt, mapCocone₂_ι_app, CategoryTheory.Limits.PreservesColimit₂.nonempty_isColimit_mapCocone₂
mapCone₂ 📖	CompOp	3 math math: mapCone₂_pt, CategoryTheory.Limits.PreservesLimit₂.nonempty_isLimit_mapCone₂, mapCone₂_π_app

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mapCocone₂_pt 📖	mathematical	—	CategoryTheory.Limits.Cocone.pt CategoryTheory.prod' obj CategoryTheory.Functor category uncurry whiskeringLeft₂ mapCocone₂	—	—
mapCocone₂_ι_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.prod' obj CategoryTheory.Functor category uncurry whiskeringLeft₂ const CategoryTheory.Limits.Cocone.pt CategoryTheory.Limits.Cocone.ι mapCocone₂ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct map	—	—
mapCone₂_pt 📖	mathematical	—	CategoryTheory.Limits.Cone.pt CategoryTheory.prod' obj CategoryTheory.Functor category uncurry whiskeringLeft₂ mapCone₂	—	—
mapCone₂_π_app 📖	mathematical	—	CategoryTheory.NatTrans.app CategoryTheory.prod' obj CategoryTheory.Functor category const CategoryTheory.Limits.Cone.pt uncurry whiskeringLeft₂ CategoryTheory.Limits.Cone.π mapCone₂ CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct map	—	—

CategoryTheory.Limits

Definitions

Name	Category	Theorems
PreservesColimit₂ 📖	CompData	2 math math: PreservesColimit₂.of_preservesColimits_in_each_variable, PreservesColimit₂.of_preservesColimit₂_flip
PreservesLimit₂ 📖	CompData	2 math math: PreservesLimit₂.of_preservesLimit₂_flip, PreservesLimit₂.of_preservesLimits_in_each_variable
isColimitOfPreserves₂ 📖	CompOp	—
isLimitOfPreserves₂ 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instHasColimitProdObjFunctorUncurryWhiskeringLeft₂OfPreservesColimit₂ 📖	mathematical	—	HasColimit CategoryTheory.prod' CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.uncurry CategoryTheory.Functor.whiskeringLeft₂	—	PreservesColimit₂.nonempty_isColimit_mapCocone₂
instHasLimitProdObjFunctorUncurryWhiskeringLeft₂OfPreservesLimit₂ 📖	mathematical	—	HasLimit CategoryTheory.prod' CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.uncurry CategoryTheory.Functor.whiskeringLeft₂	—	PreservesLimit₂.nonempty_isLimit_mapCone₂

CategoryTheory.Limits.PreservesColimit₂

Definitions

Name	Category	Theorems
isoColimitUncurryWhiskeringLeft₂ 📖	CompOp	5 math math: CategoryTheory.IsSifted.factorization_prodComparison_colim, map_ι_comp_isoColimitUncurryWhiskeringLeft₂_inv_assoc, map_ι_comp_isoColimitUncurryWhiskeringLeft₂_inv, ι_comp_isoColimitUncurryWhiskeringLeft₂_hom_assoc, ι_comp_isoColimitUncurryWhiskeringLeft₂_hom
isoObjCoconePointsOfIsColimit 📖	CompOp	4 math math: map_ι_comp_isoObjConePointsOfIsColimit_hom, map_ι_comp_isoObjConePointsOfIsColimit_hom_assoc, ι_comp_isoObjConePointsOfIsColimit_inv, ι_comp_isoObjConePointsOfIsColimit_inv_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_ι_comp_isoColimitUncurryWhiskeringLeft₂_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.colimit CategoryTheory.prod' CategoryTheory.Functor.uncurry CategoryTheory.Functor.whiskeringLeft₂ CategoryTheory.Limits.instHasColimitProdObjFunctorUncurryWhiskeringLeft₂OfPreservesColimit₂ CategoryTheory.NatTrans.app CategoryTheory.Functor.map CategoryTheory.Limits.colimit.ι CategoryTheory.Iso.inv isoColimitUncurryWhiskeringLeft₂	—	map_ι_comp_isoObjConePointsOfIsColimit_hom CategoryTheory.Limits.instHasColimitProdObjFunctorUncurryWhiskeringLeft₂OfPreservesColimit₂
map_ι_comp_isoColimitUncurryWhiskeringLeft₂_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.colimit CategoryTheory.NatTrans.app CategoryTheory.Functor.map CategoryTheory.Limits.colimit.ι CategoryTheory.prod' CategoryTheory.Functor.uncurry CategoryTheory.Functor.whiskeringLeft₂ CategoryTheory.Limits.instHasColimitProdObjFunctorUncurryWhiskeringLeft₂OfPreservesColimit₂ CategoryTheory.Iso.inv isoColimitUncurryWhiskeringLeft₂	—	CategoryTheory.Limits.instHasColimitProdObjFunctorUncurryWhiskeringLeft₂OfPreservesColimit₂ CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_ι_comp_isoColimitUncurryWhiskeringLeft₂_inv
map_ι_comp_isoObjConePointsOfIsColimit_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.prod' CategoryTheory.Functor.uncurry CategoryTheory.Functor.whiskeringLeft₂ CategoryTheory.NatTrans.app CategoryTheory.Functor.map CategoryTheory.Limits.Cocone.ι CategoryTheory.Iso.hom isoObjCoconePointsOfIsColimit	—	CategoryTheory.Category.assoc CategoryTheory.Iso.eq_comp_inv ι_comp_isoObjConePointsOfIsColimit_inv
map_ι_comp_isoObjConePointsOfIsColimit_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Functor.map CategoryTheory.Limits.Cocone.ι CategoryTheory.prod' CategoryTheory.Functor.uncurry CategoryTheory.Functor.whiskeringLeft₂ CategoryTheory.Iso.hom isoObjCoconePointsOfIsColimit	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' map_ι_comp_isoObjConePointsOfIsColimit_hom
nonempty_isColimit_mapCocone₂ 📖	mathematical	—	CategoryTheory.Limits.IsColimit CategoryTheory.prod' CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.uncurry CategoryTheory.Functor.whiskeringLeft₂ CategoryTheory.Functor.mapCocone₂	—	—
of_preservesColimits_in_each_variable 📖	mathematical	CategoryTheory.Limits.PreservesColimit CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.flip	CategoryTheory.Limits.PreservesColimit₂	—	CategoryTheory.NatTrans.naturality CategoryTheory.Functor.map_id CategoryTheory.Functor.map_comp CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Limits.IsColimit.hom_ext CategoryTheory.Limits.IsColimit.fac
of_preservesColimit₂_flip 📖	mathematical	—	CategoryTheory.Limits.PreservesColimit₂ CategoryTheory.Functor.flip	—	CategoryTheory.Category.id_comp CategoryTheory.Category.comp_id CategoryTheory.Category.assoc CategoryTheory.NatTrans.naturality
ι_comp_isoColimitUncurryWhiskeringLeft₂_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.prod' CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.uncurry CategoryTheory.Functor.whiskeringLeft₂ CategoryTheory.Limits.colimit CategoryTheory.Limits.instHasColimitProdObjFunctorUncurryWhiskeringLeft₂OfPreservesColimit₂ CategoryTheory.Limits.colimit.ι CategoryTheory.Iso.hom isoColimitUncurryWhiskeringLeft₂ CategoryTheory.NatTrans.app CategoryTheory.Functor.map	—	ι_comp_isoObjConePointsOfIsColimit_inv CategoryTheory.Limits.instHasColimitProdObjFunctorUncurryWhiskeringLeft₂OfPreservesColimit₂
ι_comp_isoColimitUncurryWhiskeringLeft₂_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.prod' CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.uncurry CategoryTheory.Functor.whiskeringLeft₂ CategoryTheory.Limits.colimit CategoryTheory.Limits.instHasColimitProdObjFunctorUncurryWhiskeringLeft₂OfPreservesColimit₂ CategoryTheory.Limits.colimit.ι CategoryTheory.Iso.hom isoColimitUncurryWhiskeringLeft₂ CategoryTheory.NatTrans.app CategoryTheory.Functor.map	—	CategoryTheory.Limits.instHasColimitProdObjFunctorUncurryWhiskeringLeft₂OfPreservesColimit₂ CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_comp_isoColimitUncurryWhiskeringLeft₂_hom
ι_comp_isoObjConePointsOfIsColimit_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.prod' CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.uncurry CategoryTheory.Functor.whiskeringLeft₂ CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι CategoryTheory.Iso.inv isoObjCoconePointsOfIsColimit CategoryTheory.Functor.map	—	CategoryTheory.Limits.IsColimit.comp_coconePointUniqueUpToIso_inv
ι_comp_isoObjConePointsOfIsColimit_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.prod' CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.uncurry CategoryTheory.Functor.whiskeringLeft₂ CategoryTheory.Functor.const CategoryTheory.Limits.Cocone.pt CategoryTheory.NatTrans.app CategoryTheory.Limits.Cocone.ι CategoryTheory.Iso.inv isoObjCoconePointsOfIsColimit CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_comp_isoObjConePointsOfIsColimit_inv

CategoryTheory.Limits.PreservesLimit₂

Definitions

Name	Category	Theorems
isoLimitUncurryWhiskeringLeft₂ 📖	CompOp	4 math math: isoLimitUncurryWhiskeringLeft₂_inv_comp_π, isoLimitUncurryWhiskeringLeft₂_inv_comp_π_assoc, isoLimitUncurryWhiskeringLeft₂_hom_comp_map_π, isoLimitUncurryWhiskeringLeft₂_hom_comp_map_π_assoc
isoObjConePointsOfIsLimit 📖	CompOp	4 math math: isoObjConePointsOfIsColimit_inv_comp_map_π, isoObjConePointsOfIsLimit_hom_comp_π, isoObjConePointsOfIsColimit_inv_comp_map_π_assoc, isoObjConePointsOfIsLimit_hom_comp_π_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isoLimitUncurryWhiskeringLeft₂_hom_comp_map_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.limit CategoryTheory.prod' CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.uncurry CategoryTheory.Functor.whiskeringLeft₂ CategoryTheory.Limits.instHasLimitProdObjFunctorUncurryWhiskeringLeft₂OfPreservesLimit₂ CategoryTheory.Iso.hom isoLimitUncurryWhiskeringLeft₂ CategoryTheory.NatTrans.app CategoryTheory.Functor.map CategoryTheory.Limits.limit.π	—	isoObjConePointsOfIsColimit_inv_comp_map_π CategoryTheory.Limits.instHasLimitProdObjFunctorUncurryWhiskeringLeft₂OfPreservesLimit₂
isoLimitUncurryWhiskeringLeft₂_hom_comp_map_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.limit CategoryTheory.prod' CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.uncurry CategoryTheory.Functor.whiskeringLeft₂ CategoryTheory.Limits.instHasLimitProdObjFunctorUncurryWhiskeringLeft₂OfPreservesLimit₂ CategoryTheory.Iso.hom isoLimitUncurryWhiskeringLeft₂ CategoryTheory.NatTrans.app CategoryTheory.Functor.map CategoryTheory.Limits.limit.π	—	CategoryTheory.Limits.instHasLimitProdObjFunctorUncurryWhiskeringLeft₂OfPreservesLimit₂ CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoLimitUncurryWhiskeringLeft₂_hom_comp_map_π
isoLimitUncurryWhiskeringLeft₂_inv_comp_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.limit CategoryTheory.prod' CategoryTheory.Functor.uncurry CategoryTheory.Functor.whiskeringLeft₂ CategoryTheory.Limits.instHasLimitProdObjFunctorUncurryWhiskeringLeft₂OfPreservesLimit₂ CategoryTheory.Iso.inv isoLimitUncurryWhiskeringLeft₂ CategoryTheory.Limits.limit.π CategoryTheory.NatTrans.app CategoryTheory.Functor.map	—	isoObjConePointsOfIsLimit_hom_comp_π CategoryTheory.Limits.instHasLimitProdObjFunctorUncurryWhiskeringLeft₂OfPreservesLimit₂
isoLimitUncurryWhiskeringLeft₂_inv_comp_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.limit CategoryTheory.prod' CategoryTheory.Functor.uncurry CategoryTheory.Functor.whiskeringLeft₂ CategoryTheory.Limits.instHasLimitProdObjFunctorUncurryWhiskeringLeft₂OfPreservesLimit₂ CategoryTheory.Iso.inv isoLimitUncurryWhiskeringLeft₂ CategoryTheory.Limits.limit.π CategoryTheory.NatTrans.app CategoryTheory.Functor.map	—	CategoryTheory.Limits.instHasLimitProdObjFunctorUncurryWhiskeringLeft₂OfPreservesLimit₂ CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoLimitUncurryWhiskeringLeft₂_inv_comp_π
isoObjConePointsOfIsColimit_inv_comp_map_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.prod' CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.uncurry CategoryTheory.Functor.whiskeringLeft₂ CategoryTheory.Iso.inv isoObjConePointsOfIsLimit CategoryTheory.NatTrans.app CategoryTheory.Functor.const CategoryTheory.Functor.map CategoryTheory.Limits.Cone.π	—	CategoryTheory.Iso.inv_comp_eq isoObjConePointsOfIsLimit_hom_comp_π
isoObjConePointsOfIsColimit_inv_comp_map_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Limits.Cone.pt CategoryTheory.prod' CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.uncurry CategoryTheory.Functor.whiskeringLeft₂ CategoryTheory.Iso.inv isoObjConePointsOfIsLimit CategoryTheory.NatTrans.app CategoryTheory.Functor.const CategoryTheory.Functor.map CategoryTheory.Limits.Cone.π	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoObjConePointsOfIsColimit_inv_comp_map_π
isoObjConePointsOfIsLimit_hom_comp_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.Cone.pt CategoryTheory.prod' CategoryTheory.Functor.uncurry CategoryTheory.Functor.whiskeringLeft₂ CategoryTheory.Iso.hom isoObjConePointsOfIsLimit CategoryTheory.NatTrans.app CategoryTheory.Functor.const CategoryTheory.Limits.Cone.π CategoryTheory.Functor.map	—	CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp
isoObjConePointsOfIsLimit_hom_comp_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Limits.Cone.pt CategoryTheory.prod' CategoryTheory.Functor.uncurry CategoryTheory.Functor.whiskeringLeft₂ CategoryTheory.Iso.hom isoObjConePointsOfIsLimit CategoryTheory.NatTrans.app CategoryTheory.Functor.const CategoryTheory.Limits.Cone.π CategoryTheory.Functor.map	—	CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' isoObjConePointsOfIsLimit_hom_comp_π
nonempty_isLimit_mapCone₂ 📖	mathematical	—	CategoryTheory.Limits.IsLimit CategoryTheory.prod' CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.uncurry CategoryTheory.Functor.whiskeringLeft₂ CategoryTheory.Functor.mapCone₂	—	—
of_preservesLimits_in_each_variable 📖	mathematical	CategoryTheory.Limits.PreservesLimit CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.Functor.flip	CategoryTheory.Limits.PreservesLimit₂	—	CategoryTheory.NatTrans.naturality CategoryTheory.Functor.map_id CategoryTheory.Functor.map_comp CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.Limits.IsLimit.hom_ext CategoryTheory.Limits.IsLimit.fac
of_preservesLimit₂_flip 📖	mathematical	—	CategoryTheory.Limits.PreservesLimit₂ CategoryTheory.Functor.flip	—	CategoryTheory.Category.comp_id CategoryTheory.Category.id_comp CategoryTheory.NatTrans.naturality

---

← Back to Index