instPreservesFiniteBiproductsTensorLeft

English

For any object X, the functor tensorLeft X preserves finite biproducts; i.e., it preserves finite coproducts and biproducts structure under tensoring with X.

Русский

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

LaTeX

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

Lean4

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

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