Theorems · Theorem · category theory

CategoryTheory.GradedObject.Monoidal.tensorObj_ext

∀ {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} {j : I} (f g : CategoryTheory.GradedObject.Monoidal.tensorObj X₁ X₂ j ⟶ A),
  (∀ (i₁ i₂ : I) (hi : i₁ + i₂ = j),
      CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₁ X₂ i₁ i₂ j hi) f =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₁ X₂ i₁ i₂ j hi) g) →
    f = g

Defined in

Mathlib.CategoryTheory.GradedObject.Monoidal

Cited by

6 results in Mathlib

Foundations

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

Assumes

AddMonoidCategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.GradedObject.HasTensor