hom_inv_apply

Mathlib.Algebra.Category.ModuleCat.Basic

URI: https://scilib.ai/kg/mathlib#ModuleCat.hom_inv_apply

English

For an isomorphism e: M ≅ N and y ∈ N, e.hom(e.inv(y)) = y; i.e., e ∘ e^{-1} = id_N.

Русский

Для изоморфизма e: M ≅ N и элемента y ∈ N справедливо e.hom(e.inv(y)) = y; то есть e ∘ e^{-1} = id_N.

LaTeX

$$$ e( e^{-1}(y) ) = y \quad (y \in N) $$$

Lean4

theorem hom_inv_apply {M N : ModuleCat.{v} R} (e : M ≅ N) (x : N) : e.hom (e.inv x) = x := by simp

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

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

Разделы

Аффилиация

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