associator_hom_app_app_app — Mathlib

English

Let L1, L2, L3 and the related localization data form a trifunctor setup; the hom component of the associator between the three functors, evaluated at objects X1, X2, X3, matches the corresponding lifted composite given by the chosen isomorphisms and liftings. This expresses a coherence between the two ways of rebracketing the triple composition under localization.

Русский

Пусть данные для тройной функторной композиции образуют конфигурацию локализации; гомоморфизм компонент ассоциатора между тремя функторaми, взятый на объектах X1, X2, X3, совпадает с соответствующим восходящим композитом, заданным выбранными изоморфизмами и подъёмами. Это выражает когеренцию двух способов скобочной расстановки тройной композиции в локализации.

LaTeX

$$$$\\text{(associator hom)}_{(L_1,L_2,L_3,L_{12},L_{23},W)}^{\\mathrm{hom}}((L_1 X_1) (L_2 X_2) (L_3 X_3)) = \\,\\text{(lifted composite via }G',F',\\ldots)$$$$

Lean4

theorem associator_hom_app_app_app (X₁ : C₁) (X₂ : C₂) (X₃ : C₃) :
    (((associator L₁ L₂ L₃ L₁₂ L₂₃ L W₁ W₂ W₃ W₁₂ W₂₃ iso F₁₂' G' F' G₂₃').hom.app (L₁.obj X₁)).app (L₂.obj X₂)).app
        (L₃.obj X₃) =
      (G'.map (((Lifting₂.iso L₁ L₂ W₁ W₂ (F₁₂ ⋙ (whiskeringRight C₂ C₁₂ D₁₂).obj L₁₂) F₁₂').hom.app X₁).app X₂)).app
          (L₃.obj X₃) ≫
        ((Lifting₂.iso L₁₂ L₃ W₁₂ W₃ (G ⋙ (whiskeringRight C₃ C D).obj L) G').hom.app ((F₁₂.obj X₁).obj X₂)).app X₃ ≫
          L.map (((iso.hom.app X₁).app X₂).app X₃) ≫
            ((Lifting₂.iso L₁ L₂₃ W₁ W₂₃ (F ⋙ (whiskeringRight _ _ _).obj L) F').inv.app X₁).app ((G₂₃.obj X₂).obj X₃) ≫
              (F'.obj (L₁.obj X₁)).map
                (((Lifting₂.iso L₂ L₃ W₂ W₃ (G₂₃ ⋙ (whiskeringRight _ _ _).obj L₂₃) G₂₃').inv.app X₂).app X₃) :=
  by
  dsimp [associator]
  rw [lift₃NatTrans_app_app_app]
  dsimp [Lifting₃.iso, Lifting₃.bifunctorComp₁₂, Lifting₃.bifunctorComp₂₃]
  simp only [Category.assoc]

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