Commit 2024-02-14 00:27 5eae4d85

View on Github →

feat(CategoryTheory): Guitart exact squares (#10270) This PR defines the categorical notion of 2-exact square in the sense of Guitart. It is introduced in order to prepare for future applications to derived functors.

Estimated changes

Modified Mathlib.lean

Created Mathlib/CategoryTheory/GuitartExact.lean

added def CategoryTheory.TwoSquare.EquivalenceJ.functor

added def CategoryTheory.TwoSquare.EquivalenceJ.inverse

added def CategoryTheory.TwoSquare.costructuredArrowRightwards

added def CategoryTheory.TwoSquare.equivalenceJ

added theorem CategoryTheory.TwoSquare.ext

added theorem CategoryTheory.TwoSquare.guitartExact_iff_final

added theorem CategoryTheory.TwoSquare.guitartExact_iff_initial

added theorem CategoryTheory.TwoSquare.guitartExact_iff_isConnected_downwards

added theorem CategoryTheory.TwoSquare.guitartExact_iff_isConnected_rightwards

added theorem CategoryTheory.TwoSquare.isConnected_rightwards_iff_downwards

added def CategoryTheory.TwoSquare.structuredArrowDownwards

added def CategoryTheory.TwoSquare

Modified Mathlib/CategoryTheory/IsConnected.lean

added theorem CategoryTheory.isConnected_iff_of_equivalence

added theorem CategoryTheory.isPreconnected_iff_of_equivalence

Modified docs/references.bib