commShift_adjunction_op_int — Mathlib

English

The zero-shift-induced unit-counit interplay on Opposite category yields a simple expression for the inverse app at X in Cᵒᵖ, via the op map of the unit and the inverse of the zero functor.

Русский

Единство и обратное для нулевого сдвига в противоположной категории даёт простое выражение для inv.app X через оп-отображение единицы и обратное нулевого функторa.

LaTeX

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

Lean4

noncomputable scoped instance commShift_adjunction_op_int {G : D ⥤ C} [G.CommShift ℤ] (adj : F ⊣ G)
    [Adjunction.CommShift adj ℤ] : Adjunction.CommShift adj.op ℤ :=
  by
  have eq :
    adj.op =
      PullbackShift.adjunction (AddMonoidHom.mk' (fun (n : ℤ) => -n) (by intros; dsimp; cutsat))
        (OppositeShift.adjunction ℤ adj) :=
    by
    ext
    dsimp [PullbackShift.adjunction, NatTrans.PullbackShift.natIsoId, NatTrans.PullbackShift.natIsoComp,
      PullbackShift.functor, PullbackShift.natTrans, OppositeShift.adjunction, OppositeShift.natTrans,
      NatTrans.OppositeShift.natIsoId, NatTrans.OppositeShift.natIsoComp, OppositeShift.functor]
    simp only [Category.comp_id, Category.id_comp]
  rw [eq]
  exact
    inferInstanceAs
      (Adjunction.CommShift
        (PullbackShift.adjunction (AddMonoidHom.mk' (fun (n : ℤ) => -n) (by intros; dsimp; cutsat))
          (OppositeShift.adjunction ℤ adj))
        ℤ)

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