English
Let C be a category equipped with shifts indexed by an additive commutative monoid A. For objects X in C and elements i, j in A, the isomorphism that swaps the order of shifting by i and then by j is inverted precisely by swapping i and j; i.e. (shiftComm X i j).symm = shiftComm X j i.
Русский
Пусть C — категория с сдвигами, индексированными по коммутативному моноиду A. Для объектов X и элементов i, j ∈ A, изоморфизм, меняющий порядок последовательных сдвигов на i и затем на j, имеет обратное равенство: (shiftComm X i j).symm = shiftComm X j i.
LaTeX
$$$ (shiftComm X i j).symm = shiftComm X j i $$$
Lean4
@[simp]
theorem shiftComm_symm (i j : A) : (shiftComm X i j).symm = shiftComm X j i :=
by
ext
exact NatTrans.congr_app (congr_arg Iso.hom (shiftFunctorComm_symm C i j)) X
