Commit 2026-02-18 23:09 2ace7b90

View on Github →

chore(CategoryTheory/Limits): dualize (parts of) pullback.diagonal (#35454) We add the definition pushout.codiagonal, some API and prove one square is a pushout square.

Estimated changes

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

added theorem CategoryTheory.Limits.isPushout_map_codiagonal

added theorem CategoryTheory.Limits.pushout.inl_codiagonal

added theorem CategoryTheory.Limits.pushout.inr_codiagonal

added theorem CategoryTheory.Limits.pushout.isIso_codiagonal_iff

added theorem CategoryTheory.Limits.pushout.op_codiagonal

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

added theorem CategoryTheory.IsPullback.op_iff

added theorem CategoryTheory.IsPullback.unop_iff

added theorem CategoryTheory.IsPushout.op_iff

added theorem CategoryTheory.IsPushout.unop_iff