Theorems · Theorem · category theory

CategoryTheory.GradedObject.single_map_singleObjApplyIsoOfEq_hom

∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Limits.HasInitial C] [inst_2 : DecidableEq J] (j : J) {X Y : C} (f : X ⟶ Y) (i : J)
  (h : i = j),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.GradedObject.single j).map f i)
      (CategoryTheory.GradedObject.singleObjApplyIsoOfEq j Y i h).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.singleObjApplyIsoOfEq j X i h).hom f

Defined in

Mathlib.CategoryTheory.GradedObject.Single

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasInitialDecidableEq