Opposites

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

Statistics

Metric	Count
Definitions colimitLeftOpIsoUnopLimit, colimitOpIsoOpLimit, colimitRightOpIsoUnopLimit, colimitUnopIsoOpLimit, isColimitCoconeLeftOpOfCone, isColimitCoconeOfConeLeftOp, isColimitCoconeOfConeRightOp, isColimitCoconeOfConeUnop, isColimitCoconeRightOpOfCone, isColimitCoconeUnopOfCone, isColimitOfConeLeftOpOfCocone, isColimitOfConeOfCoconeLeftOp, isColimitOfConeOfCoconeRightOp, isColimitOfConeOfCoconeUnop, isColimitOfConeRightOpOfCocone, isColimitOfConeUnopOfCocone, isLimitConeLeftOpOfCocone, isLimitConeOfCoconeLeftOp, isLimitConeOfCoconeRightOp, isLimitConeOfCoconeUnop, isLimitConeRightOpOfCocone, isLimitConeUnopOfCocone, isLimitOfCoconeLeftOpOfCone, isLimitOfCoconeOfConeLeftOp, isLimitOfCoconeOfConeRightOp, isLimitOfCoconeOfConeUnop, isLimitOfCoconeRightOpOfCone, isLimitOfCoconeUnopOfCone, limitLeftOpIsoUnopColimit, limitOpIsoOpColimit, limitRightOpIsoOpColimit, limitUnopIsoUnopColimit	32
Theorems hasColimit_leftOp_of_hasLimit, hasColimit_of_hasLimit_leftOp, hasColimit_of_hasLimit_op, hasColimit_of_hasLimit_rightOp, hasColimit_of_hasLimit_unop, hasColimit_op_of_hasLimit, hasColimit_rightOp_of_hasLimit, hasColimit_unop_of_hasLimit, hasColimitsOfShape_of_hasLimitsOfShape_op, hasColimitsOfShape_op_of_hasLimitsOfShape, hasColimits_of_hasLimits_op, hasColimits_op_of_hasLimits, hasFiniteColimits_opposite, hasFiniteLimits_opposite, hasLimit_leftOp_of_hasColimit, hasLimit_of_hasColimit_leftOp, hasLimit_of_hasColimit_op, hasLimit_of_hasColimit_rightOp, hasLimit_of_hasColimit_unop, hasLimit_op_of_hasColimit, hasLimit_rightOp_of_hasColimit, hasLimit_unop_of_hasColimit, hasLimitsOfShape_of_hasColimitsOfShape_op, hasLimitsOfShape_op_of_hasColimitsOfShape, hasLimits_of_hasColimits_op, hasLimits_op_of_hasColimits, isColimitCoconeLeftOpOfCone_desc, isColimitCoconeOfConeLeftOp_desc, isColimitCoconeOfConeRightOp_desc, isColimitCoconeOfConeUnop_desc, isColimitCoconeRightOpOfCone_desc, isColimitCoconeUnopOfCone_desc, isColimitOfConeLeftOpOfCocone_desc, isColimitOfConeOfCoconeLeftOp_desc, isColimitOfConeOfCoconeRightOp_desc, isColimitOfConeOfCoconeUnop_desc, isColimitOfConeRightOpOfCocone_desc, isColimitOfConeUnopOfCocone_desc, isLimitConeLeftOpOfCocone_lift, isLimitConeOfCoconeLeftOp_lift, isLimitConeOfCoconeRightOp_lift, isLimitConeOfCoconeUnop_lift, isLimitConeRightOpOfCocone_lift, isLimitConeUnopOfCocone_lift, isLimitOfCoconeLeftOpOfCone_lift, isLimitOfCoconeOfConeLeftOp_lift, isLimitOfCoconeOfConeRightOp_lift, isLimitOfCoconeOfConeUnop_lift, isLimitOfCoconeRightOpOfCone_lift, isLimitOfCoconeUnopOfCone_lift, limitLeftOpIsoUnopColimit_hom_comp_ι, limitLeftOpIsoUnopColimit_hom_comp_ι_assoc, limitLeftOpIsoUnopColimit_inv_comp_π, limitLeftOpIsoUnopColimit_inv_comp_π_assoc, limitOpIsoOpColimit_hom_comp_ι, limitOpIsoOpColimit_hom_comp_ι_assoc, limitOpIsoOpColimit_inv_comp_π, limitOpIsoOpColimit_inv_comp_π_assoc, limitRightOpIsoOpColimit_hom_comp_ι, limitRightOpIsoOpColimit_hom_comp_ι_assoc, limitRightOpIsoOpColimit_inv_comp_π, limitRightOpIsoOpColimit_inv_comp_π_assoc, limitUnopIsoUnopColimit_hom_comp_ι, limitUnopIsoUnopColimit_hom_comp_ι_assoc, limitUnopIsoUnopColimit_inv_comp_π, limitUnopIsoUnopColimit_inv_comp_π_assoc, ι_comp_colimitLeftOpIsoUnopLimit_hom, ι_comp_colimitLeftOpIsoUnopLimit_hom_assoc, ι_comp_colimitOpIsoOpLimit_hom, ι_comp_colimitOpIsoOpLimit_hom_assoc, ι_comp_colimitRightOpIsoUnopLimit_hom, ι_comp_colimitRightOpIsoUnopLimit_hom_assoc, ι_comp_colimitUnopIsoOpLimit_hom, ι_comp_colimitUnopIsoOpLimit_hom_assoc, π_comp_colimitLeftOpIsoUnopLimit_inv, π_comp_colimitLeftOpIsoUnopLimit_inv_assoc, π_comp_colimitOpIsoOpLimit_inv, π_comp_colimitOpIsoOpLimit_inv_assoc, π_comp_colimitRightOpIsoUnopLimit_inv, π_comp_colimitRightOpIsoUnopLimit_inv_assoc, π_comp_colimitUnopIsoOpLimit_inv, π_comp_colimitUnopIsoOpLimit_inv_assoc	82
Total	114

