binaryProductLimitCone

Mathlib.Algebra.Category.Grp.Biproducts

URI: https://scilib.ai/kg/mathlib#AddCommGrpCat.binaryProductLimitCone

Lean4

/-- Construct limit data for a binary product in `AddCommGrpCat`, using
`AddCommGrpCat.of (G × H)`.
-/
@[simps! cone_pt isLimit_lift]
def binaryProductLimitCone (G H : AddCommGrpCat.{u}) : Limits.LimitCone (pair G H)
    where
  cone := BinaryFan.mk (ofHom (AddMonoidHom.fst G H)) (ofHom (AddMonoidHom.snd G H))
  isLimit :=
    BinaryFan.IsLimit.mk _ (fun l r => ofHom (AddMonoidHom.prod l.hom r.hom)) (fun _ _ => rfl) (fun _ _ => rfl)
      (by cat_disch)

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

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

Разделы

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

Аффилиация

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