pullbackShiftFunctorZero_hom_app — Mathlib

English

The forward (hom) component of the zero-shift is compatible with the pullback shift iso in the expected factorization.

Русский

Прямой компонент hом нулевого сдвига совместим с изоморфизмом pullbackShift в ожидаемом разложении.

LaTeX

$$$ (shiftFunctorZero\;\_\; A).hom.app\ X = (pullbackShiftIso\; C\; \varphi\; 0\ 0\ (by\ simp)).hom.app\ X \;\gg\; (shiftFunctorZero\; C\; B).hom.app\ X $$$

Lean4

theorem pullbackShiftFunctorZero_hom_app :
    (shiftFunctorZero _ A).hom.app X =
      (pullbackShiftIso C φ 0 0 (by simp)).hom.app X ≫ (shiftFunctorZero C B).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

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