Commit 2025-01-03 11:53 a8f082c8

View on Github →

chore(CategoryTheory/Shift): fix NatTrans.CommShift (#20364) This PR improves some proofs about NatTrans.CommShift (the commutation of a natural transformation to shifts). The field comm' of NatTrans.CommShift had an unnecessary ' in it, it is renamed shift_comm, and API lemmas are moved from NatTrans.CommShift to the NatTrans namespace (where comm becomes shift_comm and comm_app becomes shift_app_comm).

Estimated changes

Modified Mathlib/CategoryTheory/Shift/Adjunction.lean

Modified Mathlib/CategoryTheory/Shift/CommShift.lean

deleted theorem CategoryTheory.NatTrans.CommShift.app_shift

deleted theorem CategoryTheory.NatTrans.CommShift.comm

deleted theorem CategoryTheory.NatTrans.CommShift.comm_app

deleted theorem CategoryTheory.NatTrans.CommShift.shift_app

added theorem CategoryTheory.NatTrans.app_shift

added theorem CategoryTheory.NatTrans.shift_app

added theorem CategoryTheory.NatTrans.shift_app_comm

added theorem CategoryTheory.NatTrans.shift_comm

Modified Mathlib/CategoryTheory/Shift/Quotient.lean

Modified Mathlib/CategoryTheory/Shift/SingleFunctors.lean

Modified Mathlib/CategoryTheory/Triangulated/Functor.lean