binaryProductLimitCone

Mathlib.Algebra.Category.Grp.CartesianMonoidal

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

Lean4

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

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

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

Разделы

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

Аффилиация

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