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)
:
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.
Instances For
@[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]
:
The functor which sends X : C
to the graded object which is X
in degree 0
and the initial object in nonzero degrees.
Instances For
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
Instances For
@[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
Instances For
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)
:
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)
Instances For
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)
:
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)
:
@[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.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)
:
@[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)
@[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)
:
@[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
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)
:
The composition of the single functor single j : C ⥤ GradedObject J C
and the
evaluation functor eval j
identifies to the identity functor.