inv_obj_hom_obj_of_iso

Mathlib.CategoryTheory.Category.Quiv

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Quiv.inv_obj_hom_obj_of_iso

English

The inverse of an isomorphism on objects brings the image back to the original object: e.inv.obj (e.hom.obj X) = X.

Русский

Обратный объект отображения возвращает изображение к исходному объекту: e.inv.obj (e.hom.obj X) = X.

LaTeX

$$$e.inv.obj (e.hom.obj X) = X$$$

Lean4

@[simp]
theorem inv_obj_hom_obj_of_iso (X : V) : e.inv.obj (e.hom.obj X) = X :=
  (equivOfIso e).left_inv X

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

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

Разделы

Аффилиация

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