English
The hom-component of the commShiftIso for F at X is given by a composite using F.map on the hom of the shift op iso on X and the op of the corresponding inv, mirroring the naturality of commShift.
Русский
Гом-компонента commShiftIso для F в X задаётся композицией через F.map на гом-часть shift-op-изоморфизма и op соответствующего inv, отражая натуральность commShift.
LaTeX
$$$ (F.op.commShiftIso n).hom.app X = (F.map ((shiftFunctorOpIso C n m h).hom.app X).unop).op ≫ ((F.commShiftIso m).inv.app X.unop).op ≫ (shiftFunctorOpIso D n m h).inv.app (op (F.obj X.unop)) $$$
Lean4
@[reassoc]
theorem op_commShiftIso_inv_app (X : Cᵒᵖ) (n m : ℤ) (h : n + m = 0) :
(F.op.commShiftIso n).inv.app X =
(shiftFunctorOpIso D n m h).hom.app (op (F.obj X.unop)) ≫
((F.commShiftIso m).hom.app X.unop).op ≫ (F.map ((shiftFunctorOpIso C n m h).inv.app X).unop).op :=
by
rw [← cancel_epi ((F.op.commShiftIso n).hom.app X), Iso.hom_inv_id_app, op_commShiftIso_hom_app _ X n m h, assoc,
assoc]
simp [← op_comp, ← F.map_comp]
