The category of graded objects #
For any type β
, a β
-graded object over some category C
is just
a function β → C
into the objects of C
.
We put the "pointwise" category structure on these, as the non-dependent specialization of
CategoryTheory.Pi
.
We describe the comap
functors obtained by precomposing with functions β → γ
.
As a consequence a fixed element (e.g. 1
) in an additive group β
provides a shift
functor on β
-graded objects
When C
has coproducts we construct the total
functor GradedObject β C ⥤ C
,
show that it is faithful, and deduce that when C
is concrete so is GradedObject β C
.
A type synonym for β → C
, used for β
-graded objects in a category C
.
Instances For
A type synonym for β → C
, used for β
-graded objects in a category C
with a shift functor given by translation by s
.
Instances For
The projection of a graded object to its i
-th component.
Instances For
Pull back an I
-graded object in C
to a J
-graded object along a function J → I
.
Instances For
The natural isomorphism comparing between pulling back along two propositionally equal functions.
Instances For
The equivalence between β-graded objects and γ-graded objects, given an equivalence between β and γ.
Instances For
The total object of a graded object is the coproduct of the graded components.
Instances For
The total
functor taking a graded object to the coproduct of its graded components is faithful.
To prove this, we need to know that the coprojections into the coproduct are monomorphisms,
which follows from the fact we have zero morphisms and decidable equality for the grading.