mapHomologicalComplex

Mathlib.Algebra.Homology.Additive

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Equivalence.mapHomologicalComplex

Lean4

/-- An equivalence of categories induces an equivalences between the respective categories
of homological complex.
-/
@[simps]
def mapHomologicalComplex (e : W₁ ≌ W₂) [e.functor.PreservesZeroMorphisms] (c : ComplexShape ι) :
    HomologicalComplex W₁ c ≌ HomologicalComplex W₂ c
    where
  functor := e.functor.mapHomologicalComplex c
  inverse := e.inverse.mapHomologicalComplex c
  unitIso := (Functor.mapHomologicalComplexIdIso W₁ c).symm ≪≫ NatIso.mapHomologicalComplex e.unitIso c
  counitIso := NatIso.mapHomologicalComplex e.counitIso c ≪≫ Functor.mapHomologicalComplexIdIso W₂ c

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

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

Разделы

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

Аффилиация

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