mapBifunctorAssociatorX — Mathlib

Lean4

/-- The associator isomorphism for the action of bifunctors
on homological complexes, in each degree. -/
noncomputable def mapBifunctorAssociatorX [H₁₂ : HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄]
    [H₂₃ : HasGoodTrifunctor₂₃Obj F G₂₃ K₁ K₂ K₃ c₁₂ c₂₃ c₄] (j : ι₄) :
    (mapBifunctor (mapBifunctor K₁ K₂ F₁₂ c₁₂) K₃ G c₄).X j ≅ (mapBifunctor K₁ (mapBifunctor K₂ K₃ G₂₃ c₂₃) F c₄).X j :=
  (GradedObject.eval j).mapIso
    (GradedObject.mapBifunctorAssociator (associator := associator) (H₁₂ := H₁₂) (H₂₃ := H₂₃))

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