map_inv_hom_id

Mathlib.CategoryTheory.Iso

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

English

For any f: X → Y, F.map inv f ≫ F.map f = id_{F.obj X} when f is an isomorphism.

Русский

Для любого f: X → Y, если f — изоморфизм, то F.map inv f ∘ F.map f = id_{F.obj X}.

LaTeX

$$$F.map(\\operatorname{inv} f) \\circ F.map f = \\mathrm{Id}_{F.obj X}$$$

Lean4

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

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

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

Разделы

Аффилиация

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