shiftIso_zero_inv_app — Mathlib

English

Inverse component for a zero-shift in the pulled-back setting aligns with the base inverse via the pullback iso.

Русский

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

LaTeX

$$$ (F.shiftIso 0 a a (zero_add a)).inv.app X = (F.shift a).map ((shiftFunctorZero C M).inv.app X) $$$

Lean4

@[simp]
theorem shiftIso_zero_inv_app (a : M) (X : C) :
    (F.shiftIso 0 a a (zero_add a)).inv.app X = (shift F a).map ((shiftFunctorZero C M).inv.app X) := by
  simp [F.shiftIso_zero a]

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