bifunctorComp₁₂ — Mathlib

Lean4
/-- The construction `bifunctorComp₁₂` of a trifunctor by composition of bifunctors
is compatible with localization. -/
noncomputable def bifunctorComp₁₂ :
    Lifting₃ L₁ L₂ L₃ W₁ W₂ W₃ ((Functor.postcompose₃.obj L).obj (bifunctorComp₁₂ F₁₂ G)) (bifunctorComp₁₂ F₁₂' G')
    where
  iso :=
    ((whiskeringRight C₁ _ _).obj ((whiskeringRight C₂ _ _).obj ((whiskeringLeft _ _ D).obj L₃))).mapIso
        ((bifunctorComp₁₂Functor.mapIso (Lifting₂.iso L₁ L₂ W₁ W₂ (F₁₂ ⋙ (whiskeringRight _ _ _).obj L₁₂) F₁₂')).app
          G') ≪≫
      (bifunctorComp₁₂Functor.obj F₁₂).mapIso (Lifting₂.iso L₁₂ L₃ W₁₂ W₃ (G ⋙ (whiskeringRight _ _ _).obj L) G')
Похожие утверждения