Commit 2025-10-21 12:12 c3836ff4

View on Github →

feat(CategoryTheory/Limits/Opposites) : add opposites of coforks and forks (#30200) This PR adds missing definitions surrounding op and unop of coforks and forks. In CategoryTheory/Limits/Shapes/Equalizers.lean:

CoforkOfπ.ext : Adds an extensionality def corresponding to the existing ForkOfι.ext In CategoryTheory/Limits/Opposites.lean:
parallelPairOpIso: the dual behavior for parallelPair (similar to spanOp, cospanOp)
pullbackIsoOpPushout: the dual version of the existing pullbackIsoUnopPushout
Cofork.unop, Cofork.op, Fork.unop, Fork.op: define unop and op of Cofork and Fork
isColimitEquivIsLimitOp: A cofork in C is a colimit if and only if its opposite is limit in Cᵒᵖ
isColimitOfπEquivIsLimitOp: Cofork.ofπ π is colimit in C if and only if Fork.ofι π.op is limit in Cᵒᵖ
isColimitCoforkPushoutEquivIsColimitForkOpPullback: Cofork.ofπ f pullback.condition is colimit in C if and only if Fork.ofι f.op pushout.condition is limit in Cᵒᵖ. Relevant dual statements have also been added.

Estimated changes

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

added def CategoryTheory.Limits.CoforkOfπ.ext

added theorem CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_hom_app_op_one

added theorem CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_hom_app_op_zero

added theorem CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_inv_app_op_one

added theorem CategoryTheory.Limits.walkingParallelPairOpEquiv_counitIso_inv_app_op_zero

added theorem CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_hom_app_one

added theorem CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_hom_app_zero

added theorem CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_inv_app_one

added theorem CategoryTheory.Limits.walkingParallelPairOpEquiv_unitIso_inv_app_zero

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

added def CategoryTheory.Limits.Cofork.isColimitCoforkPushoutEquivIsColimitForkOpPullback

added def CategoryTheory.Limits.Cofork.isColimitCoforkPushoutEquivIsColimitForkUnopPullback

added def CategoryTheory.Limits.Cofork.isColimitEquivIsLimitOp

added def CategoryTheory.Limits.Cofork.isColimitEquivIsLimitUnop

added def CategoryTheory.Limits.Cofork.isColimitOfπEquivIsLimitOp

added def CategoryTheory.Limits.Cofork.isColimitOfπEquivIsLimitUnop

added def CategoryTheory.Limits.Cofork.ofπOpIsoOfι

added def CategoryTheory.Limits.Cofork.ofπUnopIsoOfι

added def CategoryTheory.Limits.Cofork.op

added def CategoryTheory.Limits.Cofork.opUnopIso

added theorem CategoryTheory.Limits.Cofork.op_unop_π

added theorem CategoryTheory.Limits.Cofork.op_ι

added theorem CategoryTheory.Limits.Cofork.op_π_app_one

added theorem CategoryTheory.Limits.Cofork.op_π_app_zero

added def CategoryTheory.Limits.Cofork.unop

added def CategoryTheory.Limits.Cofork.unopOpIso

added theorem CategoryTheory.Limits.Cofork.unop_op_π

added theorem CategoryTheory.Limits.Cofork.unop_ι

added theorem CategoryTheory.Limits.Cofork.unop_π_app_one

added theorem CategoryTheory.Limits.Cofork.unop_π_app_zero

added def CategoryTheory.Limits.Fork.isLimitEquivIsColimitOp

added def CategoryTheory.Limits.Fork.isLimitEquivIsColimitUnop

added def CategoryTheory.Limits.Fork.isLimitForkPushoutEquivIsColimitForkOpPullback

added def CategoryTheory.Limits.Fork.isLimitForkPushoutEquivIsColimitForkUnopPullback

added def CategoryTheory.Limits.Fork.isLimitOfιEquivIsColimitOp

added def CategoryTheory.Limits.Fork.isLimitOfιEquivIsColimitUnop

added def CategoryTheory.Limits.Fork.ofιOpIsoOfπ

added def CategoryTheory.Limits.Fork.ofιUnopIsoOfπ

added def CategoryTheory.Limits.Fork.op

added def CategoryTheory.Limits.Fork.opUnopIso

added theorem CategoryTheory.Limits.Fork.op_unop_ι

added theorem CategoryTheory.Limits.Fork.op_ι_app_one

added theorem CategoryTheory.Limits.Fork.op_ι_app_zero

added theorem CategoryTheory.Limits.Fork.op_π

added def CategoryTheory.Limits.Fork.unop

added def CategoryTheory.Limits.Fork.unopOpIso

added theorem CategoryTheory.Limits.Fork.unop_op_ι

added theorem CategoryTheory.Limits.Fork.unop_ι_app_one

added theorem CategoryTheory.Limits.Fork.unop_ι_app_zero

added theorem CategoryTheory.Limits.Fork.unop_π

added def CategoryTheory.Limits.opParallelPairIso

added theorem CategoryTheory.Limits.opParallelPairIso_hom_app_one

added theorem CategoryTheory.Limits.opParallelPairIso_hom_app_zero

added theorem CategoryTheory.Limits.opParallelPairIso_inv_app_one

added theorem CategoryTheory.Limits.opParallelPairIso_inv_app_zero

added def CategoryTheory.Limits.parallelPairOpIso

added theorem CategoryTheory.Limits.parallelPairOpIso_hom_app_one

added theorem CategoryTheory.Limits.parallelPairOpIso_hom_app_zero

added theorem CategoryTheory.Limits.parallelPairOpIso_inv_app_one

added theorem CategoryTheory.Limits.parallelPairOpIso_inv_app_zero

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

deleted def CategoryTheory.Limits.PullbackCone.opUnop

added def CategoryTheory.Limits.PullbackCone.opUnopIso

deleted def CategoryTheory.Limits.PullbackCone.unopOp

added def CategoryTheory.Limits.PullbackCone.unopOpIso

deleted def CategoryTheory.Limits.PushoutCocone.opUnop

added def CategoryTheory.Limits.PushoutCocone.opUnopIso

deleted def CategoryTheory.Limits.PushoutCocone.unopOp

added def CategoryTheory.Limits.PushoutCocone.unopOpIso

added theorem CategoryTheory.Limits.pullbackIsoOpPushout_hom_inl

added theorem CategoryTheory.Limits.pullbackIsoOpPushout_hom_inr

added theorem CategoryTheory.Limits.pullbackIsoOpPushout_inv_fst

added theorem CategoryTheory.Limits.pullbackIsoOpPushout_inv_snd

added theorem CategoryTheory.Limits.pushoutIsoOpPullback_inl_hom

added theorem CategoryTheory.Limits.pushoutIsoOpPullback_inr_hom

added theorem CategoryTheory.Limits.pushoutIsoOpPullback_inv_fst

added theorem CategoryTheory.Limits.pushoutIsoOpPullback_inv_snd