opEquiv_symm_apply_comp — Mathlib

English

For f,g and degrees n,m, the inverse of opEquiv' applied to f and g comp h equals the composition of the inverses.

Русский

Для f,g и степеней n,m обратное к opEquiv' применённому к f и g с композицией h равно композиции обратных.

LaTeX

$$$ (opEquiv' n m q h)^{-1}(f \\circ g) = (opEquiv' m)^{-1} g \\circ (opEquiv' n)^{-1} f $$$

Lean4

theorem opEquiv_symm_apply_comp {X Y : C} {a : ℤ} (f : ShiftedHom (Opposite.op X) (Opposite.op Y) a) {b : ℤ} {Z : C}
    (z : ShiftedHom X Z b) {c : ℤ} (h : b + a = c) :
    ((ShiftedHom.opEquiv a).symm f).comp z h =
      (ShiftedHom.opEquiv a).symm (z.op ≫ f) ≫ (shiftFunctorAdd' C b a c h).inv.app Z :=
  by
  rw [ShiftedHom.opEquiv_symm_apply, ShiftedHom.opEquiv_symm_apply, ShiftedHom.comp]
  dsimp
  simp only [assoc, Functor.map_comp]

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