back_coe

Mathlib.CategoryTheory.Action

URI: https://scilib.ai/kg/mathlib#CategoryTheory.ActionCategory.back_coe

English

The backwards projection from ActionCategory M X to X exactly recovers the original object when viewed in the canonical embedding.

Русский

Обратная проекция восстанавливает исходный элемент через каноническое вложение.

LaTeX

$$$\text{back}_{ActionCategory} \circ (\text{coe}) = \mathrm{id}$$$

Lean4

@[simp]
theorem back_coe (x : ActionCategory M X) : ↑x.back = x := by cases x; rfl

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

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

Разделы

Аффилиация

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