The graded object in a single degree

In this file, we define the functor GradedObject.single j : C ⥤ GradedObject J C which sends an object X : C to the graded object which is X in degree j and the initial object of C in other degrees.

noncomputable def CategoryTheory.GradedObject.single {J : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Limits.HasInitial C] [DecidableEq J] (j : J) : Functor C (GradedObject J C)

The functor which sends X : C to the graded object which is X in degree j and the initial object in other degrees.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

noncomputable abbrev CategoryTheory.GradedObject.single₀ (J : Type u_1) {C : Type u_2} [Category.{v_1, u_2} C] [Limits.HasInitial C] [DecidableEq J] [Zero J] : Functor C (GradedObject J C)

The functor which sends X : C to the graded object which is X in degree 0 and the initial object in nonzero degrees.

Equations

• CategoryTheory.GradedObject.single₀ J = CategoryTheory.GradedObject.single 0

noncomputable def CategoryTheory.GradedObject.singleObjApplyIsoOfEq {J : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Limits.HasInitial C] [DecidableEq J] (j : J) (X : C) (i : J) (h : i = j) : (single j).obj X i ≅ X

The canonical isomorphism (single j).obj X i ≅ X when i = j.

Equations

• CategoryTheory.GradedObject.singleObjApplyIsoOfEq j X i h = CategoryTheory.eqToIso ⋯

@[reducible, inline]

noncomputable abbrev CategoryTheory.GradedObject.singleObjApplyIso {J : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Limits.HasInitial C] [DecidableEq J] (j : J) (X : C) : (single j).obj X j ≅ X

The canonical isomorphism (single j).obj X j ≅ X.

Equations

• CategoryTheory.GradedObject.singleObjApplyIso j X = CategoryTheory.GradedObject.singleObjApplyIsoOfEq j X j ⋯

noncomputable def CategoryTheory.GradedObject.isInitialSingleObjApply {J : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Limits.HasInitial C] [DecidableEq J] (j : J) (X : C) (i : J) (h : i ≠ j) : Limits.IsInitial ((single j).obj X i)

The object (single j).obj X i is initial when i ≠ j.

Equations

• CategoryTheory.GradedObject.isInitialSingleObjApply j X i h = id (⋯.mpr CategoryTheory.Limits.initialIsInitial)

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

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

@[simp]

theorem CategoryTheory.GradedObject.singleObjApplyIso_inv_single_map {J : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Limits.HasInitial C] [DecidableEq J] (j : J) {X Y : C} (f : X ⟶ Y) : CategoryStruct.comp (singleObjApplyIso j X).inv ((single j).map f j) = CategoryStruct.comp f (singleObjApplyIso j Y).inv

@[simp]

theorem CategoryTheory.GradedObject.singleObjApplyIso_inv_single_map_assoc {J : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Limits.HasInitial C] [DecidableEq J] (j : J) {X Y : C} (f : X ⟶ Y) {Z : C} (h : (single j).obj Y j ⟶ Z) : CategoryStruct.comp (singleObjApplyIso j X).inv (CategoryStruct.comp ((single j).map f j) h) = CategoryStruct.comp f (CategoryStruct.comp (singleObjApplyIso j Y).inv h)

@[simp]

theorem CategoryTheory.GradedObject.single_map_singleObjApplyIso_hom {J : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Limits.HasInitial C] [DecidableEq J] (j : J) {X Y : C} (f : X ⟶ Y) : CategoryStruct.comp ((single j).map f j) (singleObjApplyIso j Y).hom = CategoryStruct.comp (singleObjApplyIso j X).hom f

@[simp]

theorem CategoryTheory.GradedObject.single_map_singleObjApplyIso_hom_assoc {J : Type u_1} {C : Type u_2} [Category.{v_1, u_2} C] [Limits.HasInitial C] [DecidableEq J] (j : J) {X Y : C} (f : X ⟶ Y) {Z : C} (h : Y ⟶ Z) : CategoryStruct.comp ((single j).map f j) (CategoryStruct.comp (singleObjApplyIso j Y).hom h) = CategoryStruct.comp (singleObjApplyIso j X).hom (CategoryStruct.comp f h)

noncomputable def CategoryTheory.GradedObject.singleCompEval {J : Type u_1} (C : Type u_2) [Category.{v_1, u_2} C] [Limits.HasInitial C] [DecidableEq J] (j : J) : (single j).comp (eval j) ≅ Functor.id C

The composition of the single functor single j : C ⥤ GradedObject J C and the evaluation functor eval j identifies to the identity functor.

Equations

• CategoryTheory.GradedObject.singleCompEval C j = CategoryTheory.NatIso.ofComponents (CategoryTheory.GradedObject.singleObjApplyIso j) ⋯

@[simp]

theorem CategoryTheory.GradedObject.singleCompEval_hom_app {J : Type u_1} (C : Type u_2) [Category.{v_1, u_2} C] [Limits.HasInitial C] [DecidableEq J] (j : J) (X : C) : (singleCompEval C j).hom.app X = (singleObjApplyIso j X).hom

@[simp]

theorem CategoryTheory.GradedObject.singleCompEval_inv_app {J : Type u_1} (C : Type u_2) [Category.{v_1, u_2} C] [Limits.HasInitial C] [DecidableEq J] (j : J) (X : C) : (singleCompEval C j).inv.app X = (singleObjApplyIso j X).inv