mapBifunctorAssociator — Mathlib

Lean4

/-- The associator isomorphism for the action of bifunctors
on homological complexes. -/
noncomputable def mapBifunctorAssociator :
    mapBifunctor (mapBifunctor K₁ K₂ F₁₂ c₁₂) K₃ G c₄ ≅ mapBifunctor K₁ (mapBifunctor K₂ K₃ G₂₃ c₂₃) F c₄ :=
  Hom.isoOfComponents (mapBifunctorAssociatorX associator K₁ K₂ K₃ c₁₂ c₂₃ c₄)
    (by
      intro j j' _
      simp only [mapBifunctor₁₂.d_eq, mapBifunctor₂₃.d_eq _ _ _ _ _ c₁₂, Preadditive.add_comp, Preadditive.comp_add,
        mapBifunctorAssociatorX_hom_D₁, mapBifunctorAssociatorX_hom_D₂, mapBifunctorAssociatorX_hom_D₃])

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