instComp — Mathlib

English

The identity adjunction carries a canonical CommShift structure, coming from the left unitor data on the identity functor.

Русский

Идентичное сопряжение имеет каноническую структуру CommShift, исходящую из левого унитора на тождественный функтор.

LaTeX

$$$ (\mathrm{Adjunction.id}(C)).CommShift A$$$

Lean4

/-- Compatibility of `Adjunction.Commshift` with the composition of adjunctions.
-/
instance instComp : (adj.comp adj').CommShift A
    where
  commShift_counit := by
    rw [comp_counit]
    infer_instance
  commShift_unit := by
    rw [comp_unit]
    infer_instance

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