inv_left_hom_left

Mathlib.CategoryTheory.Comma.Over.Basic

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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