mapBifunctorComp₂₃MapObjIso — Mathlib

English

The cofan built from mapBifunctor maps is a colimit, i.e., it universalizes maps from its apex to any object A.

Русский

Кофан, построенный из отображений mapBifunctor, является колимитом: универсально описывает все гомоморфизмы от вершины к произвольному объекту A.

LaTeX

$$$$IsColimit (cofan₃MapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ j).$$$$

Lean4

/-- The action on graded objects of a trifunctor obtained by composition of two
bifunctors can be computed as a composition of the actions of these two bifunctors. -/
noncomputable def mapBifunctorComp₂₃MapObjIso :
    mapTrifunctorMapObj (bifunctorComp₂₃ F G₂₃) r X₁ X₂ X₃ ≅
      mapBifunctorMapObj F ρ₂₃.q X₁ (mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) :=
  isoMk _ _ (fun j => (CofanMapObjFun.iso (isColimitCofan₃MapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ j)).symm)

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