Theorems · Definition · category theory

CategoryTheory.GradedObject.HasTensor

{I : Type u} →
  [AddMonoid I] →
    {C : Type u_1} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [CategoryTheory.MonoidalCategory C] → CategoryTheory.GradedObject I C → CategoryTheory.GradedObject I C → Prop

The tensor product of two graded objects X₁ and X₂ exists if for any n, the coproduct of the objects X₁ i ⊗ X₂ j for i + j = n exists.

Defined in

Mathlib.CategoryTheory.GradedObject.Monoidal

Cited by

49 results in Mathlib

Foundations

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

Assumes

AddMonoidCategoryTheory.CategoryCategoryTheory.MonoidalCategory