Commit 2026-02-17 21:47 bd255db5

View on Github →

chore(CategoryTheory/Limits): add instances for HasPullback f.op g.op and HasPushout f.op g.op (#35453) We also add some iff lemmas relating these and two lemmas computing the opposites of pullback.map and pushout.map.

Estimated changes

Modified Mathlib/CategoryTheory/Limits/HasLimits.lean

added theorem CategoryTheory.Limits.hasColimit_equivalence_comp_iff

added theorem CategoryTheory.Limits.hasColimit_inverse_equivalence_comp_iff

added theorem CategoryTheory.Limits.hasLimit_equivalence_comp_iff

added theorem CategoryTheory.Limits.hasLimit_inverse_equivalence_comp_iff

Modified Mathlib/CategoryTheory/Limits/Opposites.lean

added theorem CategoryTheory.Limits.hasColimit_leftOp_iff_hasLimit

added theorem CategoryTheory.Limits.hasColimit_op_iff_hasLimit

added theorem CategoryTheory.Limits.hasColimit_rightOp_iff_hasLimit

added theorem CategoryTheory.Limits.hasLimit_leftOp_iff_hasColimit

added theorem CategoryTheory.Limits.hasLimit_op_iff_hasColimit

added theorem CategoryTheory.Limits.hasLimit_rightOp_iff_hasColimit

Modified Mathlib/CategoryTheory/Limits/Shapes/Opposites/Pullbacks.lean

added def CategoryTheory.Limits.cospanUnop

added theorem CategoryTheory.Limits.hasPullback_op_iff_hasPushout

added theorem CategoryTheory.Limits.hasPullback_unop_iff_hasPushout

added theorem CategoryTheory.Limits.hasPushout_op_iff_hasPullback

added theorem CategoryTheory.Limits.hasPushout_unop_iff_hasPullback

added theorem CategoryTheory.Limits.op_pullbackMap

added theorem CategoryTheory.Limits.op_pushoutMap

modified theorem CategoryTheory.Limits.pullbackIsoOpPushout_hom_inl

modified theorem CategoryTheory.Limits.pullbackIsoOpPushout_hom_inr

modified theorem CategoryTheory.Limits.pullbackIsoOpPushout_inv_fst

modified theorem CategoryTheory.Limits.pullbackIsoOpPushout_inv_snd

modified theorem CategoryTheory.Limits.pullbackIsoUnopPushout_hom_inl

modified theorem CategoryTheory.Limits.pullbackIsoUnopPushout_hom_inr

modified theorem CategoryTheory.Limits.pullbackIsoUnopPushout_inv_fst

modified theorem CategoryTheory.Limits.pullbackIsoUnopPushout_inv_snd

modified theorem CategoryTheory.Limits.pushoutIsoOpPullback_inl_hom

modified theorem CategoryTheory.Limits.pushoutIsoOpPullback_inr_hom

modified theorem CategoryTheory.Limits.pushoutIsoOpPullback_inv_fst

modified theorem CategoryTheory.Limits.pushoutIsoOpPullback_inv_snd

modified theorem CategoryTheory.Limits.pushoutIsoUnopPullback_inl_hom

modified theorem CategoryTheory.Limits.pushoutIsoUnopPullback_inr_hom

modified theorem CategoryTheory.Limits.pushoutIsoUnopPullback_inv_fst

modified theorem CategoryTheory.Limits.pushoutIsoUnopPullback_inv_snd

added def CategoryTheory.Limits.spanUnop