Theorems · Definition · category theory

CategoryTheory.GradedObject.Monoidal.tensorObjDesc

{I : Type u} →
  [inst : AddMonoid I] →
    {C : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          {X₁ X₂ : CategoryTheory.GradedObject I C} →
            [inst_3 : X₁.HasTensor X₂] →
              {A : C} →
                {k : I} →
                  ((i₁ i₂ : I) → i₁ + i₂ = k → (CategoryTheory.MonoidalCategoryStruct.tensorObj (X₁ i₁) (X₂ i₂) ⟶ A)) →
                    (CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂ k ⟶ A)

Constructor for morphisms from a tensor product of two graded objects.

Defined in

Mathlib.CategoryTheory.GradedObject.Monoidal

Cited by

7 results in Mathlib

Foundations

Depth 30 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

AddMonoidCategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.GradedObject.HasTensor