commShift_of_rightAdjoint — Mathlib

English

If G CommutativeShift A holds and adjunction F ⊣ G is given, then the right adjoint G inherits a commutative shift structure, yielding a CommShift on G.

Русский

Если у правой пары сопряжения есть структура CommShift и дано сопряжение F ⊣ G, то правая сторона G наследует структуру CommShift.

LaTeX

$$$[G.CommShift A] \text{ comes from the adjunction } adj$ via the construction $LeftAdjointCommShift$ and unit/counit maps.$$

Lean4

theorem commShift_of_rightAdjoint [G.CommShift A] :
    letI := adj.leftAdjointCommShift A
    adj.CommShift A :=
  by
  letI := adj.leftAdjointCommShift A
  refine CommShift.mk' _ _ ⟨fun a ↦ ?_⟩
  ext X
  dsimp
  simpa only [Functor.commShiftIso_id_hom_app, Functor.comp_obj, Functor.id_obj, id_comp,
    Functor.commShiftIso_comp_hom_app] using LeftAdjointCommShift.compatibilityUnit_iso adj a X

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