map_hom_inv_id

Mathlib.CategoryTheory.Iso

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Iso.map_hom_inv_id

English

For any f: X → Y, if f is an isomorphism, then F.map(inv f) = inv(F.map f).

Русский

Для любого f: X → Y, если f — изоморфизм, то F.map(inv f) = inv(F.map f).

LaTeX

$$$F.map(\\operatorname{inv} f) = \\operatorname{inv}(F.map f)$$$

Lean4

@[reassoc (attr := simp), grind =]
theorem map_hom_inv_id (F : C ⥤ D) : F.map e.hom ≫ F.map e.inv = 𝟙 _ := by grind

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

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

Разделы

Аффилиация

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