hom_left_inv_left

Mathlib.CategoryTheory.Comma.Over.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Over.hom_left_inv_left

English

For an isomorphism e: f ≅ g in Over X, e.hom.left ≫ e.inv.left = id_{f.left}.

Русский

Для изоморфизма e: f ≅ g в Over X выполняется e.hom.left ∘ e.inv.left = id_{f.left}.

LaTeX

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

Lean4

@[reassoc (attr := simp)]
theorem hom_left_inv_left {f g : Over X} (e : f ≅ g) : e.hom.left ≫ e.inv.left = 𝟙 f.left := by simp [← Over.comp_left]

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

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

Разделы

Аффилиация

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