English
The commShift structure respects the composition of adjunctions: if adj and adj' are adjunctions, then their composition carries a compatible CommShift A structure.
Русский
Структура CommShift совместима с композицией сопряжений: если существуют сопряжения adj и adj', то их композиция обладает совместимой структурой CommShift A.
LaTeX
$$$ (adj.comp adj').CommShift A$$$
Lean4
/-- Constructor for `Adjunction.CommShift`. -/
theorem mk' (h : NatTrans.CommShift adj.unit A) : adj.CommShift A where
commShift_counit :=
⟨fun a ↦ by
ext
simp only [Functor.comp_obj, Functor.id_obj, NatTrans.comp_app, Functor.commShiftIso_comp_hom_app,
Functor.whiskerRight_app, assoc, Functor.whiskerLeft_app, Functor.commShiftIso_id_hom_app, comp_id]
refine (compatibilityCounit_of_compatibilityUnit adj _ _ (fun X ↦ ?_) _).symm
simpa only [NatTrans.comp_app, Functor.commShiftIso_id_hom_app, Functor.whiskerRight_app, id_comp,
Functor.commShiftIso_comp_hom_app] using congr_app (h.shift_comm a) X⟩
