mapBifunctorAssociator — Mathlib

English

The injection coming from the left-hand leg interacts with the associator in a specified way, equating two composite morphisms.

Русский

Взаимодействие вводящего отображения слева с ассоциатором выражается равенством двух композиционных морфизмов.

LaTeX

$$$ιMapBifunctor₁₂BifunctorMapObj F₁₂ G ρ₁₂ X₁ X₂ X₃ i_1 i_2 i_3 j h \;\; {hom}$$$

Lean4

/-- Associator isomorphism for the action of bifunctors on graded objects. -/
noncomputable def mapBifunctorAssociator :
    mapBifunctorMapObj G ρ₁₂.q (mapBifunctorMapObj F₁₂ ρ₁₂.p X₁ X₂) X₃ ≅
      mapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) :=
  have := H₁₂.hasMap
  have := H₂₃.hasMap
  (mapBifunctorComp₁₂MapObjIso F₁₂ G ρ₁₂ X₁ X₂ X₃).symm ≪≫
    mapIso ((((mapTrifunctorMapIso associator I₁ I₂ I₃).app X₁).app X₂).app X₃) r ≪≫
      mapBifunctorComp₂₃MapObjIso F G₂₃ ρ₂₃ X₁ X₂ X₃

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