flipFunctor

Mathlib.Algebra.Homology.HomologicalBicomplex

URI: https://scilib.ai/kg/mathlib#HomologicalComplex₂.flipFunctor

Lean4

/-- Flipping a complex of complexes over the diagonal, as a functor. -/
@[simps]
def flipFunctor : HomologicalComplex₂ C c₁ c₂ ⥤ HomologicalComplex₂ C c₂ c₁
    where
  obj K := K.flip
  map {K L}
    f :=
    { f := fun i =>
        { f := fun j => (f.f j).f i
          comm' := by intros; simp }
      comm' := by intros; ext; simp }

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

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

Разделы

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

Аффилиация

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