shiftIso_inv_naturality — Mathlib

English

The inverse part of shiftIso satisfies naturality with respect to f: (F.shiftIso n).inv.app Y; f; equals X side through F.map and shiftFunctor.

Русский

Обратная часть shiftIso удовлетворяет натуральности по f: обсудим через F.map и shiftFunctor.

LaTeX

$$$\text{(F.shiftIso n).inv.app Y} \circ F.map(f^{\,n}) = F.map(f) \circ (F.shiftIso n a a' ha')^{-1}_{X}$$$

Lean4

@[reassoc]
theorem shiftIso_inv_naturality {X Y : C} (n a a' : M) (ha' : n + a = a') (f : X ⟶ Y) :
    (shift F a').map f ≫ (shiftIso F n a a' ha').inv.app Y =
      (shiftIso F n a a' ha').inv.app X ≫ (shift F a).map (f⟦n⟧') :=
  by simp

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