hom₁

Mathlib.Algebra.Homology.BifunctorHomotopy

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

Lean4

/-- Auxiliary definition for `mapBifunctorMapHomotopy₁`. -/
noncomputable def hom₁ (j j' : J) : (mapBifunctor K₁ K₂ F c).X j ⟶ (mapBifunctor L₁ L₂ F c).X j' :=
  HomologicalComplex₂.totalDesc _
    (fun i₁ i₂ _ =>
      ComplexShape.ε₁ c₁ c₂ c (c₁.prev i₁, i₂) •
        (F.map (h₁.hom i₁ (c₁.prev i₁))).app (K₂.X i₂) ≫
          (F.obj (L₁.X (c₁.prev i₁))).map (f₂.f i₂) ≫ ιMapBifunctorOrZero L₁ L₂ F c _ _ j')

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

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

Разделы

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

Аффилиация

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