Commit 2026-05-23 12:42 5e77d5cf

View on Github →

chore(CategoryTheory/Limits): some API for binary (co)products (#39594) We add BinaryFan.IsLimit.lift as the analogue to Fan.IsLimit.lift and BinaryFan.isLimitMapConeEquiv as the analogue to Fan.isLimitMapConeEquiv. We also add the dual versions.

Estimated changes

Modified Mathlib/CategoryTheory/Adhesive/Basic.lean

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

Modified Mathlib/CategoryTheory/Limits/MonoCoprod.lean

Modified Mathlib/CategoryTheory/Limits/Preorder.lean

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

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

added def CategoryTheory.Limits.BinaryCofan.IsColimit.desc

added theorem CategoryTheory.Limits.BinaryCofan.IsColimit.inl_desc

added theorem CategoryTheory.Limits.BinaryCofan.IsColimit.inr_desc

added def CategoryTheory.Limits.BinaryCofan.isColimitMapConeEquiv

added theorem CategoryTheory.Limits.BinaryCofan.map_inl

added theorem CategoryTheory.Limits.BinaryCofan.map_inr

added def CategoryTheory.Limits.BinaryFan.IsLimit.lift

added theorem CategoryTheory.Limits.BinaryFan.IsLimit.lift_fst

added theorem CategoryTheory.Limits.BinaryFan.IsLimit.lift_snd

added def CategoryTheory.Limits.BinaryFan.isLimitMapConeEquiv

added theorem CategoryTheory.Limits.BinaryFan.map_fst

added theorem CategoryTheory.Limits.BinaryFan.map_snd

Modified Mathlib/CategoryTheory/Limits/Shapes/Pullback/IsPullback/Basic.lean

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

Modified Mathlib/CategoryTheory/Preadditive/Biproducts.lean