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} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasInitial C] [DecidableEq J] (j : J) : CategoryTheory.Functor C (CategoryTheory.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} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasInitial C] [DecidableEq J] [Zero J] : CategoryTheory.Functor C (CategoryTheory.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} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasInitial C] [DecidableEq J] (j : J) (X : C) (i : J) (h : i = j) : (CategoryTheory.GradedObject.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} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasInitial C] [DecidableEq J] (j : J) (X : C) : (CategoryTheory.GradedObject.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} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasInitial C] [DecidableEq J] (j : J) (X : C) (i : J) (h : i ≠ j) : CategoryTheory.Limits.IsInitial ((CategoryTheory.GradedObject.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} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasInitial C] [DecidableEq J] (j : J) {X : C} {Y : C} (f : X ⟶ Y) (i : J) (h : i = j) : CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.singleObjApplyIsoOfEq j X i h).inv ((CategoryTheory.GradedObject.single j).map f i) = CategoryTheory.CategoryStruct.comp f (CategoryTheory.GradedObject.singleObjApplyIsoOfEq j Y i h).inv

theorem CategoryTheory.GradedObject.single_map_singleObjApplyIsoOfEq_hom {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasInitial C] [DecidableEq J] (j : J) {X : C} {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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

noncomputable def CategoryTheory.GradedObject.singleCompEval {J : Type u_1} (C : Type u_2) [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasInitial C] [DecidableEq J] (j : J) : (CategoryTheory.GradedObject.single j).comp (CategoryTheory.GradedObject.eval j) ≅ CategoryTheory.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) [CategoryTheory.Category.{u_3, u_2} C] [CategoryTheory.Limits.HasInitial C] [DecidableEq J] (j : J) (X : C) : (CategoryTheory.GradedObject.singleCompEval C j).hom.app X = (CategoryTheory.GradedObject.singleObjApplyIso j X).hom

@[simp]

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