addCommMonoidHomOfHasBinaryBiproducts

Mathlib.CategoryTheory.Preadditive.OfBiproducts

URI: https://scilib.ai/kg/mathlib#CategoryTheory.SemiadditiveOfBinaryBiproducts.addCommMonoidHomOfHasBinaryBiproducts

Lean4

/-- In a category with binary biproducts, the morphisms form a commutative monoid. -/
def addCommMonoidHomOfHasBinaryBiproducts : AddCommMonoid (X ⟶ Y)
    where
  add := (· +ᵣ ·)
  add_assoc := (EckmannHilton.mul_assoc (isUnital_leftAdd X Y) (isUnital_rightAdd X Y) (distrib X Y)).assoc
  zero := 0
  zero_add := (isUnital_rightAdd X Y).left_id
  add_zero := (isUnital_rightAdd X Y).right_id
  add_comm := (EckmannHilton.mul_comm (isUnital_leftAdd X Y) (isUnital_rightAdd X Y) (distrib X Y)).comm
  nsmul :=
    letI : Add (X ⟶ Y) := ⟨(· +ᵣ ·)⟩;
    nsmulRec

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru