instId — Mathlib

English

The commShift construction for a left adjoint yields a compatible CommShift structure on the adjunction.

Русский

Конструкция CommShift для левого сопряжения образует совместимую структуру CommShift для этой пары.

LaTeX

$$$ \text{commShift_of_leftAdjoint}[F.CommShift A] : \text{adj.CommShift A}$$$

Lean4

/-- The identity adjunction is compatible with the trivial `CommShift` structure on the
identity functor.
-/
instance instId : (Adjunction.id (C := C)).CommShift A
    where
  commShift_counit := inferInstanceAs (NatTrans.CommShift (𝟭 C).leftUnitor.hom A)
  commShift_unit := inferInstanceAs (NatTrans.CommShift (𝟭 C).leftUnitor.inv A)

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