opShiftFunctorEquivalence_unitIso_inv_app_eq

English

The op-opposite of the hom component of shiftFunctorAdd' decomposes via op and inverse morphisms and the map by F on X.unop, consistent with op-shift isomorphisms.

Русский

Оппозиционный к обеим сторонам гомоморфизм shiftFunctorAdd' распадается через операции op и inverse и отображение F на X.unop, согласуясь с изоморфизмами оп-сдвига.

LaTeX

$$$ (\\text{shiftFunctorAdd'} \\; C^{op} a_1 a_2 a_3 h).hom.app X = (\\text{shiftFunctorOpIso } C a_3 b_3 h_3).hom.app X ≫ ((\\text{shiftFunctorAdd'} \\; C b_1 b_2 b_3 (by cutsat)).inv.app X.unop).op ≫ (\\text{shiftFunctorOpIso } C a_2 b_2 h_2).inv.app _ ≫ (\\text{shiftFunctor } C^{op} a_2).map ((\\text{shiftFunctorOpIso } C a_1 b_1 h_1).inv.app X) $$$

Lean4

theorem opShiftFunctorEquivalence_unitIso_inv_app_eq (X : Cᵒᵖ) (m n p : ℤ) (h : m + n = p) :
    (opShiftFunctorEquivalence C p).unitIso.inv.app X =
      (((shiftFunctorAdd' Cᵒᵖ n m p (by cutsat)).hom.app X).unop⟦p⟧').op ≫
        ((shiftFunctorAdd' C m n p h).inv.app _).op ≫
          (((opShiftFunctorEquivalence C m).unitIso.inv.app (X⟦n⟧)).unop⟦n⟧').op ≫
            (opShiftFunctorEquivalence C n).unitIso.inv.app X :=
  by
  rw [← cancel_mono ((opShiftFunctorEquivalence C p).unitIso.hom.app X), Iso.inv_hom_id_app,
    opShiftFunctorEquivalence_unitIso_hom_app_eq _ _ _ _ h, Category.assoc, Category.assoc, Category.assoc,
    Iso.inv_hom_id_app_assoc]
  apply Quiver.Hom.unop_inj
  dsimp
  simp only [Category.assoc, ← unop_comp, Iso.inv_hom_id_app, Functor.comp_obj, Functor.op_obj, unop_id, Functor.map_id,
    id_comp, ← Functor.map_comp, Iso.hom_inv_id_app]

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