English
HasGoodTrifunctor₁₂Obj asserts a compatibility condition: for all i₁₂ and i₃, the functor G(-, X₃ i₃) preserves the colimits of the coproducts arising from the F₁₂ X₁ i₁, X₂ i₂.
Русский
HasGoodTrifunctor₁₂Obj требует совместимости: для всех i₁₂ и i₃ функтор G(-, X₃ i₃) сохраняет колимит coproduct-ов, возникающих из F₁₂ X₁ i₁ X₂ i₂.
LaTeX
$$$\text{HasGoodTrifunctor}_{12}\, r \;:\; \forall i_{12}, i_3, \; PreservesColimit (Discrete.functor (mapObjFun ((F_1 2 \otimes X_1) X_2) r_p i_{12}))\cdot ((Functor.flip G).obj (X_3 i_3))$$$
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 `G(-, X₃ i₃)` commutes with the coproducts of the `F₁₂(X₁ i₁, X₂ i₂)`
such that `ρ₁₂.p ⟨i₁, i₂⟩ = i₁₂`. -/
abbrev HasGoodTrifunctor₁₂Obj :=
∀ (i₁₂ : ρ₁₂.I₁₂) (i₃ : I₃),
PreservesColimit (Discrete.functor (mapObjFun (((mapBifunctor F₁₂ I₁ I₂).obj X₁).obj X₂) ρ₁₂.p i₁₂))
((Functor.flip G).obj (X₃ i₃))
