Commit 2025-10-15 10:06 ff11cd51

View on Github →

chore(CategoryTheory/Limits/Opposites): split the file Limits.Opposites (#30517) This PR splits the file

Mathlib/CategoryTheory/Limits/Opposites.lean into
Mathlib/CategoryTheory/Limits/Opposites.lean
Mathlib/CategoryTheory/Limits/Shapes/Opposites/ This was suggested in a review of #30200.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean

Modified Mathlib/AlgebraicGeometry/Limits.lean

Modified Mathlib/CategoryTheory/Generator/Basic.lean

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

Modified Mathlib/CategoryTheory/Limits/FormalCoproducts.lean

Modified Mathlib/CategoryTheory/Limits/Opposites.lean

deleted def CategoryTheory.Limits.Cofan.op

deleted def CategoryTheory.Limits.CokernelCofork.IsColimit.ofπOp

deleted def CategoryTheory.Limits.CokernelCofork.IsColimit.ofπUnop

deleted def CategoryTheory.Limits.Fan.op

deleted def CategoryTheory.Limits.KernelFork.IsLimit.ofιOp

deleted def CategoryTheory.Limits.KernelFork.IsLimit.ofιUnop

deleted def CategoryTheory.Limits.PullbackCone.isLimitEquivIsColimitOp

deleted def CategoryTheory.Limits.PullbackCone.isLimitEquivIsColimitUnop

deleted def CategoryTheory.Limits.PullbackCone.op

deleted def CategoryTheory.Limits.PullbackCone.opUnop

deleted theorem CategoryTheory.Limits.PullbackCone.op_inl

deleted theorem CategoryTheory.Limits.PullbackCone.op_inr

deleted def CategoryTheory.Limits.PullbackCone.unop

deleted def CategoryTheory.Limits.PullbackCone.unopOp

deleted theorem CategoryTheory.Limits.PullbackCone.unop_inl

deleted theorem CategoryTheory.Limits.PullbackCone.unop_inr

deleted def CategoryTheory.Limits.PushoutCocone.isColimitEquivIsLimitOp

deleted def CategoryTheory.Limits.PushoutCocone.isColimitEquivIsLimitUnop

deleted def CategoryTheory.Limits.PushoutCocone.op

deleted def CategoryTheory.Limits.PushoutCocone.opUnop

deleted theorem CategoryTheory.Limits.PushoutCocone.op_fst

deleted theorem CategoryTheory.Limits.PushoutCocone.op_snd

deleted def CategoryTheory.Limits.PushoutCocone.unop

deleted def CategoryTheory.Limits.PushoutCocone.unopOp

deleted theorem CategoryTheory.Limits.PushoutCocone.unop_fst

deleted theorem CategoryTheory.Limits.PushoutCocone.unop_snd

deleted def CategoryTheory.Limits.cospanOp

deleted theorem CategoryTheory.Limits.desc_op_comp_opCoproductIsoProduct'_hom

deleted theorem CategoryTheory.Limits.desc_op_comp_opCoproductIsoProduct_hom

deleted theorem CategoryTheory.Limits.fst_opProdIsoCoprod_hom

deleted theorem CategoryTheory.Limits.hasCoproductsOfShape_of_opposite

deleted theorem CategoryTheory.Limits.hasCoproducts_of_opposite

deleted theorem CategoryTheory.Limits.hasFiniteCoproducts_of_opposite

deleted theorem CategoryTheory.Limits.hasFiniteProducts_of_opposite

deleted theorem CategoryTheory.Limits.hasProductsOfShape_of_opposite

deleted theorem CategoryTheory.Limits.hasProducts_of_opposite

deleted theorem CategoryTheory.Limits.has_cofiltered_limits_of_has_filtered_colimits_op

deleted theorem CategoryTheory.Limits.has_filtered_colimits_of_has_cofiltered_limits_op

deleted theorem CategoryTheory.Limits.inl_opProdIsoCoprod_inv

deleted theorem CategoryTheory.Limits.inr_opProdIsoCoprod_inv

deleted def CategoryTheory.Limits.opCoproductIsoProduct'

deleted theorem CategoryTheory.Limits.opCoproductIsoProduct'_comp_self

deleted theorem CategoryTheory.Limits.opCoproductIsoProduct'_hom_comp_proj

deleted theorem CategoryTheory.Limits.opCoproductIsoProduct'_inv_comp_inj

deleted def CategoryTheory.Limits.opCoproductIsoProduct

deleted theorem CategoryTheory.Limits.opCoproductIsoProduct_hom_comp_π

deleted theorem CategoryTheory.Limits.opCoproductIsoProduct_inv_comp_ι

deleted def CategoryTheory.Limits.opCospan

deleted def CategoryTheory.Limits.opProdIsoCoprod

deleted theorem CategoryTheory.Limits.opProdIsoCoprod_hom_fst

deleted theorem CategoryTheory.Limits.opProdIsoCoprod_hom_snd

deleted theorem CategoryTheory.Limits.opProdIsoCoprod_inv_inl

deleted theorem CategoryTheory.Limits.opProdIsoCoprod_inv_inr

deleted def CategoryTheory.Limits.opProductIsoCoproduct'

deleted theorem CategoryTheory.Limits.opProductIsoCoproduct'_comp_self

deleted theorem CategoryTheory.Limits.opProductIsoCoproduct'_inv_comp_lift

deleted def CategoryTheory.Limits.opProductIsoCoproduct

deleted theorem CategoryTheory.Limits.opProductIsoCoproduct_inv_comp_lift

deleted def CategoryTheory.Limits.opSpan

deleted theorem CategoryTheory.Limits.proj_comp_opProductIsoCoproduct'_hom

deleted theorem CategoryTheory.Limits.pullbackIsoUnopPushout_hom_inl

deleted theorem CategoryTheory.Limits.pullbackIsoUnopPushout_hom_inr

deleted theorem CategoryTheory.Limits.pullbackIsoUnopPushout_inv_fst

deleted theorem CategoryTheory.Limits.pullbackIsoUnopPushout_inv_snd

deleted theorem CategoryTheory.Limits.pushoutIsoUnopPullback_inl_hom

deleted theorem CategoryTheory.Limits.pushoutIsoUnopPullback_inr_hom

deleted theorem CategoryTheory.Limits.pushoutIsoUnopPullback_inv_fst

deleted theorem CategoryTheory.Limits.pushoutIsoUnopPullback_inv_snd

deleted theorem CategoryTheory.Limits.snd_opProdIsoCoprod_hom

deleted def CategoryTheory.Limits.spanOp

deleted theorem CategoryTheory.Limits.π_comp_opProductIsoCoproduct_hom

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

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

Created Mathlib/CategoryTheory/Limits/Shapes/Opposites/Filtered.lean

added theorem CategoryTheory.Limits.has_cofiltered_limits_of_has_filtered_colimits_op

added theorem CategoryTheory.Limits.has_filtered_colimits_of_has_cofiltered_limits_op

Created Mathlib/CategoryTheory/Limits/Shapes/Opposites/Kernels.lean

added def CategoryTheory.Limits.CokernelCofork.IsColimit.ofπOp

added def CategoryTheory.Limits.CokernelCofork.IsColimit.ofπUnop

added def CategoryTheory.Limits.KernelFork.IsLimit.ofιOp

added def CategoryTheory.Limits.KernelFork.IsLimit.ofιUnop

Created Mathlib/CategoryTheory/Limits/Shapes/Opposites/Products.lean

added def CategoryTheory.Limits.Cofan.op

added def CategoryTheory.Limits.Fan.op

added theorem CategoryTheory.Limits.desc_op_comp_opCoproductIsoProduct'_hom

added theorem CategoryTheory.Limits.desc_op_comp_opCoproductIsoProduct_hom

added theorem CategoryTheory.Limits.fst_opProdIsoCoprod_hom

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.hasProductsOfShape_of_opposite

added theorem CategoryTheory.Limits.hasProducts_of_opposite

added theorem CategoryTheory.Limits.inl_opProdIsoCoprod_inv

added theorem CategoryTheory.Limits.inr_opProdIsoCoprod_inv

added def CategoryTheory.Limits.opCoproductIsoProduct'

added theorem CategoryTheory.Limits.opCoproductIsoProduct'_comp_self

added theorem CategoryTheory.Limits.opCoproductIsoProduct'_hom_comp_proj

added theorem CategoryTheory.Limits.opCoproductIsoProduct'_inv_comp_inj

added def CategoryTheory.Limits.opCoproductIsoProduct

added theorem CategoryTheory.Limits.opCoproductIsoProduct_hom_comp_π

added theorem CategoryTheory.Limits.opCoproductIsoProduct_inv_comp_ι

added def CategoryTheory.Limits.opProdIsoCoprod

added theorem CategoryTheory.Limits.opProdIsoCoprod_hom_fst

added theorem CategoryTheory.Limits.opProdIsoCoprod_hom_snd

added theorem CategoryTheory.Limits.opProdIsoCoprod_inv_inl

added theorem CategoryTheory.Limits.opProdIsoCoprod_inv_inr

added def CategoryTheory.Limits.opProductIsoCoproduct'

added theorem CategoryTheory.Limits.opProductIsoCoproduct'_comp_self

added theorem CategoryTheory.Limits.opProductIsoCoproduct'_inv_comp_lift

added def CategoryTheory.Limits.opProductIsoCoproduct

added theorem CategoryTheory.Limits.opProductIsoCoproduct_inv_comp_lift

added theorem CategoryTheory.Limits.proj_comp_opProductIsoCoproduct'_hom

added theorem CategoryTheory.Limits.snd_opProdIsoCoprod_hom

added theorem CategoryTheory.Limits.π_comp_opProductIsoCoproduct_hom

Created Mathlib/CategoryTheory/Limits/Shapes/Opposites/Pullbacks.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 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/Sites/Hypercover/Homotopy.lean

Modified Mathlib/CategoryTheory/Sites/Preserves.lean

Modified Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean

Modified Mathlib/Topology/Category/CompHausLike/SigmaComparison.lean

Modified Mathlib/Topology/Category/TopCat/Yoneda.lean