inv_hom_id_app_apply

Mathlib.CategoryTheory.Types.Basic

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

English

For α: F ≅ G, X, x ∈ F.obj X, we have α.inv.app X (α.hom.app X x) = x; transport along hom then inv recovers the original.

Русский

Для α: F ≅ G, X и x ∈ F.obj X: α.inv.app X (α.hom.app X x) = x.

LaTeX

$$$$ \alpha_{\text{inv}}(X) (\alpha_{\text{hom}}(X) x) = x. $$$$

Lean4

@[simp]
theorem inv_hom_id_app_apply (α : F ≅ G) (X) (x) : α.hom.app X (α.inv.app X x) = x :=
  congr_fun (α.inv_hom_id_app X) x

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

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

Разделы

Аффилиация

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