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.

def CategoryTheory.GradedObject (β : Type w) (C : Type u) : Type (max w u)

A type synonym for β → C, used for β-graded objects in a category C.

instance CategoryTheory.inhabitedGradedObject (β : Type w) (C : Type u) [Inhabited C] : Inhabited (CategoryTheory.GradedObject β C)

@[inline, reducible]

abbrev CategoryTheory.GradedObjectWithShift {β : Type w} [AddCommGroup β] : β → Type u → Type (max w u)

A type synonym for β → C, used for β-graded objects in a category C with a shift functor given by translation by s.

@[simp]

theorem CategoryTheory.GradedObject.categoryOfGradedObjects_id {C : Type u} [CategoryTheory.Category.{v, u} C] (β : Type w) (X : (i : β) → (fun x => C) i) (i : β) : CategoryTheory.CategoryStruct.id (CategoryTheory.GradedObject β C) CategoryTheory.Category.toCategoryStruct X i = CategoryTheory.CategoryStruct.id (X i)

@[simp]

theorem CategoryTheory.GradedObject.categoryOfGradedObjects_comp {C : Type u} [CategoryTheory.Category.{v, u} C] (β : Type w) : ∀ {X Y Z : (i : β) → (fun x => C) i} (f : X ⟶ Y) (g : Y ⟶ Z) (i : β), CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject β C) CategoryTheory.Category.toCategoryStruct X Y Z f g i = CategoryTheory.CategoryStruct.comp (f i) (g i)

instance CategoryTheory.GradedObject.categoryOfGradedObjects {C : Type u} [CategoryTheory.Category.{v, u} C] (β : Type w) : CategoryTheory.Category.{max w v, max u w} (CategoryTheory.GradedObject β C)

theorem CategoryTheory.GradedObject.hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] {β : Type u_1} {X : CategoryTheory.GradedObject β C} {Y : CategoryTheory.GradedObject β C} (f : X ⟶ Y) (g : X ⟶ Y) (h : ∀ (x : β), f x = g x) : f = g

@[simp]

theorem CategoryTheory.GradedObject.eval_obj {C : Type u} [CategoryTheory.Category.{v, u} C] {β : Type w} (b : β) (X : CategoryTheory.GradedObject β C) : (CategoryTheory.GradedObject.eval b).obj X = X b

@[simp]

theorem CategoryTheory.GradedObject.eval_map {C : Type u} [CategoryTheory.Category.{v, u} C] {β : Type w} (b : β) : ∀ {X Y : CategoryTheory.GradedObject β C} (f : X ⟶ Y), (CategoryTheory.GradedObject.eval b).map f = f b

def CategoryTheory.GradedObject.eval {C : Type u} [CategoryTheory.Category.{v, u} C] {β : Type w} (b : β) : CategoryTheory.Functor (CategoryTheory.GradedObject β C) C

The projection of a graded object to its i-th component.

@[inline, reducible]

abbrev CategoryTheory.GradedObject.comap (C : Type u) [CategoryTheory.Category.{v, u} C] {I : Type u_1} {J : Type u_2} (h : J → I) : CategoryTheory.Functor (CategoryTheory.GradedObject I C) (CategoryTheory.GradedObject J C)

Pull back an I-graded object in C to a J-graded object along a function J → I.

@[simp]

theorem CategoryTheory.GradedObject.eqToHom_proj (C : Type u) [CategoryTheory.Category.{v, u} C] {I : Type u_1} {x : CategoryTheory.GradedObject I C} {x' : CategoryTheory.GradedObject I C} (h : x = x') (i : I) : CategoryTheory.eqToHom (CategoryTheory.GradedObject I C) (CategoryTheory.GradedObject.categoryOfGradedObjects I) x x' h i = CategoryTheory.eqToHom (_ : x i = x' i)

@[simp]

theorem CategoryTheory.GradedObject.comapEq_inv_app (C : Type u) [CategoryTheory.Category.{v, u} C] {β : Type w} {γ : Type w} {f : β → γ} {g : β → γ} (h : f = g) (X : CategoryTheory.GradedObject γ C) (b : β) : (CategoryTheory.GradedObject γ C).app (CategoryTheory.GradedObject.categoryOfGradedObjects γ) (CategoryTheory.GradedObject β C) (CategoryTheory.GradedObject.categoryOfGradedObjects β) (CategoryTheory.GradedObject.comap C g) (CategoryTheory.GradedObject.comap C f) (CategoryTheory.GradedObject.comapEq C h).inv X b = CategoryTheory.eqToHom (_ : (CategoryTheory.GradedObject γ C).obj CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.GradedObject β C) CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.GradedObject.comap C g).toPrefunctor X b = (CategoryTheory.GradedObject γ C).obj CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.GradedObject β C) CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.GradedObject.comap C f).toPrefunctor X b)

