instHasForget

Mathlib.CategoryTheory.Action.Basic

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

English

There is a canonical HasForget structure on Action V G, relating Action V G to V via forgetful data.

Русский

Существует каноническая структура HasForget на Action V G, связывающая Action V G с V через данные забывания.

LaTeX

$$instance: HasForget (Action V G)$$

Lean4

instance [HasForget V] : HasForget (Action V G) where forget := forget V G ⋙ HasForget.forget

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

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

Разделы

Аффилиация

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