hom_inv_id_left

Mathlib.CategoryTheory.Comma.Arrow

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

English

For Iso e, e.hom.left ≫ e.inv.left = id on f.left.

Русский

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

LaTeX

$$$e.hom.left \circ e.inv.left = \mathrm{Id}_{f.left}$$$

Lean4

@[reassoc (attr := simp)]
theorem hom_inv_id_left (e : f ≅ g) : e.hom.left ≫ e.inv.left = 𝟙 _ := by rw [← comp_left, e.hom_inv_id, id_left]

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

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

Разделы

Аффилиация

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