opShiftFunctorEquivalence_unitIso_hom_naturality

English

The naturality of the unit of the opShiftFunctorEquivalence with respect to morphisms in Cᵒᵖ holds after suitable reassociations; in particular f maps under the unit on Y with Y = X → Y obeys a commutativity relation.

Русский

Естественность единицы эквивалентности оп-сдвига под действием морфизмов в C^{op} сохраняется после перестановок скобок; в частности для f: X → Y выполняется нужная диаграмма.

LaTeX

$$$ f \\; \\gg (opShiftFunctorEquivalence\, C\, n).unitIso.hom.app Y = (opShiftFunctorEquivalence\, C\, n).unitIso.hom.app X \\; \\gg \\; (f⟦n⟧').unop\\;^n \\;\\gg \\; \\text{...}$$$

Lean4

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

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