instGroupoid

Mathlib.CategoryTheory.Action

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ActionCategory.instGroupoid

English

If G is a group acting on X, then ActionCategory G X is a groupoid (every morphism is invertible).

Русский

Если G — группа, действующая на X, то категория действий ActionCategory G X является группоидом (каждый морфизм обратим).

LaTeX

$$IsGroupoid(ActionCategory G X)$$

Lean4

instance : Groupoid (ActionCategory G X) :=
  CategoryTheory.groupoidOfElements _

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

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

Разделы

Аффилиация

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