shift_map_op — Mathlib

English

The inverse component of the op-commShiftIso is the composition of the shift op iso on D, the inverse of FcommShift on X.unop, and the F.map on the inner op.

Русский

Обратная компонента op-commShiftIso совпадает с композицией shift op iso на D, обратным FcommShift на X.unop и F.map на внутреннее op.

LaTeX

$$$ (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 $$$

Lean4

@[reassoc]
theorem shift_map_op {X Y : C} (f : X ⟶ Y) (n : ℤ) :
    (F.map f).op⟦n⟧' = (F.op.commShiftIso n).inv.app _ ≫ (F.map (f.op⟦n⟧').unop).op ≫ (F.op.commShiftIso n).hom.app _ :=
  (NatIso.naturality_1 (F.op.commShiftIso n) f.op).symm

Похожие утверждения