opShiftFunctorEquivalence_zero_unitIso_hom_app

English

The unit component for the zero shift in Opposite matches the op of the zero shift inverse component after applying shift zero maps.

Русский

Единичный компонент нулевого сдвига в Opposite совпадает с операцией противоположного нулевого сдвига после применения соответствующих отображений.

LaTeX

$$$ (opShiftFunctorEquivalence C 0).unitIso.hom.app X = ((shiftFunctorZero C \\mathbb{Z}).hom.app X.unop).op ≫ ((shiftFunctorZero C^{op} \\mathbb{Z}).inv.app X).unop^{{0}}.op $$$

Lean4

theorem opShiftFunctorEquivalence_zero_unitIso_hom_app (X : Cᵒᵖ) :
    (opShiftFunctorEquivalence C 0).unitIso.hom.app X =
      ((shiftFunctorZero C ℤ).hom.app X.unop).op ≫ (((shiftFunctorZero Cᵒᵖ ℤ).inv.app X).unop⟦(0 : ℤ)⟧').op :=
  by
  apply Quiver.Hom.unop_inj
  dsimp [opShiftFunctorEquivalence]
  rw [shiftFunctorZero_op_inv_app, unop_comp, Quiver.Hom.unop_op, Functor.map_comp,
    shiftFunctorCompIsoId_zero_zero_hom_app, assoc]

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