preservesCoLimit_curriedTensor — Mathlib

English

If for every object c in C the functor F preserves Colimits of tensoring with c on the right, then F preserves the curried tensor product functor curriedTensor C.

Русский

Если для каждого объекта c в C функция F сохраняет колимиты тензорирования справа на c, тогда F сохраняет кривую тензоризацию curriedTensor C.

LaTeX

$$$\\forall c:\\, C,\\; PreservesColimit\\ F\\ (\\text{tensorRight } c) \\;\\Rightarrow\\; PreservesColimit\\ F\\ (\\text{curriedTensor } C)$$$

Lean4

theorem preservesCoLimit_curriedTensor [h : ∀ c : C, PreservesColimit F (tensorRight c)] :
    PreservesColimit F (curriedTensor C) :=
  preservesColimit_of_evaluation _ _ (fun c ↦ inferInstanceAs (PreservesColimit F (tensorRight c)))

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