opShiftFunctorEquivalence_unitIso_inv_naturality

English

Dual naturality for the inverse component of the opShiftFunctorEquivalence: the inverse is natural with respect to morphisms in the opposite category, mirroring the forward naturality.

Русский

Двойственная натуральность для обратной составляющей.opShiftFunctorEquivalence: обратный естественен по отношению к морфизмам в противоположной категории.

LaTeX

$$$ f \\; \\Rightarrow \\; (opShiftFunctorEquivalence C n).unitIso.inv.app X $ commute with morphisms as in the naturality axiom.$$

Lean4

@[reassoc (attr := simp)]
theorem opShiftFunctorEquivalence_unitIso_inv_naturality (n : ℤ) {X Y : Cᵒᵖ} (f : X ⟶ Y) :
    (f⟦n⟧').unop⟦n⟧'.op ≫ (opShiftFunctorEquivalence C n).unitIso.inv.app Y =
      (opShiftFunctorEquivalence C n).unitIso.inv.app X ≫ f :=
  (opShiftFunctorEquivalence C n).unitIso.inv.naturality f

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