commShift_of_functor — Mathlib

English

If E is an equivalence and E admits a CommShift structure with respect to A, then E carries a CommShift A structure (via its inverse).

Русский

Если эквивалентность E поддерживает структуру CommShift относительно A, то E обладает структурой CommShift A (через свою обратную эквивалентность).

LaTeX

$$$E\\,\\mathrm{CommShift}(A)$$$

Lean4

theorem commShift_of_functor [E.functor.CommShift A] :
    letI := E.commShiftInverse A
    E.CommShift A :=
  by
  letI := E.commShiftInverse A
  exact CommShift.mk' _ _ (E.toAdjunction.commShift_of_leftAdjoint A).commShift_unit

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