@[simp]

theorem CategoryTheory.GradedObject.comapEq_hom_app (C : Type u) [CategoryTheory.Category.{v, u} C] {β : Type w} {γ : Type w} {f : β → γ} {g : β → γ} (h : f = g) (X : CategoryTheory.GradedObject γ C) (b : β) : (CategoryTheory.GradedObject γ C).app (CategoryTheory.GradedObject.categoryOfGradedObjects γ) (CategoryTheory.GradedObject β C) (CategoryTheory.GradedObject.categoryOfGradedObjects β) (CategoryTheory.GradedObject.comap C f) (CategoryTheory.GradedObject.comap C g) (CategoryTheory.GradedObject.comapEq C h).hom X b = CategoryTheory.eqToHom (_ : (CategoryTheory.GradedObject γ C).obj CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.GradedObject β C) CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.GradedObject.comap C f).toPrefunctor X b = (CategoryTheory.GradedObject γ C).obj CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.GradedObject β C) CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.GradedObject.comap C g).toPrefunctor X b)

def CategoryTheory.GradedObject.comapEq (C : Type u) [CategoryTheory.Category.{v, u} C] {β : Type w} {γ : Type w} {f : β → γ} {g : β → γ} (h : f = g) : CategoryTheory.GradedObject.comap C f ≅ CategoryTheory.GradedObject.comap C g

The natural isomorphism comparing between pulling back along two propositionally equal functions.

theorem CategoryTheory.GradedObject.comapEq_symm (C : Type u) [CategoryTheory.Category.{v, u} C] {β : Type w} {γ : Type w} {f : β → γ} {g : β → γ} (h : f = g) : CategoryTheory.GradedObject.comapEq C (_ : g = f) = (CategoryTheory.GradedObject.comapEq C h).symm

theorem CategoryTheory.GradedObject.comapEq_trans (C : Type u) [CategoryTheory.Category.{v, u} C] {β : Type w} {γ : Type w} {f : β → γ} {g : β → γ} {h : β → γ} (k : f = g) (l : g = h) : CategoryTheory.GradedObject.comapEq C (_ : f = h) = CategoryTheory.GradedObject.comapEq C k ≪≫ CategoryTheory.GradedObject.comapEq C l

@[simp]

theorem CategoryTheory.GradedObject.eqToHom_apply (C : Type u) [CategoryTheory.Category.{v, u} C] {β : Type w} {X : β → C} {Y : β → C} (h : X = Y) (b : β) : CategoryTheory.eqToHom (β → C) (CategoryTheory.pi fun x => C) X Y h b = CategoryTheory.eqToHom (_ : X b = Y b)

@[simp]

theorem CategoryTheory.GradedObject.comapEquiv_functor (C : Type u) [CategoryTheory.Category.{v, u} C] {β : Type w} {γ : Type w} (e : β ≃ γ) : (CategoryTheory.GradedObject.comapEquiv C e).functor = CategoryTheory.GradedObject.comap C ↑e.symm

@[simp]

theorem CategoryTheory.GradedObject.comapEquiv_unitIso (C : Type u) [CategoryTheory.Category.{v, u} C] {β : Type w} {γ : Type w} (e : β ≃ γ) : (CategoryTheory.GradedObject.comapEquiv C e).unitIso = CategoryTheory.GradedObject.comapEq C (_ : (fun i => i) = ↑e.symm ∘ ↑e) ≪≫ (CategoryTheory.Pi.comapComp (fun x => C) ↑e ↑e.symm).symm

@[simp]

theorem CategoryTheory.GradedObject.comapEquiv_counitIso (C : Type u) [CategoryTheory.Category.{v, u} C] {β : Type w} {γ : Type w} (e : β ≃ γ) : (CategoryTheory.GradedObject.comapEquiv C e).counitIso = CategoryTheory.Pi.comapComp (fun x => C) ↑e.symm ↑e ≪≫ CategoryTheory.GradedObject.comapEq C (_ : ↑e ∘ ↑e.symm = fun i => i)

@[simp]

