map_shift_unop — Mathlib

English

The operation of taking op on a morphism followed by a shift equals the composition of op of the mapped morphism, with the op of the shift isomorphisms, ensuring compatibility of the op- functor with shifts.

Русский

Операция взятия оп-на морфизму и последующего сдвига равна композиции оп отображения морфизма и оповых изоморфизмов сдвига, обеспечивая совместимость оп-функторa со сдвигами.

LaTeX

$$$ F.map ((f⟦n⟧').unop) = ((F.op.commShiftIso n).inv.app Y).unop ≫ ((F.map f.unop).op⟦n⟧').unop ≫ ((F.op.commShiftIso n).hom.app X).unop $$$

Lean4

@[reassoc]
theorem map_shift_unop {X Y : Cᵒᵖ} (f : X ⟶ Y) (n : ℤ) :
    F.map ((f⟦n⟧').unop) =
      ((F.op.commShiftIso n).inv.app Y).unop ≫ ((F.map f.unop).op⟦n⟧').unop ≫ ((F.op.commShiftIso n).hom.app X).unop :=
  by simp [shift_map_op]

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