mapBifunctorMapHomotopy₁

Mathlib.Algebra.Homology.BifunctorHomotopy

URI: https://scilib.ai/kg/mathlib#HomologicalComplex.mapBifunctorMapHomotopy₁

Lean4

/-- The homotopy between `mapBifunctorMap f₁ f₂ F c` and `mapBifunctorMap f₁' f₂ F c` that
is induced by an homotopy between `f₁` and `f₁'`. -/
noncomputable def mapBifunctorMapHomotopy₁ : Homotopy (mapBifunctorMap f₁ f₂ F c) (mapBifunctorMap f₁' f₂ F c)
    where
  hom := hom₁ h₁ f₂ F c
  zero := zero₁ h₁ f₂ F c
  comm := comm₁ h₁ f₂ F c

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

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

Разделы

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

Аффилиация

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