linearCoyoneda_obj_additive

Mathlib.CategoryTheory.Linear.Yoneda

URI: https://scilib.ai/kg/mathlib#CategoryTheory.linearCoyoneda_obj_additive

English

Similarly, the Coyoneda construction yields an additive object for each Y ∈ Cᵒᵖ.

Русский

Аналогично Койоне́да-конструкция порождает аддитивный объект для каждого Y ∈ Cᵒᵖ.

LaTeX

$$$((\\text{linearCoyoneda}_R(C)).\\mathrm{obj}\\,Y) \\text{ is additive}$$$

Lean4

instance linearCoyoneda_obj_additive (Y : Cᵒᵖ) : ((linearCoyoneda R C).obj Y).Additive where

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

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

Разделы

Аффилиация

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