mk'' — Mathlib

English

Let E be an equivalence between categories C and D, and A an additive monoid equipped with a shift structure compatible with E. If there exists a natural transformation h from E.counitIso at A, then E carries a CommShift A structure.

Русский

Пусть E — эквивалентность между категориями C и D, и A — аддитивный моноид с допустимой на нём структурой сдвига, совместимой с E. Если существует натрансформация h из E.counitIso на A, тогда E получает структуру CommShift A.

LaTeX

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

Lean4

/-- Constructor for `Equivalence.CommShift`. -/
theorem mk'' (h : NatTrans.CommShift E.counitIso.hom A) : E.CommShift A :=
  have := mk' E.symm A (inferInstanceAs (NatTrans.CommShift E.counitIso.inv A))
  inferInstanceAs (E.symm.symm.CommShift A)

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