opShiftFunctorEquivalence_counitIso_hom_naturality

English

The inverse component at X in the opposite category is determined by composing the op of the forward component with the inverse of the shift-iso, aligning with the op-shift structure.

Русский

Обратная составляющая в X в противоположной категории задаётся композицией противоположной к прямой компоненте и обратного изоморфизма сдвига, согласуясь с оп-структурой сдвига.

LaTeX

$$$ (opShiftFunctorEquivalence C n).unitIso.inv.app X = ((shiftFunctor C n).map ((opShiftFunctorEquivalence C n).unitIso.inv.app X)).op \\; ≫ \\; (shiftFunctorOpIso C n 0 (zero_add 0)).inv.app X $$$

Lean4

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

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