op_commShiftIso_hom_app — Mathlib

English

An auxiliary equality for the zero-shift case, tying the unit-inverse inverse through the op-shift, consistent with prior lemmas.

Русский

Вспомогательное равенство для нулевого сдвига, связывающее единицу и обратное через оп-сдвиг, согласуется с предыдущими леммами.

LaTeX

$$$ (opShiftFunctorEquivalence C 0).unitIso.inv.app X = ((shiftFunctorZero C ℤ).hom.app X.unop).op ≫ (((shiftFunctorZero Cᵒᵖ ℤ).inv.app X).unop⟦0⟧').op $$$

Lean4

@[reassoc]
theorem op_commShiftIso_hom_app (X : Cᵒᵖ) (n m : ℤ) (h : n + m = 0) :
    (F.op.commShiftIso n).hom.app X =
      (F.map ((shiftFunctorOpIso C n m h).hom.app X).unop).op ≫
        ((F.commShiftIso m).inv.app X.unop).op ≫ (shiftFunctorOpIso D n m h).inv.app (op (F.obj X.unop)) :=
  by
  obtain rfl : m = -n := by cutsat
  rfl

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