map

Mathlib.CategoryTheory.Idempotents.FunctorCategories

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Idempotents.KaroubiFunctorCategoryEmbedding.map

Lean4

/-- Tautological action on maps of the functor `Karoubi (J ⥤ C) ⥤ (J ⥤ Karoubi C)`. -/
@[simps]
def map {P Q : Karoubi (J ⥤ C)} (f : P ⟶ Q) : obj P ⟶ obj Q where app j := ⟨f.f.app j, congr_app f.comm j⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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