Commit 2023-03-11 16:29 3fcb15f5

View on Github →

feat: port CategoryTheory.Limits.Opposites (#2805)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Limits/Constructions/FiniteProductsOfBinaryProducts.lean

Modified Mathlib/CategoryTheory/Limits/EssentiallySmall.lean

Modified Mathlib/CategoryTheory/Limits/HasLimits.lean

modified def CategoryTheory.Limits.colimCoyoneda

modified theorem CategoryTheory.Limits.colimit.post_post

deleted theorem CategoryTheory.Limits.hasLimitsOfShapeOfEquivalence

added theorem CategoryTheory.Limits.hasLimitsOfShape_of_equivalence

modified theorem CategoryTheory.Limits.limit.id_pre

Created Mathlib/CategoryTheory/Limits/Opposites.lean

added def CategoryTheory.Limits.PullbackCone.isLimitEquivIsColimitOp

added def CategoryTheory.Limits.PullbackCone.isLimitEquivIsColimitUnop

added def CategoryTheory.Limits.PullbackCone.op

added def CategoryTheory.Limits.PullbackCone.opUnop

added theorem CategoryTheory.Limits.PullbackCone.op_inl

added theorem CategoryTheory.Limits.PullbackCone.op_inr

added def CategoryTheory.Limits.PullbackCone.unop

added def CategoryTheory.Limits.PullbackCone.unopOp

added theorem CategoryTheory.Limits.PullbackCone.unop_inl

added theorem CategoryTheory.Limits.PullbackCone.unop_inr

added def CategoryTheory.Limits.PushoutCocone.isColimitEquivIsLimitOp

added def CategoryTheory.Limits.PushoutCocone.isColimitEquivIsLimitUnop

added def CategoryTheory.Limits.PushoutCocone.op

added def CategoryTheory.Limits.PushoutCocone.opUnop

added theorem CategoryTheory.Limits.PushoutCocone.op_fst

added theorem CategoryTheory.Limits.PushoutCocone.op_snd

added def CategoryTheory.Limits.PushoutCocone.unop

added def CategoryTheory.Limits.PushoutCocone.unopOp

added theorem CategoryTheory.Limits.PushoutCocone.unop_fst

added theorem CategoryTheory.Limits.PushoutCocone.unop_snd

added def CategoryTheory.Limits.cospanOp

added theorem CategoryTheory.Limits.hasColimit_of_hasLimit_leftOp

added theorem CategoryTheory.Limits.hasColimit_of_hasLimit_op

added theorem CategoryTheory.Limits.hasColimitsOfShape_of_hasLimitsOfShape_op

added theorem CategoryTheory.Limits.hasColimits_of_hasLimits_op

added theorem CategoryTheory.Limits.hasCoproductsOfShape_of_opposite

added theorem CategoryTheory.Limits.hasCoproducts_of_opposite

added theorem CategoryTheory.Limits.hasFiniteCoproducts_of_opposite

added theorem CategoryTheory.Limits.hasFiniteProducts_of_opposite

added theorem CategoryTheory.Limits.hasLimit_of_hasColimit_leftOp

added theorem CategoryTheory.Limits.hasLimit_of_hasColimit_op

added theorem CategoryTheory.Limits.hasLimitsOfShape_of_hasColimitsOfShape_op

added theorem CategoryTheory.Limits.hasLimitsOfShape_op_of_hasColimitsOfShape

added theorem CategoryTheory.Limits.hasLimits_of_hasColimits_op

added theorem CategoryTheory.Limits.hasProductsOfShape_of_opposite

added theorem CategoryTheory.Limits.hasProducts_of_opposite

added theorem CategoryTheory.Limits.has_cofiltered_limits_of_has_filtered_colimits_op

added theorem CategoryTheory.Limits.has_filtered_colimits_of_has_cofiltered_limits_op

added def CategoryTheory.Limits.isColimitCoconeLeftOpOfCone

added def CategoryTheory.Limits.isColimitCoconeOfConeLeftOp

added def CategoryTheory.Limits.isColimitCoconeOfConeRightOp

added def CategoryTheory.Limits.isColimitCoconeRightOpOfCone

added def CategoryTheory.Limits.isColimitCoconeUnopOfCone

added def CategoryTheory.Limits.isColimitConeOfCoconeUnop

added def CategoryTheory.Limits.isColimitConeOp

added def CategoryTheory.Limits.isColimitConeUnop

added def CategoryTheory.Limits.isLimitCoconeOp

added def CategoryTheory.Limits.isLimitCoconeUnop

added def CategoryTheory.Limits.isLimitConeLeftOpOfCocone

added def CategoryTheory.Limits.isLimitConeOfCoconeLeftOp

added def CategoryTheory.Limits.isLimitConeOfCoconeRightOp

added def CategoryTheory.Limits.isLimitConeOfCoconeUnop

added def CategoryTheory.Limits.isLimitConeRightOpOfCocone

added def CategoryTheory.Limits.isLimitConeUnopOfCocone

added def CategoryTheory.Limits.opCospan

added def CategoryTheory.Limits.opSpan

added theorem CategoryTheory.Limits.pullbackIsoUnopPushout_hom_inl

added theorem CategoryTheory.Limits.pullbackIsoUnopPushout_hom_inr

added theorem CategoryTheory.Limits.pullbackIsoUnopPushout_inv_fst

added theorem CategoryTheory.Limits.pullbackIsoUnopPushout_inv_snd

added theorem CategoryTheory.Limits.pushoutIsoUnopPullback_inl_hom

added theorem CategoryTheory.Limits.pushoutIsoUnopPullback_inr_hom

added theorem CategoryTheory.Limits.pushoutIsoUnopPullback_inv_fst

added theorem CategoryTheory.Limits.pushoutIsoUnopPullback_inv_snd

added def CategoryTheory.Limits.spanOp

Modified Mathlib/CategoryTheory/Limits/Shapes/FiniteLimits.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/FiniteProducts.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/Products.lean

Modified Mathlib/CategoryTheory/Limits/Shapes/WidePullbacks.lean

modified def CategoryTheory.Limits.WidePullbackShape.evalCasesBash

modified def CategoryTheory.Limits.WidePullbackShape

modified def CategoryTheory.Limits.WidePushoutShape.evalCasesBash'

modified def CategoryTheory.Limits.WidePushoutShape