Commit 2024-06-04 08:15 9b24c0a2

View on Github →

feat(CategoryTheory): vertical composition of Guitart exact squares (#12627) This is esoteric category theory, but it shall be used in the formalization of derived functors.

Estimated changes

Modified Mathlib.lean

Renamed Mathlib/CategoryTheory/GuitartExact.lean to Mathlib/CategoryTheory/GuitartExact/Basic.lean

Created Mathlib/CategoryTheory/GuitartExact/VerticalComposition.lean

added theorem CategoryTheory.TwoSquare.GuitartExact.whiskerVertical

added theorem CategoryTheory.TwoSquare.GuitartExact.whiskerVertical_iff

added def CategoryTheory.TwoSquare.structuredArrowDownwardsComp

added def CategoryTheory.TwoSquare.vComp'

added def CategoryTheory.TwoSquare.vComp

added def CategoryTheory.TwoSquare.whiskerVertical

Modified Mathlib/CategoryTheory/Limits/Final.lean

deleted theorem CategoryTheory.Functor.final_comp

deleted theorem CategoryTheory.Functor.initial_comp