English
The projection from the colimit cocone to a component is compatible with the universal descent map, yielding an equality of the two ways of expressing a morphism from the cocone apex to A.
Русский
Проекция из кокона колимита совместима с универсальным отображением desc, давая равенство двух способов выражения морфизма из вершины кокона в A.
LaTeX
$$$$ιMapBifunctor₁₂BifunctorDesc f = f i_1 i_2 i_3 h$$$$
Lean4
/-- Given bifunctors `F : C₁ ⥤ C₂₃ ⥤ C₄`, `G₂₃ : C₂ ⥤ C₃ ⥤ C₂₃`, graded objects
`X₁ : GradedObject I₁ C₁`, `X₂ : GradedObject I₂ C₂`, `X₃ : GradedObject I₃ C₃` and
`ρ₂₃ : BifunctorComp₂₃IndexData r`, this asserts that for all `i₁ : I₁` and `i₂₃ : ρ₂₃.I₂₃`,
the functor `F(X₁ i₁, _)` commutes with the coproducts of the `G₂₃(X₂ i₂, X₃ i₃)`
such that `ρ₂₃.p ⟨i₂, i₃⟩ = i₂₃`. -/
abbrev HasGoodTrifunctor₂₃Obj :=
∀ (i₁ : I₁) (i₂₃ : ρ₂₃.I₂₃),
PreservesColimit (Discrete.functor (mapObjFun (((mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃) ρ₂₃.p i₂₃)) (F.obj (X₁ i₁))
