inv_left_hom_right

Mathlib.CategoryTheory.Comma.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Comma.inv_left_hom_right

English

For an isomorphism e in the comma category, we have L.map (inv e.left) ≫ X.hom ≫ R.map e.right = Y.hom.

Русский

Для изоморфизма e в комма‑категории выполняется L.map (inv e.left) ≫ X.hom ≫ R.map e.right = Y.hom.

LaTeX

$$$ L.map(\mathrm{inv}(e.left)) \; \circ X.hom \; \circ R.map(e.right) = Y.hom. $$$

Lean4

theorem inv_left_hom_right [IsIso e] : L.map (inv e.left) ≫ X.hom ≫ R.map e.right = Y.hom := by simp

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

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

Разделы

Аффилиация

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