map_hom_map_inv_apply

Mathlib.CategoryTheory.Types.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.FunctorToTypes.map_hom_map_inv_apply

English

For f: X ≅ Y and y ∈ F.obj Y, F.map f.hom (F.map f.inv y) = y; transporting back and forth along an isomorphism yields the original element.

Русский

Для f: X ≅ Y и y ∈ F.obj Y: F.map f.hom (F.map f.inv y) = y.

LaTeX

$$$$ F.map f.hom (F.map f.inv y) = y. $$$$

Lean4

@[simp]
theorem map_hom_map_inv_apply (f : X ≅ Y) (y : F.obj Y) : F.map f.hom (F.map f.inv y) = y :=
  congr_fun (F.mapIso f).inv_hom_id y

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

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

Разделы

Аффилиация

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