rightDual_v

Mathlib.CategoryTheory.Action.Monoidal

URI: https://scilib.ai/kg/mathlib#Action.rightDual_v

English

For X in Action V H, the underlying right dual object matches the right dual of X’s underlying V-object.

Русский

Для X в Action V H правое двойственное над X совпадает с правым двойственным над базовым V-объектом X.

LaTeX

$$$X^{\mathrm{R}}.V = X.V^{\mathrm{R}}$$$

Lean4

@[simp]
theorem rightDual_v [RightRigidCategory V] : Xᘁ.V = X.Vᘁ :=
  rfl

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

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

Разделы

Аффилиация

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