shiftIso_add_hom_app — Mathlib

English

Two morphisms between SingleFunctors are equal if their underlying hom components are equal.

Русский

Две отображения между SingleFunctors равны, если их одночлены гомоморфизмов совпадают.

LaTeX

$$$$ \\text{@[ext]}\\;\\forall f,g:\\mathrm{SingleFunctors}.Hom F G,\\; f.hom = g.hom \\Rightarrow f = g. $$$$

Lean4

theorem shiftIso_add_hom_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''])).hom.app X =
      (shiftFunctorAdd D m n).hom.app ((F.functor a'').obj X) ≫
        ((F.shiftIso m a' a'' ha'').hom.app X)⟦n⟧' ≫ (F.shiftIso n a a' ha').hom.app X :=
  by simp [F.shiftIso_add n m a a' a'' ha' ha'']

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