hom_inv_apply

Mathlib.Algebra.Category.CommAlgCat.Basic

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

English

For an isomorphism e, the inverse-then-forward composition acts as identity on the carrier.

Русский

Для изоморфизма e композиция обратного и прямого отображает тождественный на носителе.

LaTeX

$$$e \circ e^{-1} = \mathrm{id}$ on the carrier$$

Lean4

theorem hom_inv_apply (e : A ≅ B) (x : B) : e.hom (e.inv x) = x := by simp

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

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

Разделы

Аффилиация

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