IndYoneda

📁 Source: Mathlib/CategoryTheory/Limits/IndYoneda.lean

Statistics

Metric	Count
Definitions colimitCoyonedaHomIsoLimit, colimitCoyonedaHomIsoLimit', colimitCoyonedaHomIsoLimitLeftOp, colimitCoyonedaHomIsoLimitUnop, colimitHomIsoLimitYoneda, colimitHomIsoLimitYoneda', colimitYonedaHomIsoLimit, colimitYonedaHomIsoLimit', colimitYonedaHomIsoLimitOp, colimitYonedaHomIsoLimitRightOp, coyonedaOpColimitIsoLimitCoyoneda, coyonedaOpColimitIsoLimitCoyoneda'	12
Theorems colimitCoyonedaHomIsoLimit'_π_apply, colimitCoyonedaHomIsoLimitLeftOp_π_apply, colimitCoyonedaHomIsoLimitUnop_π_apply, colimitCoyonedaHomIsoLimit_π_apply, colimitHomIsoLimitYoneda'_hom_comp_π, colimitHomIsoLimitYoneda'_hom_comp_π_assoc, colimitHomIsoLimitYoneda'_inv_comp_π, colimitHomIsoLimitYoneda'_inv_comp_π_assoc, colimitHomIsoLimitYoneda_hom_comp_π, colimitHomIsoLimitYoneda_hom_comp_π_assoc, colimitHomIsoLimitYoneda_inv_comp_π, colimitHomIsoLimitYoneda_inv_comp_π_assoc, colimitYonedaHomIsoLimit'_π_apply, colimitYonedaHomIsoLimitOp_π_apply, colimitYonedaHomIsoLimitRightOp_π_apply, colimitYonedaHomIsoLimit_π_apply, coyonedaOpColimitIsoLimitCoyoneda'_hom_comp_π, coyonedaOpColimitIsoLimitCoyoneda'_hom_comp_π_assoc, coyonedaOpColimitIsoLimitCoyoneda'_inv_comp_π, coyonedaOpColimitIsoLimitCoyoneda'_inv_comp_π_assoc, coyonedaOpColimitIsoLimitCoyoneda_hom_comp_π, coyonedaOpColimitIsoLimitCoyoneda_hom_comp_π_assoc, coyonedaOpColimitIsoLimitCoyoneda_inv_comp_π, coyonedaOpColimitIsoLimitCoyoneda_inv_comp_π_assoc	24
Total	36

CategoryTheory.Limits

Definitions

