opShiftFunctorEquivalence_zero_unitIso_inv_app

English

In the zero-shift case, the inverse of the unit has an explicit expression via the op of the inverse of the zero functor and the op-shift isomorphism.

Русский

В случае нулевого сдвига выражение обратной единицы задаётся через оп-обратное нулевого функтор и изоморфизм сдвига.

LaTeX

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

Lean4

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

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