CategoryTheory.Limits

Definitions

Name	Category	Theorems
colimitLeftOpIsoUnopLimit 📖	CompOp	4 math math: π_comp_colimitLeftOpIsoUnopLimit_inv, π_comp_colimitLeftOpIsoUnopLimit_inv_assoc, ι_comp_colimitLeftOpIsoUnopLimit_hom_assoc, ι_comp_colimitLeftOpIsoUnopLimit_hom
colimitOpIsoOpLimit 📖	CompOp	4 math math: ι_comp_colimitOpIsoOpLimit_hom_assoc, π_comp_colimitOpIsoOpLimit_inv_assoc, π_comp_colimitOpIsoOpLimit_inv, ι_comp_colimitOpIsoOpLimit_hom
colimitRightOpIsoUnopLimit 📖	CompOp	4 math math: ι_comp_colimitRightOpIsoUnopLimit_hom_assoc, ι_comp_colimitRightOpIsoUnopLimit_hom, π_comp_colimitRightOpIsoUnopLimit_inv, π_comp_colimitRightOpIsoUnopLimit_inv_assoc
colimitUnopIsoOpLimit 📖	CompOp	4 math math: π_comp_colimitUnopIsoOpLimit_inv, ι_comp_colimitUnopIsoOpLimit_hom_assoc, π_comp_colimitUnopIsoOpLimit_inv_assoc, ι_comp_colimitUnopIsoOpLimit_hom
isColimitCoconeLeftOpOfCone 📖	CompOp	1 math math: isColimitCoconeLeftOpOfCone_desc
isColimitCoconeOfConeLeftOp 📖	CompOp	1 math math: isColimitCoconeOfConeLeftOp_desc
isColimitCoconeOfConeRightOp 📖	CompOp	1 math math: isColimitCoconeOfConeRightOp_desc
isColimitCoconeOfConeUnop 📖	CompOp	1 math math: isColimitCoconeOfConeUnop_desc
isColimitCoconeRightOpOfCone 📖	CompOp	1 math math: isColimitCoconeRightOpOfCone_desc
isColimitCoconeUnopOfCone 📖	CompOp	1 math math: isColimitCoconeUnopOfCone_desc
isColimitOfConeLeftOpOfCocone 📖	CompOp	1 math math: isColimitOfConeLeftOpOfCocone_desc
isColimitOfConeOfCoconeLeftOp 📖	CompOp	1 math math: isColimitOfConeOfCoconeLeftOp_desc
isColimitOfConeOfCoconeRightOp 📖	CompOp	1 math math: isColimitOfConeOfCoconeRightOp_desc
isColimitOfConeOfCoconeUnop 📖	CompOp	1 math math: isColimitOfConeOfCoconeUnop_desc
isColimitOfConeRightOpOfCocone 📖	CompOp	1 math math: isColimitOfConeRightOpOfCocone_desc
isColimitOfConeUnopOfCocone 📖	CompOp	1 math math: isColimitOfConeUnopOfCocone_desc
isLimitConeLeftOpOfCocone 📖	CompOp	1 math math: isLimitConeLeftOpOfCocone_lift
isLimitConeOfCoconeLeftOp 📖	CompOp	1 math math: isLimitConeOfCoconeLeftOp_lift
isLimitConeOfCoconeRightOp 📖	CompOp	1 math math: isLimitConeOfCoconeRightOp_lift
isLimitConeOfCoconeUnop 📖	CompOp	1 math math: isLimitConeOfCoconeUnop_lift
isLimitConeRightOpOfCocone 📖	CompOp	1 math math: isLimitConeRightOpOfCocone_lift
isLimitConeUnopOfCocone 📖	CompOp	1 math math: isLimitConeUnopOfCocone_lift
isLimitOfCoconeLeftOpOfCone 📖	CompOp	1 math math: isLimitOfCoconeLeftOpOfCone_lift
isLimitOfCoconeOfConeLeftOp 📖	CompOp	1 math math: isLimitOfCoconeOfConeLeftOp_lift
isLimitOfCoconeOfConeRightOp 📖	CompOp	1 math math: isLimitOfCoconeOfConeRightOp_lift
isLimitOfCoconeOfConeUnop 📖	CompOp	1 math math: isLimitOfCoconeOfConeUnop_lift
isLimitOfCoconeRightOpOfCone 📖	CompOp	1 math math: isLimitOfCoconeRightOpOfCone_lift
isLimitOfCoconeUnopOfCone 📖	CompOp	1 math math: isLimitOfCoconeUnopOfCone_lift
limitLeftOpIsoUnopColimit 📖	CompOp	4 math math: limitLeftOpIsoUnopColimit_inv_comp_π, limitLeftOpIsoUnopColimit_hom_comp_ι_assoc, limitLeftOpIsoUnopColimit_inv_comp_π_assoc, limitLeftOpIsoUnopColimit_hom_comp_ι
limitOpIsoOpColimit 📖	CompOp	4 math math: limitOpIsoOpColimit_hom_comp_ι_assoc, limitOpIsoOpColimit_inv_comp_π_assoc, limitOpIsoOpColimit_inv_comp_π, limitOpIsoOpColimit_hom_comp_ι
limitRightOpIsoOpColimit 📖	CompOp	4 math math: limitRightOpIsoOpColimit_hom_comp_ι, limitRightOpIsoOpColimit_hom_comp_ι_assoc, limitRightOpIsoOpColimit_inv_comp_π_assoc, limitRightOpIsoOpColimit_inv_comp_π
limitUnopIsoUnopColimit 📖	CompOp	4 math math: limitUnopIsoUnopColimit_hom_comp_ι, limitUnopIsoUnopColimit_inv_comp_π_assoc, limitUnopIsoUnopColimit_hom_comp_ι_assoc, limitUnopIsoUnopColimit_inv_comp_π

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
hasColimit_leftOp_of_hasLimit 📖	mathematical	—	HasColimit Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp	—	—
hasColimit_of_hasLimit_leftOp 📖	mathematical	—	HasColimit Opposite CategoryTheory.Category.opposite	—	—
hasColimit_of_hasLimit_op 📖	mathematical	—	HasColimit	—	—
hasColimit_of_hasLimit_rightOp 📖	mathematical	—	HasColimit Opposite CategoryTheory.Category.opposite	—	—
hasColimit_of_hasLimit_unop 📖	mathematical	—	HasColimit Opposite CategoryTheory.Category.opposite	—	—
hasColimit_op_of_hasLimit 📖	mathematical	—	HasColimit Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	—	—
hasColimit_rightOp_of_hasLimit 📖	mathematical	—	HasColimit Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp	—	—
hasColimit_unop_of_hasLimit 📖	mathematical	—	HasColimit CategoryTheory.Functor.unop	—	—
hasColimitsOfShape_of_hasLimitsOfShape_op 📖	mathematical	—	HasColimitsOfShape	—	hasColimit_of_hasLimit_op hasLimitOfHasLimitsOfShape
hasColimitsOfShape_op_of_hasLimitsOfShape 📖	mathematical	—	HasColimitsOfShape Opposite CategoryTheory.Category.opposite	—	hasColimit_of_hasLimit_leftOp hasLimitOfHasLimitsOfShape
hasColimits_of_hasLimits_op 📖	mathematical	—	HasColimitsOfSize	—	hasColimitsOfShape_of_hasLimitsOfShape_op hasLimitsOfShapeOfHasLimits
hasColimits_op_of_hasLimits 📖	mathematical	—	HasColimitsOfSize Opposite CategoryTheory.Category.opposite	—	hasColimitsOfShape_op_of_hasLimitsOfShape hasLimitsOfShapeOfHasLimits
hasFiniteColimits_opposite 📖	mathematical	—	HasFiniteColimits Opposite CategoryTheory.Category.opposite	—	hasColimitsOfShape_op_of_hasLimitsOfShape hasLimitsOfShape_of_hasFiniteLimits
hasFiniteLimits_opposite 📖	mathematical	—	HasFiniteLimits Opposite CategoryTheory.Category.opposite	—	hasLimitsOfShape_op_of_hasColimitsOfShape hasColimitsOfShape_of_hasFiniteColimits
hasLimit_leftOp_of_hasColimit 📖	mathematical	—	HasLimit Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp	—	—
hasLimit_of_hasColimit_leftOp 📖	mathematical	—	HasLimit Opposite CategoryTheory.Category.opposite	—	—
hasLimit_of_hasColimit_op 📖	mathematical	—	HasLimit	—	—
hasLimit_of_hasColimit_rightOp 📖	mathematical	—	HasLimit Opposite CategoryTheory.Category.opposite	—	—
hasLimit_of_hasColimit_unop 📖	mathematical	—	HasLimit Opposite CategoryTheory.Category.opposite	—	—
hasLimit_op_of_hasColimit 📖	mathematical	—	HasLimit Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.op	—	—
hasLimit_rightOp_of_hasColimit 📖	mathematical	—	HasLimit Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp	—	—
hasLimit_unop_of_hasColimit 📖	mathematical	—	HasLimit CategoryTheory.Functor.unop	—	—
hasLimitsOfShape_of_hasColimitsOfShape_op 📖	mathematical	—	HasLimitsOfShape	—	hasLimit_of_hasColimit_op hasColimitOfHasColimitsOfShape
hasLimitsOfShape_op_of_hasColimitsOfShape 📖	mathematical	—	HasLimitsOfShape Opposite CategoryTheory.Category.opposite	—	hasLimit_of_hasColimit_leftOp hasColimitOfHasColimitsOfShape
hasLimits_of_hasColimits_op 📖	mathematical	—	HasLimitsOfSize	—	hasLimitsOfShape_of_hasColimitsOfShape_op hasColimitsOfShapeOfHasColimitsOfSize
hasLimits_op_of_hasColimits 📖	mathematical	—	HasLimitsOfSize Opposite CategoryTheory.Category.opposite	—	hasLimitsOfShape_op_of_hasColimitsOfShape hasColimitsOfShapeOfHasColimitsOfSize
isColimitCoconeLeftOpOfCone_desc 📖	mathematical	—	IsColimit.desc Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp coconeLeftOpOfCone isColimitCoconeLeftOpOfCone Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Cone.pt coneOfCoconeLeftOp IsLimit.lift	—	—
isColimitCoconeOfConeLeftOp_desc 📖	mathematical	—	IsColimit.desc Opposite CategoryTheory.Category.opposite coconeOfConeLeftOp isColimitCoconeOfConeLeftOp Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Cone.pt CategoryTheory.Functor.leftOp coneLeftOpOfCocone IsLimit.lift	—	—
isColimitCoconeOfConeRightOp_desc 📖	mathematical	—	IsColimit.desc Opposite CategoryTheory.Category.opposite coconeOfConeRightOp isColimitCoconeOfConeRightOp Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Cone.pt CategoryTheory.Functor.rightOp coneRightOpOfCocone IsLimit.lift	—	—
isColimitCoconeOfConeUnop_desc 📖	mathematical	—	IsColimit.desc Opposite CategoryTheory.Category.opposite coconeOfConeUnop isColimitCoconeOfConeUnop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Cone.pt CategoryTheory.Functor.unop coneUnopOfCocone IsLimit.lift	—	—
isColimitCoconeRightOpOfCone_desc 📖	mathematical	—	IsColimit.desc Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp coconeRightOpOfCone isColimitCoconeRightOpOfCone Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Cone.pt coneOfCoconeRightOp IsLimit.lift	—	—
isColimitCoconeUnopOfCone_desc 📖	mathematical	—	IsColimit.desc CategoryTheory.Functor.unop coconeUnopOfCone isColimitCoconeUnopOfCone Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Cone.pt Opposite CategoryTheory.Category.opposite coneOfCoconeUnop IsLimit.lift	—	—
isColimitOfConeLeftOpOfCocone_desc 📖	mathematical	—	IsColimit.desc Opposite CategoryTheory.Category.opposite isColimitOfConeLeftOpOfCocone Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop Cocone.pt IsLimit.lift CategoryTheory.Functor.leftOp coneLeftOpOfCocone	—	—
isColimitOfConeOfCoconeLeftOp_desc 📖	mathematical	—	IsColimit.desc Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp isColimitOfConeOfCoconeLeftOp Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.op Cocone.pt IsLimit.lift coneOfCoconeLeftOp	—	—
isColimitOfConeOfCoconeRightOp_desc 📖	mathematical	—	IsColimit.desc Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp isColimitOfConeOfCoconeRightOp Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop Cocone.pt IsLimit.lift coneOfCoconeRightOp	—	—
isColimitOfConeOfCoconeUnop_desc 📖	mathematical	—	IsColimit.desc CategoryTheory.Functor.unop isColimitOfConeOfCoconeUnop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.op Cocone.pt IsLimit.lift Opposite CategoryTheory.Category.opposite coneOfCoconeUnop	—	—
isColimitOfConeRightOpOfCocone_desc 📖	mathematical	—	IsColimit.desc Opposite CategoryTheory.Category.opposite isColimitOfConeRightOpOfCocone Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.op Cocone.pt IsLimit.lift CategoryTheory.Functor.rightOp coneRightOpOfCocone	—	—
isColimitOfConeUnopOfCocone_desc 📖	mathematical	—	IsColimit.desc Opposite CategoryTheory.Category.opposite isColimitOfConeUnopOfCocone Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop Cocone.pt IsLimit.lift CategoryTheory.Functor.unop coneUnopOfCocone	—	—
isLimitConeLeftOpOfCocone_lift 📖	mathematical	—	IsLimit.lift Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp coneLeftOpOfCocone isLimitConeLeftOpOfCocone Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Cocone.pt coconeOfConeLeftOp IsColimit.desc	—	—
isLimitConeOfCoconeLeftOp_lift 📖	mathematical	—	IsLimit.lift Opposite CategoryTheory.Category.opposite coneOfCoconeLeftOp isLimitConeOfCoconeLeftOp Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Cocone.pt CategoryTheory.Functor.leftOp coconeLeftOpOfCone IsColimit.desc	—	—
isLimitConeOfCoconeRightOp_lift 📖	mathematical	—	IsLimit.lift Opposite CategoryTheory.Category.opposite coneOfCoconeRightOp isLimitConeOfCoconeRightOp Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Cocone.pt CategoryTheory.Functor.rightOp coconeRightOpOfCone IsColimit.desc	—	—
isLimitConeOfCoconeUnop_lift 📖	mathematical	—	IsLimit.lift Opposite CategoryTheory.Category.opposite coneOfCoconeUnop isLimitConeOfCoconeUnop Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Cocone.pt CategoryTheory.Functor.unop coconeUnopOfCone IsColimit.desc	—	—
isLimitConeRightOpOfCocone_lift 📖	mathematical	—	IsLimit.lift Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp coneRightOpOfCocone isLimitConeRightOpOfCocone Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Cocone.pt coconeOfConeRightOp IsColimit.desc	—	—
isLimitConeUnopOfCocone_lift 📖	mathematical	—	IsLimit.lift CategoryTheory.Functor.unop coneUnopOfCocone isLimitConeUnopOfCocone Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Cocone.pt Opposite CategoryTheory.Category.opposite coconeOfConeUnop IsColimit.desc	—	—
isLimitOfCoconeLeftOpOfCone_lift 📖	mathematical	—	IsLimit.lift Opposite CategoryTheory.Category.opposite isLimitOfCoconeLeftOpOfCone Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop Cone.pt IsColimit.desc CategoryTheory.Functor.leftOp coconeLeftOpOfCone	—	—
isLimitOfCoconeOfConeLeftOp_lift 📖	mathematical	—	IsLimit.lift Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp isLimitOfCoconeOfConeLeftOp Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.op Cone.pt IsColimit.desc coconeOfConeLeftOp	—	—
isLimitOfCoconeOfConeRightOp_lift 📖	mathematical	—	IsLimit.lift Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp isLimitOfCoconeOfConeRightOp Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop Cone.pt IsColimit.desc coconeOfConeRightOp	—	—
isLimitOfCoconeOfConeUnop_lift 📖	mathematical	—	IsLimit.lift CategoryTheory.Functor.unop isLimitOfCoconeOfConeUnop Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.op Cone.pt IsColimit.desc Opposite CategoryTheory.Category.opposite coconeOfConeUnop	—	—
isLimitOfCoconeRightOpOfCone_lift 📖	mathematical	—	IsLimit.lift Opposite CategoryTheory.Category.opposite isLimitOfCoconeRightOpOfCone Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.op Cone.pt IsColimit.desc CategoryTheory.Functor.rightOp coconeRightOpOfCone	—	—
isLimitOfCoconeUnopOfCone_lift 📖	mathematical	—	IsLimit.lift Opposite CategoryTheory.Category.opposite isLimitOfCoconeUnopOfCone Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver CategoryTheory.Category.toCategoryStruct Opposite.unop Cone.pt IsColimit.desc CategoryTheory.Functor.unop coconeUnopOfCone	—	—
limitLeftOpIsoUnopColimit_hom_comp_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct limit Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp hasLimit_leftOp_of_hasColimit Opposite.unop colimit CategoryTheory.Functor.obj CategoryTheory.Iso.hom limitLeftOpIsoUnopColimit Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver colimit.ι limit.π Opposite.op	—	hasLimit_leftOp_of_hasColimit limitLeftOpIsoUnopColimit_inv_comp_π
limitLeftOpIsoUnopColimit_hom_comp_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct limit Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp hasLimit_leftOp_of_hasColimit Opposite.unop colimit CategoryTheory.Iso.hom limitLeftOpIsoUnopColimit CategoryTheory.Functor.obj Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver colimit.ι limit.π Opposite.op	—	hasLimit_leftOp_of_hasColimit CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' limitLeftOpIsoUnopColimit_hom_comp_ι
limitLeftOpIsoUnopColimit_inv_comp_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop colimit Opposite CategoryTheory.Category.opposite limit CategoryTheory.Functor.leftOp hasLimit_leftOp_of_hasColimit CategoryTheory.Functor.obj CategoryTheory.Iso.inv limitLeftOpIsoUnopColimit limit.π Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver colimit.ι	—	hasLimit_leftOp_of_hasColimit limit.isoLimitCone_inv_π
limitLeftOpIsoUnopColimit_inv_comp_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop colimit Opposite CategoryTheory.Category.opposite limit CategoryTheory.Functor.leftOp hasLimit_leftOp_of_hasColimit CategoryTheory.Iso.inv limitLeftOpIsoUnopColimit CategoryTheory.Functor.obj limit.π Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver colimit.ι	—	hasLimit_leftOp_of_hasColimit CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' limitLeftOpIsoUnopColimit_inv_comp_π
limitOpIsoOpColimit_hom_comp_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct limit CategoryTheory.Category.opposite CategoryTheory.Functor.op hasLimit_op_of_hasColimit Opposite.op colimit CategoryTheory.Functor.obj CategoryTheory.Iso.hom limitOpIsoOpColimit Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver colimit.ι limit.π	—	hasLimit_op_of_hasColimit limitOpIsoOpColimit_inv_comp_π
limitOpIsoOpColimit_hom_comp_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite limit CategoryTheory.Functor.op hasLimit_op_of_hasColimit Opposite.op colimit CategoryTheory.Iso.hom limitOpIsoOpColimit CategoryTheory.Functor.obj Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver colimit.ι limit.π	—	hasLimit_op_of_hasColimit CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' limitOpIsoOpColimit_hom_comp_ι
limitOpIsoOpColimit_inv_comp_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct Opposite.op colimit limit CategoryTheory.Category.opposite CategoryTheory.Functor.op hasLimit_op_of_hasColimit CategoryTheory.Functor.obj CategoryTheory.Iso.inv limitOpIsoOpColimit limit.π Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver Opposite.unop colimit.ι	—	hasLimit_op_of_hasColimit limit.isoLimitCone_inv_π
limitOpIsoOpColimit_inv_comp_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite Opposite.op colimit limit CategoryTheory.Functor.op hasLimit_op_of_hasColimit CategoryTheory.Iso.inv limitOpIsoOpColimit CategoryTheory.Functor.obj limit.π Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver Opposite.unop colimit.ι	—	hasLimit_op_of_hasColimit CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' limitOpIsoOpColimit_inv_comp_π
limitRightOpIsoOpColimit_hom_comp_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct limit CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp hasLimit_rightOp_of_hasColimit Opposite.op colimit CategoryTheory.Functor.obj CategoryTheory.Iso.hom limitRightOpIsoOpColimit Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver colimit.ι limit.π Opposite.unop	—	hasLimit_rightOp_of_hasColimit limitRightOpIsoOpColimit_inv_comp_π
limitRightOpIsoOpColimit_hom_comp_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite limit CategoryTheory.Functor.rightOp hasLimit_rightOp_of_hasColimit Opposite.op colimit CategoryTheory.Iso.hom limitRightOpIsoOpColimit CategoryTheory.Functor.obj Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver colimit.ι limit.π Opposite.unop	—	hasLimit_rightOp_of_hasColimit CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' limitRightOpIsoOpColimit_hom_comp_ι
limitRightOpIsoOpColimit_inv_comp_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct Opposite.op colimit CategoryTheory.Category.opposite limit CategoryTheory.Functor.rightOp hasLimit_rightOp_of_hasColimit CategoryTheory.Functor.obj CategoryTheory.Iso.inv limitRightOpIsoOpColimit limit.π Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver colimit.ι	—	hasLimit_rightOp_of_hasColimit limit.isoLimitCone_inv_π
limitRightOpIsoOpColimit_inv_comp_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite Opposite.op colimit limit CategoryTheory.Functor.rightOp hasLimit_rightOp_of_hasColimit CategoryTheory.Iso.inv limitRightOpIsoOpColimit CategoryTheory.Functor.obj limit.π Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver colimit.ι	—	hasLimit_rightOp_of_hasColimit CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' limitRightOpIsoOpColimit_inv_comp_π
limitUnopIsoUnopColimit_hom_comp_ι 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct limit CategoryTheory.Functor.unop hasLimit_unop_of_hasColimit Opposite.unop colimit Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.Iso.hom limitUnopIsoUnopColimit Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver colimit.ι limit.π	—	hasLimit_unop_of_hasColimit limitUnopIsoUnopColimit_inv_comp_π
limitUnopIsoUnopColimit_hom_comp_ι_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct limit CategoryTheory.Functor.unop hasLimit_unop_of_hasColimit Opposite.unop colimit Opposite CategoryTheory.Category.opposite CategoryTheory.Iso.hom limitUnopIsoUnopColimit CategoryTheory.Functor.obj Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver colimit.ι limit.π	—	hasLimit_unop_of_hasColimit CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' limitUnopIsoUnopColimit_hom_comp_ι
limitUnopIsoUnopColimit_inv_comp_π 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop colimit Opposite CategoryTheory.Category.opposite limit CategoryTheory.Functor.unop hasLimit_unop_of_hasColimit CategoryTheory.Functor.obj CategoryTheory.Iso.inv limitUnopIsoUnopColimit limit.π Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver Opposite.op colimit.ι	—	hasLimit_unop_of_hasColimit limit.isoLimitCone_inv_π
limitUnopIsoUnopColimit_inv_comp_π_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop colimit Opposite CategoryTheory.Category.opposite limit CategoryTheory.Functor.unop hasLimit_unop_of_hasColimit CategoryTheory.Iso.inv limitUnopIsoUnopColimit CategoryTheory.Functor.obj limit.π Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver Opposite.op colimit.ι	—	hasLimit_unop_of_hasColimit CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' limitUnopIsoUnopColimit_inv_comp_π
ι_comp_colimitLeftOpIsoUnopLimit_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp colimit hasColimit_leftOp_of_hasLimit Opposite.unop limit colimit.ι CategoryTheory.Iso.hom colimitLeftOpIsoUnopLimit Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver limit.π	—	hasColimit_leftOp_of_hasLimit colimit.isoColimitCocone_ι_hom
ι_comp_colimitLeftOpIsoUnopLimit_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite CategoryTheory.Functor.leftOp colimit hasColimit_leftOp_of_hasLimit colimit.ι Opposite.unop limit CategoryTheory.Iso.hom colimitLeftOpIsoUnopLimit Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver limit.π	—	hasColimit_leftOp_of_hasLimit CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_comp_colimitLeftOpIsoUnopLimit_hom
ι_comp_colimitOpIsoOpLimit_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Category.opposite CategoryTheory.Functor.op colimit hasColimit_op_of_hasLimit Opposite.op limit colimit.ι CategoryTheory.Iso.hom colimitOpIsoOpLimit Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver Opposite.unop limit.π	—	hasColimit_op_of_hasLimit colimit.isoColimitCocone_ι_hom
ι_comp_colimitOpIsoOpLimit_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.Functor.op colimit hasColimit_op_of_hasLimit colimit.ι Opposite.op limit CategoryTheory.Iso.hom colimitOpIsoOpLimit Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver Opposite.unop limit.π	—	hasColimit_op_of_hasLimit CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_comp_colimitOpIsoOpLimit_hom
ι_comp_colimitRightOpIsoUnopLimit_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Category.opposite CategoryTheory.Functor.rightOp colimit hasColimit_rightOp_of_hasLimit Opposite.op limit colimit.ι CategoryTheory.Iso.hom colimitRightOpIsoUnopLimit Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver limit.π	—	hasColimit_rightOp_of_hasLimit colimit.isoColimitCocone_ι_hom
ι_comp_colimitRightOpIsoUnopLimit_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite CategoryTheory.Functor.obj CategoryTheory.Functor.rightOp colimit hasColimit_rightOp_of_hasLimit colimit.ι Opposite.op limit CategoryTheory.Iso.hom colimitRightOpIsoUnopLimit Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver limit.π	—	hasColimit_rightOp_of_hasLimit CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_comp_colimitRightOpIsoUnopLimit_hom
ι_comp_colimitUnopIsoOpLimit_hom 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.unop colimit hasColimit_unop_of_hasLimit Opposite.unop limit Opposite CategoryTheory.Category.opposite colimit.ι CategoryTheory.Iso.hom colimitUnopIsoOpLimit Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver Opposite.op limit.π	—	hasColimit_unop_of_hasLimit colimit.isoColimitCocone_ι_hom
ι_comp_colimitUnopIsoOpLimit_hom_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct CategoryTheory.Functor.obj CategoryTheory.Functor.unop colimit hasColimit_unop_of_hasLimit colimit.ι Opposite.unop limit Opposite CategoryTheory.Category.opposite CategoryTheory.Iso.hom colimitUnopIsoOpLimit Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver Opposite.op limit.π	—	hasColimit_unop_of_hasLimit CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' ι_comp_colimitUnopIsoOpLimit_hom
π_comp_colimitLeftOpIsoUnopLimit_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite limit colimit CategoryTheory.Functor.leftOp hasColimit_leftOp_of_hasLimit Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver limit.π CategoryTheory.Iso.inv colimitLeftOpIsoUnopLimit colimit.ι Opposite.op	—	hasColimit_leftOp_of_hasLimit ι_comp_colimitLeftOpIsoUnopLimit_hom
π_comp_colimitLeftOpIsoUnopLimit_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite limit Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver limit.π colimit CategoryTheory.Functor.leftOp hasColimit_leftOp_of_hasLimit CategoryTheory.Iso.inv colimitLeftOpIsoUnopLimit colimit.ι Opposite.op	—	hasColimit_leftOp_of_hasLimit CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_comp_colimitLeftOpIsoUnopLimit_inv
π_comp_colimitOpIsoOpLimit_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct Opposite.op CategoryTheory.Functor.obj limit colimit CategoryTheory.Category.opposite CategoryTheory.Functor.op hasColimit_op_of_hasLimit Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver limit.π CategoryTheory.Iso.inv colimitOpIsoOpLimit colimit.ι	—	hasColimit_op_of_hasLimit ι_comp_colimitOpIsoOpLimit_hom
π_comp_colimitOpIsoOpLimit_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor.obj limit Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver limit.π colimit CategoryTheory.Functor.op hasColimit_op_of_hasLimit CategoryTheory.Iso.inv colimitOpIsoOpLimit colimit.ι	—	hasColimit_op_of_hasLimit CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_comp_colimitOpIsoOpLimit_inv
π_comp_colimitRightOpIsoUnopLimit_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.CategoryStruct.opposite CategoryTheory.Category.toCategoryStruct Opposite.op CategoryTheory.Functor.obj CategoryTheory.Category.opposite limit colimit CategoryTheory.Functor.rightOp hasColimit_rightOp_of_hasLimit Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver limit.π CategoryTheory.Iso.inv colimitRightOpIsoUnopLimit colimit.ι Opposite.unop	—	hasColimit_rightOp_of_hasLimit ι_comp_colimitRightOpIsoUnopLimit_hom
π_comp_colimitRightOpIsoUnopLimit_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp Opposite CategoryTheory.Category.toCategoryStruct CategoryTheory.Category.opposite Opposite.op CategoryTheory.Functor.obj limit Quiver.Hom.op CategoryTheory.CategoryStruct.toQuiver limit.π colimit CategoryTheory.Functor.rightOp hasColimit_rightOp_of_hasLimit CategoryTheory.Iso.inv colimitRightOpIsoUnopLimit colimit.ι Opposite.unop	—	hasColimit_rightOp_of_hasLimit CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_comp_colimitRightOpIsoUnopLimit_inv
π_comp_colimitUnopIsoOpLimit_inv 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite limit colimit CategoryTheory.Functor.unop hasColimit_unop_of_hasLimit Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver limit.π CategoryTheory.Iso.inv colimitUnopIsoOpLimit colimit.ι	—	hasColimit_unop_of_hasLimit ι_comp_colimitUnopIsoOpLimit_hom
π_comp_colimitUnopIsoOpLimit_inv_assoc 📖	mathematical	—	CategoryTheory.CategoryStruct.comp CategoryTheory.Category.toCategoryStruct Opposite.unop CategoryTheory.Functor.obj Opposite CategoryTheory.Category.opposite limit Quiver.Hom.unop CategoryTheory.CategoryStruct.toQuiver limit.π colimit CategoryTheory.Functor.unop hasColimit_unop_of_hasLimit CategoryTheory.Iso.inv colimitUnopIsoOpLimit colimit.ι	—	hasColimit_unop_of_hasLimit CategoryTheory.Category.assoc Mathlib.Tactic.Reassoc.eq_whisker' π_comp_colimitUnopIsoOpLimit_inv

---

← Back to Index