shiftIso_add_inv_app — Mathlib

English

Extensionality for Hom components ensures uniqueness of morphisms between SingleFunctors.

Русский

Унарное расширение гомоморфизмов обеспечивает уникальность отображений между SingleFunctors.

LaTeX

$$$$ \\text{[ext] } f,hg \\Rightarrow f.hom = g.hom \\Rightarrow f = g $$$$

Lean4

theorem shiftIso_add_inv_app (n m a a' a'' : A) (ha' : n + a = a') (ha'' : m + a' = a'') (X : C) :
    (F.shiftIso (m + n) a a'' (by rw [add_assoc, ha', ha''])).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).inv.app ((F.functor a'').obj X) :=
  by simp [F.shiftIso_add n m a a' a'' ha' ha'']

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