shiftIso_add' — Mathlib

English

Inverse Application of shiftIso' respects the inverse shift composition with the right associator and counit of opShiftFunctorEquivalence.

Русский

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

LaTeX

$$$$ (F.shiftIso (n a' a'') ⋯).inv.app X = \\text{...} $$$$

Lean4

theorem shiftIso_add' (n m mn : A) (hnm : m + n = mn) (a a' a'' : A) (ha' : n + a = a') (ha'' : m + a' = a'') :
    F.shiftIso mn a a'' (by rw [← hnm, ← ha'', ← ha', add_assoc]) =
      isoWhiskerLeft _ (shiftFunctorAdd' D m n mn hnm) ≪≫
        (Functor.associator _ _ _).symm ≪≫ isoWhiskerRight (F.shiftIso m a' a'' ha'') _ ≪≫ F.shiftIso n a a' ha' :=
  by
  subst hnm
  rw [shiftFunctorAdd'_eq_shiftFunctorAdd, shiftIso_add]

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