mapBifunctorMap

Mathlib.Algebra.Homology.Bifunctor

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.mapBifunctorMap

Lean4

/-- The morphism `mapBifunctor K₁ K₂ F c ⟶ mapBifunctor L₁ L₂ F c` induced by
morphisms of complexes `K₁ ⟶ L₁` and `K₂ ⟶ L₂`. -/
noncomputable def mapBifunctorMap : mapBifunctor K₁ K₂ F c ⟶ mapBifunctor L₁ L₂ F c :=
  HomologicalComplex₂.total.map
    (((F.mapBifunctorHomologicalComplex c₁ c₂).map f₁).app K₂ ≫
      ((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).map f₂)
    c

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

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

Разделы

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

Аффилиация

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