shiftIso_add'_inv_app — Mathlib

English

The inverse of shiftIso' expresses a factorization of the composed inverses through the shift functor and the additivity of shifts.

Русский

Обратное к shiftIso' выражает факторизацию через сдвиговую ферму и аддитивность сдвигов.

LaTeX

$$$$ (F.shiftIso n a a' ha').inv.app X ≈ (F.shiftIso n a a' ha').inv.app X $$$$

Lean4

theorem shiftIso_add'_inv_app (n m mn : A) (hnm : m + n = mn) (a a' a'' : A) (ha' : n + a = a') (ha'' : m + a' = a'')
    (X : C) :
    (F.shiftIso mn a a'' (by rw [← hnm, ← ha'', ← ha', add_assoc])).inv.app X =
      (F.shiftIso n a a' ha').inv.app X ≫
        ((F.shiftIso m a' a'' ha'').inv.app X)⟦n⟧' ≫ (shiftFunctorAdd' D m n mn hnm).inv.app ((F.functor a'').obj X) :=
  by simp [F.shiftIso_add' n m mn hnm a a' a'' ha' ha'']

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