pullbackShiftFunctorZero'_hom_app

English

A second variant of the zero-shift hom component factors through the pullback iso and the base zero shift hom.

Русский

Второй вариант гом-компоненты нулевого сдвига формируется через pullback-изоморфизм и гом-компонент нулевого сдвига базовой категории.

LaTeX

$$$ (shiftFunctorZero\; (PullbackShift\; C\; \varphi))^{hom}_{X} = (pullbackShiftIso\; C\; \varphi\ 0\ (\varphi 0)\ rfl)^{hom}_{X} \; \ggg\; (shiftFunctorZero'\; C\ (\varphi 0)\ (by rw[map_zero]))^{hom}_{X} $$$

Lean4

theorem pullbackShiftFunctorZero'_hom_app :
    (shiftFunctorZero _ A).hom.app X =
      (pullbackShiftIso C φ 0 (φ 0) rfl).hom.app X ≫ (shiftFunctorZero' C (φ 0) (by rw [map_zero])).hom.app X :=
  by
  rw [← cancel_epi ((shiftFunctorZero _ A).inv.app X), Iso.inv_hom_id_app, pullbackShiftFunctorZero'_inv_app, assoc,
    Iso.inv_hom_id_app_assoc, Iso.inv_hom_id_app]
  rfl

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