instCartesianMonoidalCategory

Mathlib.CategoryTheory.Monoidal.Grp_

URI: https://scilib.ai/kg/mathlib#Grp_.instCartesianMonoidalCategory

Lean4

instance instCartesianMonoidalCategory : CartesianMonoidalCategory (Grp_ C)
    where
  isTerminalTensorUnit := .ofUniqueHom (fun G ↦ toUnit G.toMon) fun G f ↦ by ext; exact toUnit_unique ..
  fst G H := fst G.toMon H.toMon
  snd G H := snd G.toMon H.toMon
  tensorProductIsBinaryProduct G
    H := BinaryFan.IsLimit.mk _ (fun {T} f g ↦ .mk (lift f.hom g.hom)) (by aesop_cat) (by aesop_cat) (by aesop_cat)
  fst_def G H := Mon.Hom.ext <| fst_def _ _
  snd_def G H := Mon.Hom.ext <| snd_def _ _

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

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

Разделы

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

Аффилиация

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