instLinearHomologicalComplexQuotient

Mathlib.Algebra.Homology.HomotopyCategory

URI: https://scilib.ai/kg/mathlib#HomotopyCategory.instLinearHomologicalComplexQuotient

English

The quotient functor preserves linear structure, yielding a linear functor between additive categories.

Русский

Квотирующий функтор сохраняет линейную структуру между аддитивными категориями.

LaTeX

$$$\text{Linear}(\text{quotient})$$$

Lean4

instance [Linear R V] : Functor.Linear R (HomotopyCategory.quotient V c) :=
  Quotient.linear_functor _ _ _

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

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

Разделы

Аффилиация

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