commShiftPullback — Mathlib

English

If an adjunction F ⊣ G is CommShift compatible, then its pullback along φ is also CommShift.

Русский

Если сопряжение F ⊣ G совместимо с CommShift, то его вытянутое по φ сопряжение также совместимо с CommShift.

LaTeX

$$instance commShiftPullback [adj.CommShift B] : (PullbackShift.adjunction φ adj).CommShift A$$

Lean4

/-- If an adjunction `F ⊣ G` is compatible with `CommShift` structures on `F` and `G`, then
it is also compatible with the pulled back `CommShift` structures by an additive map
`φ : B →+ A`.
-/
instance commShiftPullback [adj.CommShift B] : (PullbackShift.adjunction φ adj).CommShift A
    where
  commShift_unit := by
    dsimp [PullbackShift.adjunction]
    infer_instance
  commShift_counit := by
    dsimp [PullbackShift.adjunction]
    infer_instance

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