map_inv_map_hom_apply

Mathlib.CategoryTheory.Types.Basic

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

English

For f: X ≅ Y and x ∈ F.obj X, F.map f.inv (F.map f.hom x) = x; i.e., the inverse transport undoes the forward transport.

Русский

Для изоморфизма f: X ≅ Y и элемента x ∈ F.obj X: F.map f.inv (F.map f.hom x) = x.

LaTeX

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

Lean4

@[simp]
theorem map_inv_map_hom_apply (f : X ≅ Y) (x : F.obj X) : F.map f.inv (F.map f.hom x) = x :=
  congr_fun (F.mapIso f).hom_inv_id x

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

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

Разделы

Аффилиация

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