opEquiv'_apply — Mathlib

English

The application of opEquiv' to a morphism f is computed by composing f with the corresponding shift morphism after converting via opEquiv.

Русский

Применение opEquiv' к морфизму f вычисляется через композицию f с соответствующим морфизмом сдвига после преобразования через opEquiv.

LaTeX

$$$$ opEquiv' n a a' h (f) = opEquiv n (f \\; ≫ (shiftFunctorAdd' C a n a' (by cutsat)).hom.app Y) $$$$

Lean4

theorem opEquiv'_apply {a' : ℤ} (f : ShiftedHom X Y a') (n a : ℤ) (h : n + a = a') :
    opEquiv' n a a' h f = opEquiv n (f ≫ (shiftFunctorAdd' C a n a' (by cutsat)).hom.app Y) := by rfl

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