of_groupoid

Mathlib.CategoryTheory.Groupoid

URI: https://scilib.ai/kg/mathlib#CategoryTheory.IsIso.of_groupoid

English

In a groupoid, any morphism is an isomorphism; i.e., every arrow has an inverse.

Русский

В группеoid любой морфизм является изоморфизмом; то есть каждому ребру соответствует обратное.

LaTeX

$$$\\forall f : X \\to Y,\\; IsIso\\ f$$$

Lean4

instance (priority := 100) of_groupoid (f : X ⟶ Y) : IsIso f :=
  ⟨⟨Groupoid.inv f, Groupoid.comp_inv f, Groupoid.inv_comp f⟩⟩

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

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

Разделы

Аффилиация

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