Commit 2025-04-14 03:47 15b14b24

View on Github →

feat(CategoryTheory): the dual of a Guitart exact 2-square is Guitart exact (#22447) This shall be used in order to formalize left derivability structures (dual to right derivability structures), and to construct left derived functors.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/CategoryTheory/Functor/TwoSquare.lean

added theorem CategoryTheory.TwoSquare.natTrans_op

added def CategoryTheory.TwoSquare.op

Created Mathlib/CategoryTheory/GuitartExact/Opposite.lean

added theorem CategoryTheory.TwoSquare.guitartExact_op_iff

added def CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence.functor

added def CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence.inverse

added def CategoryTheory.TwoSquare.structuredArrowRightwardsOpEquivalence

Modified Mathlib/CategoryTheory/Opposites.lean