hasBiproductsOfShape_finite — Mathlib

English

If a category C has finite biproducts, then for every finite index set J, C has biproducts of shape J.

Русский

Если категория C имеет конечные би-произведения, то для любого конечного множества индексов J у C существуют бипродукты формы J.

LaTeX

$$$\text{HasFiniteBiproducts}(C) \land \text{Finite}(J) \Rightarrow \text{HasBiproductsOfShape}(J, C)$$$

Lean4

instance (priority := 100) hasBiproductsOfShape_finite [HasFiniteBiproducts C] [Finite J] : HasBiproductsOfShape J C :=
  by
  rcases Finite.exists_equiv_fin J with ⟨n, ⟨e⟩⟩
  haveI : HasBiproductsOfShape (Fin n) C := HasFiniteBiproducts.out n
  exact hasBiproductsOfShape_of_equiv C e

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