instPreservesBinaryBiproductEval — Mathlib

English

For every i, the evaluation functor at i preserves binary biproducts: eval_i(K ⊞ L) is isomorphic to eval_i(K) ⊞ eval_i(L).

Русский

Для каждого i функция оценки в i сохраняет бинарные би-продукты: eval_i(K ⊞ L) изоморфна eval_i(K) ⊞ eval_i(L).

LaTeX

$$$ \mathrm{eval}_i(K \oplus L) \cong \mathrm{eval}_i(K) \oplus \mathrm{eval}_i(L). $$$

Lean4

instance (i : ι) : PreservesBinaryBiproduct K L (eval C c i) :=
  preservesBinaryBiproduct_of_preservesBinaryProduct _

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