limitGroup

Mathlib.Algebra.Category.Grp.Limits

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

← MathLib Explorer

English

The limit cone for a functor into GrpCat exists and is a limit cone.

Русский

Предел-конус существует и является пределом для функторa в GrpCat.

LaTeX

$$$\\text{limitCone } F \\text{ is a limit cone}$$$

Lean4

@[to_additive]
noncomputable instance limitGroup : Group (Types.Small.limitCone.{v, u} (F ⋙ forget GrpCat.{u})).pt :=
  inferInstanceAs <| Group (Shrink (F ⋙ forget GrpCat.{u}).sections)

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

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

Разделы

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

Аффилиация

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