pullbackShiftFunctorZero_inv_app — Mathlib

English

The inverse of the zero-shift functor on the pullback shift is compatible with the base zero-shift inverse via the pullback iso.

Русский

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

LaTeX

$$$ (shiftFunctorZero\\;\\_\\; A)^{-1}_{X} = (shiftFunctorZero\\; C\\; B)^{-1}_{X} \\circ (pullbackShiftIso\\; C\\; \\varphi\\; 0\\ 0\\ (by\\ simp))^{-1}_{X} $$$

Lean4

theorem pullbackShiftFunctorZero_inv_app :
    (shiftFunctorZero _ A).inv.app X =
      (shiftFunctorZero C B).inv.app X ≫ (pullbackShiftIso C φ 0 0 (by simp)).inv.app X :=
  by
  change (shiftFunctorZero C B).inv.app X ≫ _ = _
  dsimp [Discrete.eqToHom, Discrete.addMonoidalFunctor_ε]
  congr 2
  apply eqToHom_map

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