instPreservesFiniteBiproductsTensorRight

English

For any object X, the functor tensorRight X preserves finite biproducts; i.e., tensoring on the right preserves finite biproducts.

Русский

Для любого объекта X функтор tensorRight X сохраняет конечные биопродукты; тензорирование справа сохраняет их.

LaTeX

$$$\\text{PreservesFiniteBiproducts}(\\mathrm{tensorRight}\\; X)$$$

Lean4

instance (X : C) : PreservesFiniteBiproducts (tensorRight X) where
  preserves
    {J} :=
    let ⟨_⟩ := nonempty_fintype J
    {
      preserves := fun {f} =>
        {
          preserves := fun {b} i =>
            ⟨isBilimitOfTotal _
                (by
                  dsimp
                  simp_rw [← tensorHom_id]
                  simp only [tensorHom_comp_tensorHom, Category.comp_id, ← sum_tensor, ← id_tensorHom_id,
                    IsBilimit.total i])⟩ } }

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