shiftFunctorOpIso — Mathlib

English

If F and G are isomorphic and G is homological, then F is homological.

Русский

Если F и G изоморфны и G гомологичен, то F гомологичен.

LaTeX

$$$F \simeq G \Rightarrow F\text{ IsHomological}$$$

Lean4

/-- The shift functor on the opposite category identifies to the opposite functor
of a shift functor on the original category. -/
noncomputable def shiftFunctorOpIso (n m : ℤ) (hnm : n + m = 0) : shiftFunctor Cᵒᵖ n ≅ (shiftFunctor C m).op :=
  eqToIso
    (by
      obtain rfl : m = -n := by cutsat
      rfl)

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