groupoid — Mathlib

English

There is a groupoid structure on the single-object category of a group G, with inversion given by the group inverse and standard inverse laws.

Русский

На однообъектной категории G задана структура группоида: инверсия задана обратной элементу группы, выполняются стандартные свойства обратимости.

LaTeX

$$$ \text{Groupoid}(SingleObj G) \text{ with } inv(x)=x^{-1},\; inv\_comp = (mul\_inv\_cancel),\; comp\_inv=(inv\_mul\_cancel). $$$

Lean4

/-- Groupoid structure on `SingleObj M`. -/
@[stacks 0019]
instance groupoid : Groupoid (SingleObj G) where
  inv x := x⁻¹
  inv_comp := mul_inv_cancel
  comp_inv := inv_mul_cancel

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