opShiftFunctorEquivalence_counitIso_inv_naturality

English

Equational form of the unit-inverse identity: the equality of two expressions for the unit inverse component holds by naturality and functoriality.

Русский

Эквивалентная формула для единичной обратной компоненты сохраняется за счёт натуральности и функторности.

LaTeX

$$$ (opShiftFunctorEquivalence C n).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 $$$$

Lean4

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

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