subsingleton_preadditive_of_hasBinaryBiproducts

English

The existence of binary biproducts implies there is at most one preadditive structure on the category.

Русский

Существование бинарных биопродуктов означает, что предадитивная структура в категории единственна (подтип).

LaTeX

$$Subsingleton (Preadditive C)$$

Lean4

/-- The existence of binary biproducts implies that there is at most one preadditive structure. -/
instance subsingleton_preadditive_of_hasBinaryBiproducts {C : Type u} [Category.{v} C] [HasZeroMorphisms C]
    [HasBinaryBiproducts C] : Subsingleton (Preadditive C) where
  allEq := fun a b => by
    apply Preadditive.ext; funext X Y; apply AddCommGroup.ext; funext f g
    have h₁ :=
      @biprod.add_eq_lift_id_desc _ _ a _ _ f g (by convert (inferInstance : HasBinaryBiproduct X X); subsingleton)
    have h₂ :=
      @biprod.add_eq_lift_id_desc _ _ b _ _ f g (by convert (inferInstance : HasBinaryBiproduct X X); subsingleton)
    refine h₁.trans (Eq.trans ?_ h₂.symm)
    congr! 2 <;> subsingleton

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