hom_inv_id_right

Mathlib.CategoryTheory.Comma.Arrow

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Arrow.hom_inv_id_right

English

For Iso e, e.hom.right ≫ e.inv.right = id on g.right.

Русский

Для изоморфизма e: e.hom.right ≫ e.inv.right = id_{g.right}.

LaTeX

$$$e.hom.right \circ e.inv.right = \mathrm{Id}_{g.right}$$$

Lean4

@[reassoc (attr := simp)]
theorem hom_inv_id_right (e : f ≅ g) : e.hom.right ≫ e.inv.right = 𝟙 _ := by rw [← comp_right, e.hom_inv_id, id_right]

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

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

Разделы

Аффилиация

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