extendFunctor

Mathlib.Algebra.Homology.Embedding.Extend

URI: https://scilib.ai/kg/mathlib#ComplexShape.Embedding.extendFunctor

Lean4

/-- Given an embedding `e : c.Embedding c'` of complex shapes, this is
the functor `HomologicalComplex C c ⥤ HomologicalComplex C c'` which
extend complexes along `e`: the extended complexes are zero
in the degrees that are not in the image of `e.f`. -/
@[simps]
noncomputable def extendFunctor [HasZeroMorphisms C] : HomologicalComplex C c ⥤ HomologicalComplex C c'
    where
  obj K := K.extend e
  map φ := HomologicalComplex.extendMap φ e

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

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

Разделы

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

Аффилиация

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