Commit 2025-11-17 00:03 dc6387b5

View on Github →

refactor(CategoryTheory/Shift): export Functor.CommShift.commShiftIso (#31504) The isomorphism of commutation with shifts Functor.CommShift.iso is renamed Functor.CommShift.commShiftIso and exported as Functor.commShiftIso (which was a definition previously). This allows to generate a few equational lemmas automatically. A few erw are also removed.

Estimated changes

Modified Mathlib/Algebra/Homology/HomotopyCategory/Shift.lean

Modified Mathlib/CategoryTheory/Shift/Adjunction.lean

modified theorem CategoryTheory.Adjunction.CommShift.mk'

Modified Mathlib/CategoryTheory/Shift/CommShift.lean

deleted def CategoryTheory.Functor.commShiftIso

deleted theorem CategoryTheory.Functor.commShiftIso_add

deleted theorem CategoryTheory.Functor.commShiftIso_comp_hom_app

deleted theorem CategoryTheory.Functor.commShiftIso_comp_inv_app

deleted theorem CategoryTheory.Functor.commShiftIso_id_hom_app

deleted theorem CategoryTheory.Functor.commShiftIso_id_inv_app

deleted theorem CategoryTheory.Functor.commShiftIso_zero

Modified Mathlib/CategoryTheory/Shift/Induced.lean

Modified Mathlib/CategoryTheory/Shift/Localization.lean

Modified Mathlib/CategoryTheory/Shift/Opposite.lean

Modified Mathlib/CategoryTheory/Shift/Pullback.lean

Modified Mathlib/CategoryTheory/Shift/Quotient.lean

Modified Mathlib/CategoryTheory/Shift/ShiftedHom.lean

Modified Mathlib/CategoryTheory/Triangulated/Functor.lean

Modified Mathlib/CategoryTheory/Triangulated/Opposite/Functor.lean