Theorems · Theorem · category theory

CategoryTheory.GradedObject.Monoidal.rightUnitor_naturality

∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : DecidableEq I] [inst_4 : CategoryTheory.Limits.HasInitial C]
  [inst_5 :
    ∀ (X₁ : C),
      CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C)
        ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁)]
  {X X' : CategoryTheory.GradedObject I C} (φ : X ⟶ X'),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.Monoidal.tensorHom φ
        (CategoryTheory.CategoryStruct.id CategoryTheory.GradedObject.Monoidal.tensorUnit))
      (CategoryTheory.GradedObject.Monoidal.rightUnitor X').hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.Monoidal.rightUnitor X).hom φ

Defined in

Mathlib.CategoryTheory.GradedObject.Monoidal

Cited by

1 results in Mathlib

Foundations

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

Assumes

AddMonoidCategoryTheory.CategoryCategoryTheory.MonoidalCategoryDecidableEqCategoryTheory.Limits.HasInitialCategoryTheory.Limits.PreservesColimit