HasLeftTensor₃ObjExt — Mathlib

Lean4

/-- Given `Z : C` and three graded objects `X₁`, `X₂` and `X₃` in `GradedObject I C`,
this typeclass expresses that functor `Z ⊗ _` commutes with the coproduct of
the objects `X₁ i₁ ⊗ (X₂ i₂ ⊗ X₃ i₃)` such that `i₁ + i₂ + i₃ = j` for a certain `j`.
See lemma `left_tensor_tensorObj₃_ext`. -/
abbrev _root_.CategoryTheory.GradedObject.HasLeftTensor₃ObjExt (j : I) :=
  PreservesColimit
    (Discrete.functor fun (i : {i : (I × I × I) | i.1 + i.2.1 + i.2.2 = j}) ↦
      (((mapTrifunctor (bifunctorComp₂₃ (curriedTensor C) (curriedTensor C)) I I I).obj X₁).obj X₂).obj X₃ i)
    ((curriedTensor C).obj Z)

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