English
Relates the inverse of opEquiv' composed with op and shift to f.comp g with counit naturality. A technical identity in the opposite-shift framework.
Русский
Связь между обратным применением opEquiv' и операциями op и shift с учётом counit естественности.
LaTeX
$$$$ (opEquiv' n m q h)^{-1} (g.op ≫ (opShiftFunctorEquivalence C n).counitIso.inv.app _ ≫ f.op⟦n⟧') = f.comp g (by cutsat) $$$$
Lean4
theorem opEquiv'_symm_op_opShiftFunctorEquivalence_counitIso_inv_app_op_shift {n m : ℤ} (f : ShiftedHom X Y n)
(g : ShiftedHom Y Z m) (q : ℤ) (hq : n + m = q) :
(opEquiv' n m q hq).symm (g.op ≫ (opShiftFunctorEquivalence C n).counitIso.inv.app _ ≫ f.op⟦n⟧') =
f.comp g (by cutsat) :=
by
rw [opEquiv'_symm_apply, opEquiv_symm_apply]
dsimp [comp]
apply Quiver.Hom.op_inj
simp only [assoc, Functor.map_comp, op_comp, Quiver.Hom.op_unop, opShiftFunctorEquivalence_unitIso_inv_naturality]
erw [(opShiftFunctorEquivalence C n).inverse_counitInv_comp_assoc (Opposite.op Y)]
