opShiftFunctorEquivalence — Mathlib

English

There exists a canonical autoequivalence of Cᵒᵖ given by shifting on the left and taking op on the right, with unit and counit described by two interlocking natural isomorphisms that encode shift compatibility.

Русский

Существует каноническая автоэквивалентность C^{op}, задаваемая сдвигом слева и операцией противоположной категории справа, с устройствами единицы и кофунктора, описывающими совместимость сдвигов.

LaTeX

$$$\\text{opShiftFunctorEquivalence} : C^{op} \\simeq C^{op}$ defined by$\\text{functor} = \\text{shiftFunctor} \\, C^{op} n$, $\\text{inverse} = (\\text{shiftFunctor } C n)^{op}$, with unit/counit given by the stated NatIso compositions.$$

Lean4

/-- The autoequivalence `Cᵒᵖ ≌ Cᵒᵖ` whose functor is `shiftFunctor Cᵒᵖ n` and whose inverse
functor is `(shiftFunctor C n).op`. Do not unfold the definitions of the unit and counit
isomorphisms: the compatibilities they satisfy are stated as separate lemmas. -/
@[simps functor inverse]
noncomputable def opShiftFunctorEquivalence (n : ℤ) : Cᵒᵖ ≌ Cᵒᵖ
    where
  functor := shiftFunctor Cᵒᵖ n
  inverse := (shiftFunctor C n).op
  unitIso :=
    NatIso.op (shiftFunctorCompIsoId C (-n) n n.add_left_neg) ≪≫
      Functor.isoWhiskerRight (shiftFunctorOpIso C n (-n) n.add_right_neg).symm (shiftFunctor C n).op
  counitIso :=
    Functor.isoWhiskerLeft _ (shiftFunctorOpIso C n (-n) n.add_right_neg) ≪≫
      NatIso.op (shiftFunctorCompIsoId C n (-n) n.add_right_neg).symm
  functor_unitIso_comp
    X :=
    Quiver.Hom.unop_inj
      (by
        dsimp [shiftFunctorOpIso]
        erw [comp_id, Functor.map_id, comp_id]
        change
          (shiftFunctorCompIsoId C n (-n) (add_neg_cancel n)).inv.app (X.unop⟦-n⟧) ≫
              ((shiftFunctorCompIsoId C (-n) n (neg_add_cancel n)).hom.app X.unop)⟦-n⟧' =
            𝟙 _
        rw [shift_shiftFunctorCompIsoId_neg_add_cancel_hom_app n X.unop, Iso.inv_hom_id_app])

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