instPreservesZeroMorphismsRepModuleCatFunctor

Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality

URI: https://scilib.ai/kg/mathlib#groupHomology.instPreservesZeroMorphismsRepModuleCatFunctor

English

For each n, the functor (functor k G n) preserves zero morphisms in Rep k G, i.e. it maps 0 to 0.

Русский

Для каждого n функтор (functor k G n) сохраняет нулевые морфизмы в Rep k G, отображая 0 в 0.

LaTeX

$$$ ( \text{functor } k G n).PreservesZeroMorphisms $$$

Lean4

instance (n : ℕ) : (functor k G n).PreservesZeroMorphisms where map_zero _ _ := by simp [map]

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

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

Разделы

Аффилиация

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