leftDual_v

Mathlib.CategoryTheory.Action.Monoidal

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

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem leftDual_v [LeftRigidCategory V] : (ᘁX).V = ᘁX.V :=
  rfl

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

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

Разделы

Аффилиация

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