Name	Category	Theorems
colimitCoyonedaHomIsoLimit 📖	CompOp	1 math math: colimitCoyonedaHomIsoLimit_π_apply
colimitCoyonedaHomIsoLimit' 📖	CompOp	1 math math: colimitCoyonedaHomIsoLimit'_π_apply
colimitCoyonedaHomIsoLimitLeftOp 📖	CompOp	1 math math: colimitCoyonedaHomIsoLimitLeftOp_π_apply
colimitCoyonedaHomIsoLimitUnop 📖	CompOp	1 math math: colimitCoyonedaHomIsoLimitUnop_π_apply
colimitHomIsoLimitYoneda 📖	CompOp	4 math math: colimitHomIsoLimitYoneda_hom_comp_π, colimitHomIsoLimitYoneda_hom_comp_π_assoc, colimitHomIsoLimitYoneda_inv_comp_π, colimitHomIsoLimitYoneda_inv_comp_π_assoc
colimitHomIsoLimitYoneda' 📖	CompOp	4 math math: colimitHomIsoLimitYoneda'_hom_comp_π, colimitHomIsoLimitYoneda'_hom_comp_π_assoc, colimitHomIsoLimitYoneda'_inv_comp_π_assoc, colimitHomIsoLimitYoneda'_inv_comp_π
colimitYonedaHomIsoLimit 📖	CompOp	1 math math: colimitYonedaHomIsoLimit_π_apply
colimitYonedaHomIsoLimit' 📖	CompOp	1 math math: colimitYonedaHomIsoLimit'_π_apply
colimitYonedaHomIsoLimitOp 📖	CompOp	1 math math: colimitYonedaHomIsoLimitOp_π_apply
colimitYonedaHomIsoLimitRightOp 📖	CompOp	1 math math: colimitYonedaHomIsoLimitRightOp_π_apply
coyonedaOpColimitIsoLimitCoyoneda 📖	CompOp	4 math math: coyonedaOpColimitIsoLimitCoyoneda_hom_comp_π_assoc, coyonedaOpColimitIsoLimitCoyoneda_inv_comp_π_assoc, coyonedaOpColimitIsoLimitCoyoneda_inv_comp_π, coyonedaOpColimitIsoLimitCoyoneda_hom_comp_π
coyonedaOpColimitIsoLimitCoyoneda' 📖	CompOp	4 math math: coyonedaOpColimitIsoLimitCoyoneda'_inv_comp_π, coyonedaOpColimitIsoLimitCoyoneda'_hom_comp_π, coyonedaOpColimitIsoLimitCoyoneda'_inv_comp_π_assoc, coyonedaOpColimitIsoLimitCoyoneda'_hom_comp_π_assoc

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
colimitCoyonedaHomIsoLimit'_π_apply 📖	mathematical	—	limit.π CategoryTheory.types CategoryTheory.Functor.comp CategoryTheory.uliftFunctor hasLimitOfHasLimitsOfShape CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category colimit Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op CategoryTheory.coyoneda limit colimitCoyonedaHomIsoLimit' CategoryTheory.Functor.obj CategoryTheory.NatTrans.app Opposite.op colimit.ι CategoryTheory.CategoryStruct.id	—	hasLimitOfHasLimitsOfShape CategoryTheory.Category.assoc HasLimit.isoOfNatIso_hom_π instHasLimitCompOfPreservesLimit hasLimit_rightOp_of_hasColimit CategoryTheory.yoneda_preservesLimit colimitHomIsoLimitYoneda'_hom_comp_π
colimitCoyonedaHomIsoLimitLeftOp_π_apply 📖	mathematical	—	limit.π Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.comp CategoryTheory.Functor.leftOp CategoryTheory.uliftFunctor hasLimitOfHasLimitsOfShape Opposite.op CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category colimit CategoryTheory.coyoneda limit colimitCoyonedaHomIsoLimitLeftOp CategoryTheory.Functor.obj CategoryTheory.NatTrans.app Opposite.unop colimit.ι CategoryTheory.CategoryStruct.id	—	colimitCoyonedaHomIsoLimit_π_apply
colimitCoyonedaHomIsoLimitUnop_π_apply 📖	mathematical	—	limit.π CategoryTheory.types CategoryTheory.Functor.comp CategoryTheory.Functor.unop CategoryTheory.uliftFunctor hasLimitOfHasLimitsOfShape CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category colimit Opposite CategoryTheory.Category.opposite CategoryTheory.coyoneda limit colimitCoyonedaHomIsoLimitUnop CategoryTheory.Functor.obj CategoryTheory.NatTrans.app Opposite.unop Opposite.op colimit.ι CategoryTheory.CategoryStruct.id	—	colimitCoyonedaHomIsoLimit'_π_apply
colimitCoyonedaHomIsoLimit_π_apply 📖	mathematical	—	limit.π Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.comp CategoryTheory.uliftFunctor hasLimitOfHasLimitsOfShape Opposite.op CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category colimit CategoryTheory.Functor.rightOp CategoryTheory.coyoneda limit colimitCoyonedaHomIsoLimit CategoryTheory.Functor.obj CategoryTheory.NatTrans.app colimit.ι CategoryTheory.CategoryStruct.id	—	hasLimitOfHasLimitsOfShape CategoryTheory.Category.assoc HasLimit.isoOfNatIso_hom_π instHasLimitCompOfPreservesLimit hasLimit_op_of_hasColimit CategoryTheory.yoneda_preservesLimit colimitHomIsoLimitYoneda_hom_comp_π
colimitHomIsoLimitYoneda'_hom_comp_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.types Quiver.Hom CategoryTheory.CategoryStruct.toQuiver colimit Opposite CategoryTheory.Category.opposite limit CategoryTheory.Functor.comp CategoryTheory.Functor.rightOp CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda instHasLimitCompOfPreservesLimit hasLimit_rightOp_of_hasColimit CategoryTheory.yoneda_preservesLimit CategoryTheory.Iso.hom colimitHomIsoLimitYoneda' limit.π CategoryTheory.Functor.map Opposite.op Quiver.Hom.op colimit.ι	—	instHasLimitCompOfPreservesLimit hasLimit_rightOp_of_hasColimit CategoryTheory.yoneda_preservesLimit CategoryTheory.Category.assoc functorCategoryHasLimit hasLimitOfHasLimitsOfShape hasLimitCompEvaluation limitObjIsoLimitCompEvaluation_hom_π PreservesLimitsOfShape.preservesLimit PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.coyonedaFunctor_preservesLimits coyonedaOpColimitIsoLimitCoyoneda'_hom_comp_π CategoryTheory.Functor.flip_map_app
colimitHomIsoLimitYoneda'_hom_comp_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.types Quiver.Hom CategoryTheory.CategoryStruct.toQuiver colimit Opposite CategoryTheory.Category.opposite limit CategoryTheory.Functor.comp CategoryTheory.Functor.rightOp CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda instHasLimitCompOfPreservesLimit hasLimit_rightOp_of_hasColimit CategoryTheory.yoneda_preservesLimit CategoryTheory.Iso.hom colimitHomIsoLimitYoneda' limit.π CategoryTheory.Functor.map Opposite.op Quiver.Hom.op colimit.ι	—	instHasLimitCompOfPreservesLimit hasLimit_rightOp_of_hasColimit CategoryTheory.yoneda_preservesLimit CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' colimitHomIsoLimitYoneda'_hom_comp_π
colimitHomIsoLimitYoneda'_inv_comp_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.types limit CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda instHasLimitCompOfPreservesLimit hasLimit_rightOp_of_hasColimit CategoryTheory.yoneda_preservesLimit Quiver.Hom CategoryTheory.CategoryStruct.toQuiver colimit Opposite.op CategoryTheory.Iso.inv colimitHomIsoLimitYoneda' CategoryTheory.Functor.map Quiver.Hom.op colimit.ι limit.π	—	instHasLimitCompOfPreservesLimit hasLimit_rightOp_of_hasColimit CategoryTheory.yoneda_preservesLimit colimitHomIsoLimitYoneda'_hom_comp_π CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.id_comp
colimitHomIsoLimitYoneda'_inv_comp_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.types limit CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda instHasLimitCompOfPreservesLimit hasLimit_rightOp_of_hasColimit CategoryTheory.yoneda_preservesLimit Quiver.Hom CategoryTheory.CategoryStruct.toQuiver colimit CategoryTheory.Iso.inv colimitHomIsoLimitYoneda' Opposite.op CategoryTheory.Functor.map Quiver.Hom.op colimit.ι limit.π	—	instHasLimitCompOfPreservesLimit hasLimit_rightOp_of_hasColimit CategoryTheory.yoneda_preservesLimit CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' colimitHomIsoLimitYoneda'_inv_comp_π
colimitHomIsoLimitYoneda_hom_comp_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.types Quiver.Hom CategoryTheory.CategoryStruct.toQuiver colimit limit Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp CategoryTheory.Functor.op CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda instHasLimitCompOfPreservesLimit hasLimit_op_of_hasColimit CategoryTheory.yoneda_preservesLimit Opposite.op CategoryTheory.Iso.hom colimitHomIsoLimitYoneda limit.π CategoryTheory.Functor.map Quiver.Hom.op colimit.ι	—	instHasLimitCompOfPreservesLimit hasLimit_op_of_hasColimit CategoryTheory.yoneda_preservesLimit CategoryTheory.Category.assoc functorCategoryHasLimit hasLimitOfHasLimitsOfShape hasLimitCompEvaluation limitObjIsoLimitCompEvaluation_hom_π PreservesLimitsOfShape.preservesLimit PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.coyonedaFunctor_preservesLimits coyonedaOpColimitIsoLimitCoyoneda_hom_comp_π CategoryTheory.Functor.flip_map_app
colimitHomIsoLimitYoneda_hom_comp_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.types Quiver.Hom CategoryTheory.CategoryStruct.toQuiver colimit limit Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp CategoryTheory.Functor.op CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda instHasLimitCompOfPreservesLimit hasLimit_op_of_hasColimit CategoryTheory.yoneda_preservesLimit CategoryTheory.Iso.hom colimitHomIsoLimitYoneda Opposite.op limit.π CategoryTheory.Functor.map Quiver.Hom.op colimit.ι	—	instHasLimitCompOfPreservesLimit hasLimit_op_of_hasColimit CategoryTheory.yoneda_preservesLimit CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' colimitHomIsoLimitYoneda_hom_comp_π
colimitHomIsoLimitYoneda_inv_comp_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.types limit Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp CategoryTheory.Functor.op CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda instHasLimitCompOfPreservesLimit hasLimit_op_of_hasColimit CategoryTheory.yoneda_preservesLimit Quiver.Hom CategoryTheory.CategoryStruct.toQuiver colimit Opposite.op CategoryTheory.Iso.inv colimitHomIsoLimitYoneda CategoryTheory.Functor.map Quiver.Hom.op colimit.ι limit.π	—	instHasLimitCompOfPreservesLimit hasLimit_op_of_hasColimit CategoryTheory.yoneda_preservesLimit colimitHomIsoLimitYoneda_hom_comp_π CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.id_comp
colimitHomIsoLimitYoneda_inv_comp_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.types limit Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp CategoryTheory.Functor.op CategoryTheory.Functor.obj CategoryTheory.Functor CategoryTheory.Functor.category CategoryTheory.yoneda instHasLimitCompOfPreservesLimit hasLimit_op_of_hasColimit CategoryTheory.yoneda_preservesLimit Quiver.Hom CategoryTheory.CategoryStruct.toQuiver colimit CategoryTheory.Iso.inv colimitHomIsoLimitYoneda Opposite.op CategoryTheory.Functor.map Quiver.Hom.op colimit.ι limit.π	—	instHasLimitCompOfPreservesLimit hasLimit_op_of_hasColimit CategoryTheory.yoneda_preservesLimit CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' colimitHomIsoLimitYoneda_inv_comp_π
colimitYonedaHomIsoLimit'_π_apply 📖	mathematical	—	limit.π CategoryTheory.types CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.uliftFunctor hasLimitOfHasLimitsOfShape CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category colimit CategoryTheory.Functor.leftOp CategoryTheory.yoneda limit colimitYonedaHomIsoLimit' CategoryTheory.Functor.obj CategoryTheory.NatTrans.app Opposite.op colimit.ι CategoryTheory.CategoryStruct.id Opposite.unop	—	hasLimitOfHasLimitsOfShape CategoryTheory.Category.assoc HasLimit.isoOfNatIso_hom_π instHasLimitCompOfPreservesLimit hasLimit_rightOp_of_hasColimit CategoryTheory.yoneda_preservesLimit colimitHomIsoLimitYoneda'_hom_comp_π
colimitYonedaHomIsoLimitOp_π_apply 📖	mathematical	—	limit.π Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.comp CategoryTheory.Functor.op CategoryTheory.uliftFunctor hasLimitOfHasLimitsOfShape CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category colimit CategoryTheory.yoneda limit colimitYonedaHomIsoLimitOp CategoryTheory.Functor.obj CategoryTheory.NatTrans.app Opposite.op Opposite.unop colimit.ι CategoryTheory.CategoryStruct.id	—	colimitYonedaHomIsoLimit_π_apply
colimitYonedaHomIsoLimitRightOp_π_apply 📖	mathematical	—	limit.π CategoryTheory.types CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp CategoryTheory.uliftFunctor hasLimitOfHasLimitsOfShape CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category colimit CategoryTheory.yoneda limit colimitYonedaHomIsoLimitRightOp CategoryTheory.Functor.obj CategoryTheory.NatTrans.app Opposite.op colimit.ι CategoryTheory.CategoryStruct.id	—	colimitYonedaHomIsoLimit'_π_apply
colimitYonedaHomIsoLimit_π_apply 📖	mathematical	—	limit.π Opposite CategoryTheory.Category.opposite CategoryTheory.types CategoryTheory.Functor.comp CategoryTheory.uliftFunctor hasLimitOfHasLimitsOfShape CategoryTheory.Iso.hom Quiver.Hom CategoryTheory.Functor CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category colimit CategoryTheory.Functor.unop CategoryTheory.yoneda limit colimitYonedaHomIsoLimit CategoryTheory.Functor.obj CategoryTheory.NatTrans.app Opposite.unop colimit.ι CategoryTheory.CategoryStruct.id	—	hasLimitOfHasLimitsOfShape CategoryTheory.Category.assoc HasLimit.isoOfNatIso_hom_π instHasLimitCompOfPreservesLimit hasLimit_op_of_hasColimit CategoryTheory.yoneda_preservesLimit colimitHomIsoLimitYoneda_hom_comp_π
coyonedaOpColimitIsoLimitCoyoneda'_hom_comp_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.coyoneda Opposite.op colimit limit CategoryTheory.Functor.comp CategoryTheory.Functor.rightOp instHasLimitCompOfPreservesLimit hasLimit_rightOp_of_hasColimit PreservesLimitsOfShape.preservesLimit PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.coyonedaFunctor_preservesLimits CategoryTheory.Iso.hom coyonedaOpColimitIsoLimitCoyoneda' limit.π CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver colimit.ι	—	instHasLimitCompOfPreservesLimit hasLimit_rightOp_of_hasColimit PreservesLimitsOfShape.preservesLimit PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.coyonedaFunctor_preservesLimits CategoryTheory.Category.assoc CategoryTheory.preservesLimitIso_hom_π limitRightOpIsoOpColimit_inv_comp_π
coyonedaOpColimitIsoLimitCoyoneda'_hom_comp_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.coyoneda Opposite.op colimit limit CategoryTheory.Functor.comp CategoryTheory.Functor.rightOp instHasLimitCompOfPreservesLimit hasLimit_rightOp_of_hasColimit PreservesLimitsOfShape.preservesLimit PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.coyonedaFunctor_preservesLimits CategoryTheory.Iso.hom coyonedaOpColimitIsoLimitCoyoneda' limit.π CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver colimit.ι	—	instHasLimitCompOfPreservesLimit hasLimit_rightOp_of_hasColimit PreservesLimitsOfShape.preservesLimit PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.coyonedaFunctor_preservesLimits CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' coyonedaOpColimitIsoLimitCoyoneda'_hom_comp_π
coyonedaOpColimitIsoLimitCoyoneda'_inv_comp_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category limit CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp CategoryTheory.coyoneda instHasLimitCompOfPreservesLimit hasLimit_rightOp_of_hasColimit PreservesLimitsOfShape.preservesLimit PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.coyonedaFunctor_preservesLimits CategoryTheory.Functor.obj Opposite.op colimit CategoryTheory.Iso.inv coyonedaOpColimitIsoLimitCoyoneda' CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver colimit.ι limit.π	—	instHasLimitCompOfPreservesLimit hasLimit_rightOp_of_hasColimit PreservesLimitsOfShape.preservesLimit PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.coyonedaFunctor_preservesLimits coyonedaOpColimitIsoLimitCoyoneda'_hom_comp_π CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.id_comp
coyonedaOpColimitIsoLimitCoyoneda'_inv_comp_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category limit CategoryTheory.Functor.comp Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp CategoryTheory.coyoneda instHasLimitCompOfPreservesLimit hasLimit_rightOp_of_hasColimit PreservesLimitsOfShape.preservesLimit PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.coyonedaFunctor_preservesLimits CategoryTheory.Functor.obj Opposite.op colimit CategoryTheory.Iso.inv coyonedaOpColimitIsoLimitCoyoneda' CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver colimit.ι limit.π	—	instHasLimitCompOfPreservesLimit hasLimit_rightOp_of_hasColimit PreservesLimitsOfShape.preservesLimit PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.coyonedaFunctor_preservesLimits CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' coyonedaOpColimitIsoLimitCoyoneda'_inv_comp_π
coyonedaOpColimitIsoLimitCoyoneda_hom_comp_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.coyoneda Opposite.op colimit limit CategoryTheory.Functor.comp CategoryTheory.Functor.op instHasLimitCompOfPreservesLimit hasLimit_op_of_hasColimit PreservesLimitsOfShape.preservesLimit PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.coyonedaFunctor_preservesLimits CategoryTheory.Iso.hom coyonedaOpColimitIsoLimitCoyoneda limit.π CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver colimit.ι	—	instHasLimitCompOfPreservesLimit hasLimit_op_of_hasColimit PreservesLimitsOfShape.preservesLimit PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.coyonedaFunctor_preservesLimits CategoryTheory.Category.assoc CategoryTheory.preservesLimitIso_hom_π limitOpIsoOpColimit_inv_comp_π
coyonedaOpColimitIsoLimitCoyoneda_hom_comp_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.coyoneda Opposite.op colimit limit CategoryTheory.Functor.comp CategoryTheory.Functor.op instHasLimitCompOfPreservesLimit hasLimit_op_of_hasColimit PreservesLimitsOfShape.preservesLimit PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.coyonedaFunctor_preservesLimits CategoryTheory.Iso.hom coyonedaOpColimitIsoLimitCoyoneda limit.π CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver colimit.ι	—	instHasLimitCompOfPreservesLimit hasLimit_op_of_hasColimit PreservesLimitsOfShape.preservesLimit PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.coyonedaFunctor_preservesLimits CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' coyonedaOpColimitIsoLimitCoyoneda_hom_comp_π
coyonedaOpColimitIsoLimitCoyoneda_inv_comp_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category limit Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp CategoryTheory.Functor.op CategoryTheory.coyoneda instHasLimitCompOfPreservesLimit hasLimit_op_of_hasColimit PreservesLimitsOfShape.preservesLimit PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.coyonedaFunctor_preservesLimits CategoryTheory.Functor.obj Opposite.op colimit CategoryTheory.Iso.inv coyonedaOpColimitIsoLimitCoyoneda CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver colimit.ι limit.π	—	instHasLimitCompOfPreservesLimit hasLimit_op_of_hasColimit PreservesLimitsOfShape.preservesLimit PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.coyonedaFunctor_preservesLimits coyonedaOpColimitIsoLimitCoyoneda_hom_comp_π CategoryTheory.Category.assoc CategoryTheory.Iso.inv_hom_id CategoryTheory.Category.id_comp
coyonedaOpColimitIsoLimitCoyoneda_inv_comp_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Functor CategoryTheory.types CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.category limit Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.comp CategoryTheory.Functor.op CategoryTheory.coyoneda instHasLimitCompOfPreservesLimit hasLimit_op_of_hasColimit PreservesLimitsOfShape.preservesLimit PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.coyonedaFunctor_preservesLimits CategoryTheory.Functor.obj Opposite.op colimit CategoryTheory.Iso.inv coyonedaOpColimitIsoLimitCoyoneda CategoryTheory.Functor.map Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver colimit.ι limit.π	—	instHasLimitCompOfPreservesLimit hasLimit_op_of_hasColimit PreservesLimitsOfShape.preservesLimit PreservesLimitsOfSize.preservesLimitsOfShape CategoryTheory.coyonedaFunctor_preservesLimits CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' coyonedaOpColimitIsoLimitCoyoneda_inv_comp_π

---

← Back to Index