forget₂_linear

Mathlib.CategoryTheory.Action.Limits

URI: https://scilib.ai/kg/mathlib#Action.forget₂_linear

English

The forget₂ functor forget₂ (Action V G) → V is linear over R.

Русский

Функтор forget₂ (Action V G) → V линейный над R.

LaTeX

$$$\text{Forget}_2 (\mathrm{Action}(V,G))$ is $R$-linear$$

Lean4

instance forget₂_linear [HasForget V] : Functor.Linear R (forget₂ (Action V G) V) where

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

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

Разделы

Аффилиация

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