isoZero_hom_app_obj — Mathlib

English

In the induced shift sequence, the isoZero_hom_app_obj formula describes how the iso ZERO composed with shifts interacts with the starting object L.obj X.

Русский

В индуцированной последовательности сдвигов формула isoZero_hom_app_obj описывает взаимодействие нулевого изоморфизма сдвигов с исходным объектом L.obj X.

LaTeX

$$$(isoZero e M F' e').hom.app (L.obj X) = (e' 0).hom.app X ≫ (isoShiftZero G M).hom.app X ≫ e.inv.app X$$$

Lean4

theorem isoZero_hom_app_obj (X : C) :
    (isoZero e M F' e').hom.app (L.obj X) = (e' 0).hom.app X ≫ (isoShiftZero G M).hom.app X ≫ e.inv.app X :=
  NatTrans.congr_app (((whiskeringLeft C D A).obj L).map_preimage _) X

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