theorem CategoryTheory.GradedObject.comapEquiv_inverse (C : Type u) [CategoryTheory.Category.{v, u} C] {β : Type w} {γ : Type w} (e : β ≃ γ) : (CategoryTheory.GradedObject.comapEquiv C e).inverse = CategoryTheory.GradedObject.comap C ↑e

def CategoryTheory.GradedObject.comapEquiv (C : Type u) [CategoryTheory.Category.{v, u} C] {β : Type w} {γ : Type w} (e : β ≃ γ) : CategoryTheory.GradedObject β C ≌ CategoryTheory.GradedObject γ C

The equivalence between β-graded objects and γ-graded objects, given an equivalence between β and γ.

instance CategoryTheory.GradedObject.hasShift {C : Type u} [CategoryTheory.Category.{v, u} C] {β : Type u_1} [AddCommGroup β] (s : β) : CategoryTheory.HasShift (CategoryTheory.GradedObjectWithShift s C) ℤ

@[simp]

theorem CategoryTheory.GradedObject.shiftFunctor_obj_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {β : Type u_1} [AddCommGroup β] (s : β) (X : β → C) (t : β) (n : ℤ) : (CategoryTheory.GradedObjectWithShift s C).obj CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.GradedObjectWithShift s C) CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.shiftFunctor (CategoryTheory.GradedObjectWithShift s C) n).toPrefunctor X t = X (t + n • s)

@[simp]

theorem CategoryTheory.GradedObject.shiftFunctor_map_apply {C : Type u} [CategoryTheory.Category.{v, u} C] {β : Type u_1} [AddCommGroup β] (s : β) {X : CategoryTheory.GradedObjectWithShift s C} {Y : CategoryTheory.GradedObjectWithShift s C} (f : X ⟶ Y) (t : β) (n : ℤ) : (CategoryTheory.GradedObjectWithShift s C).map CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.GradedObjectWithShift s C) CategoryTheory.CategoryStruct.toQuiver (CategoryTheory.shiftFunctor (CategoryTheory.GradedObjectWithShift s C) n).toPrefunctor X Y f t = f (t + n • s)

instance CategoryTheory.GradedObject.instZeroHomGradedObjectToQuiverToCategoryStructCategoryOfGradedObjects {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (β : Type w) (X : CategoryTheory.GradedObject β C) (Y : CategoryTheory.GradedObject β C) : Zero (X ⟶ Y)

@[simp]

theorem CategoryTheory.GradedObject.zero_apply {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (β : Type w) (X : CategoryTheory.GradedObject β C) (Y : CategoryTheory.GradedObject β C) (b : β) : OfNat.ofNat (X ⟶ Y) 0 Zero.toOfNat0 b = 0

instance CategoryTheory.GradedObject.hasZeroMorphisms {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] (β : Type w) : CategoryTheory.Limits.HasZeroMorphisms (CategoryTheory.GradedObject β C)

instance CategoryTheory.GradedObject.hasZeroObject {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] (β : Type w) : CategoryTheory.Limits.HasZeroObject (CategoryTheory.GradedObject β C)

noncomputable def CategoryTheory.GradedObject.total (β : Type) (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] : CategoryTheory.Functor (CategoryTheory.GradedObject β C) C

The total object of a graded object is the coproduct of the graded components.

instance CategoryTheory.GradedObject.instFaithfulGradedObjectCategoryOfGradedObjectsTotalType (β : Type) (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Limits.HasZeroMorphisms C] : CategoryTheory.Faithful (CategoryTheory.GradedObject.total β C)

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.

instance CategoryTheory.GradedObject.instConcreteCategoryGradedObjectCategoryOfGradedObjects (β : Type) (C : Type (u + 1)) [CategoryTheory.LargeCategory C] [CategoryTheory.ConcreteCategory C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Limits.HasZeroMorphisms C] : CategoryTheory.ConcreteCategory (CategoryTheory.GradedObject β C)

instance CategoryTheory.GradedObject.instHasForget₂GradedObjectCategoryOfGradedObjectsInstConcreteCategoryGradedObjectCategoryOfGradedObjectsType (β : Type) (C : Type (u + 1)) [CategoryTheory.LargeCategory C] [CategoryTheory.ConcreteCategory C] [CategoryTheory.Limits.HasCoproducts C] [CategoryTheory.Limits.HasZeroMorphisms C] : CategoryTheory.HasForget₂ (CategoryTheory.GradedObject β C) C