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 covariant functoriality of GradedObject β C with respect to the index set β is also introduced: if p : I → J is a map such that C has coproducts indexed by p ⁻¹' {j}, we have a functor map : GradedObject I C ⥤ GradedObject J 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.

Equations

• CategoryTheory.GradedObject β C = (β → C)

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

Equations

• CategoryTheory.inhabitedGradedObject β C = { default := fun (x : β) => default }

@[reducible, inline]

abbrev CategoryTheory.GradedObjectWithShift {β : Type w} [AddCommGroup β] : β → (C : 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.

Equations

• CategoryTheory.GradedObjectWithShift x✝ C = CategoryTheory.GradedObject β C

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

Equations

• CategoryTheory.GradedObject.categoryOfGradedObjects β = CategoryTheory.pi fun (x : β) => C

@[simp]

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

@[simp]

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

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

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

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

Equations

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

@[simp]

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

@[simp]

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

def CategoryTheory.GradedObject.isoMk {C : Type u} [Category.{v, u} C] {β : Type u_1} (X Y : GradedObject β C) (e : (i : β) → X i ≅ Y i) : X ≅ Y

Constructor for isomorphisms in GradedObject

Equations

• X.isoMk Y e = { hom := fun (i : β) => (e i).hom, inv := fun (i : β) => (e i).inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.GradedObject.isoMk_hom {C : Type u} [Category.{v, u} C] {β : Type u_1} (X Y : GradedObject β C) (e : (i : β) → X i ≅ Y i) (i : β) : (X.isoMk Y e).hom i = (e i).hom

@[simp]

theorem CategoryTheory.GradedObject.isoMk_inv {C : Type u} [Category.{v, u} C] {β : Type u_1} (X Y : GradedObject β C) (e : (i : β) → X i ≅ Y i) (i : β) : (X.isoMk Y e).inv i = (e i).inv

theorem CategoryTheory.GradedObject.isIso_of_isIso_apply {C : Type u} [Category.{v, u} C] {β : Type u_1} {X Y : GradedObject β C} (f : X ⟶ Y) [hf : ∀ (i : β), IsIso (f i)] : IsIso f

instance CategoryTheory.GradedObject.isIso_apply_of_isIso {C : Type u} [Category.{v, u} C] {β : Type u_1} {X Y : GradedObject β C} (f : X ⟶ Y) [IsIso f] (i : β) : IsIso (f i)

@[simp]

theorem CategoryTheory.Iso.hom_inv_id_eval {C : Type u_1} {J : Type u_4} [Category.{u_5, u_1} C] {X Y : GradedObject J C} (e : X ≅ Y) (j : J) : CategoryStruct.comp (e.hom j) (e.inv j) = CategoryStruct.id (X j)

@[simp]

theorem CategoryTheory.Iso.hom_inv_id_eval_assoc {C : Type u_1} {J : Type u_4} [Category.{u_5, u_1} C] {X Y : GradedObject J C} (e : X ≅ Y) (j : J) {Z : C} (h : X j ⟶ Z) : CategoryStruct.comp (e.hom j) (CategoryStruct.comp (e.inv j) h) = h

@[simp]

theorem CategoryTheory.Iso.inv_hom_id_eval {C : Type u_1} {J : Type u_4} [Category.{u_5, u_1} C] {X Y : GradedObject J C} (e : X ≅ Y) (j : J) : CategoryStruct.comp (e.inv j) (e.hom j) = CategoryStruct.id (Y j)

@[simp]

theorem CategoryTheory.Iso.inv_hom_id_eval_assoc {C : Type u_1} {J : Type u_4} [Category.{u_5, u_1} C] {X Y : GradedObject J C} (e : X ≅ Y) (j : J) {Z : C} (h : Y j ⟶ Z) : CategoryStruct.comp (e.inv j) (CategoryStruct.comp (e.hom j) h) = h

@[simp]

theorem CategoryTheory.Iso.map_hom_inv_id_eval {C : Type u_1} {D : Type u_2} {J : Type u_4} [Category.{u_5, u_1} C] [Category.{u_6, u_2} D] {X Y : GradedObject J C} (e : X ≅ Y) (F : Functor C D) (j : J) : CategoryStruct.comp (F.map (e.hom j)) (F.map (e.inv j)) = CategoryStruct.id (F.obj (X j))

@[simp]

theorem CategoryTheory.Iso.map_hom_inv_id_eval_assoc {C : Type u_1} {D : Type u_2} {J : Type u_4} [Category.{u_5, u_1} C] [Category.{u_6, u_2} D] {X Y : GradedObject J C} (e : X ≅ Y) (F : Functor C D) (j : J) {Z : D} (h : F.obj (X j) ⟶ Z) : CategoryStruct.comp (F.map (e.hom j)) (CategoryStruct.comp (F.map (e.inv j)) h) = h

@[simp]

theorem CategoryTheory.Iso.map_inv_hom_id_eval {C : Type u_1} {D : Type u_2} {J : Type u_4} [Category.{u_5, u_1} C] [Category.{u_6, u_2} D] {X Y : GradedObject J C} (e : X ≅ Y) (F : Functor C D) (j : J) : CategoryStruct.comp (F.map (e.inv j)) (F.map (e.hom j)) = CategoryStruct.id (F.obj (Y j))

@[simp]

theorem CategoryTheory.Iso.map_inv_hom_id_eval_assoc {C : Type u_1} {D : Type u_2} {J : Type u_4} [Category.{u_5, u_1} C] [Category.{u_6, u_2} D] {X Y : GradedObject J C} (e : X ≅ Y) (F : Functor C D) (j : J) {Z : D} (h : F.obj (Y j) ⟶ Z) : CategoryStruct.comp (F.map (e.inv j)) (CategoryStruct.comp (F.map (e.hom j)) h) = h

@[simp]

theorem CategoryTheory.Iso.map_hom_inv_id_eval_app {C : Type u_1} {D : Type u_2} {E : Type u_3} {J : Type u_4} [Category.{u_5, u_1} C] [Category.{u_7, u_2} D] [Category.{u_6, u_3} E] {X Y : GradedObject J C} (e : X ≅ Y) (F : Functor C (Functor D E)) (j : J) (Y✝ : D) : CategoryStruct.comp ((F.map (e.hom j)).app Y✝) ((F.map (e.inv j)).app Y✝) = CategoryStruct.id ((F.obj (X j)).obj Y✝)

@[simp]

theorem CategoryTheory.Iso.map_hom_inv_id_eval_app_assoc {C : Type u_1} {D : Type u_2} {E : Type u_3} {J : Type u_4} [Category.{u_5, u_1} C] [Category.{u_7, u_2} D] [Category.{u_6, u_3} E] {X Y : GradedObject J C} (e : X ≅ Y) (F : Functor C (Functor D E)) (j : J) (Y✝ : D) {Z : E} (h : (F.obj (X j)).obj Y✝ ⟶ Z) : CategoryStruct.comp ((F.map (e.hom j)).app Y✝) (CategoryStruct.comp ((F.map (e.inv j)).app Y✝) h) = h

@[simp]

theorem CategoryTheory.Iso.map_inv_hom_id_eval_app {C : Type u_1} {D : Type u_2} {E : Type u_3} {J : Type u_4} [Category.{u_5, u_1} C] [Category.{u_7, u_2} D] [Category.{u_6, u_3} E] {X Y : GradedObject J C} (e : X ≅ Y) (F : Functor C (Functor D E)) (j : J) (Y✝ : D) : CategoryStruct.comp ((F.map (e.inv j)).app Y✝) ((F.map (e.hom j)).app Y✝) = CategoryStruct.id ((F.obj (Y j)).obj Y✝)

@[simp]

theorem CategoryTheory.Iso.map_inv_hom_id_eval_app_assoc {C : Type u_1} {D : Type u_2} {E : Type u_3} {J : Type u_4} [Category.{u_5, u_1} C] [Category.{u_7, u_2} D] [Category.{u_6, u_3} E] {X Y : GradedObject J C} (e : X ≅ Y) (F : Functor C (Functor D E)) (j : J) (Y✝ : D) {Z : E} (h : (F.obj (Y j)).obj Y✝ ⟶ Z) : CategoryStruct.comp ((F.map (e.inv j)).app Y✝) (CategoryStruct.comp ((F.map (e.hom j)).app Y✝) h) = h

@[reducible, inline]

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

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

Equations

• CategoryTheory.GradedObject.comap C h = CategoryTheory.Pi.comap (fun (x : I) => C) h

@[simp]

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

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

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

Equations

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

@[simp]

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

@[simp]

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

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

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

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

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

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Equations

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

@[simp]

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

@[simp]

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

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

Equations

• CategoryTheory.GradedObject.instZeroHomOfHasZeroMorphisms β X Y = { zero := fun (x : β) => 0 }

@[simp]

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

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

Equations

• CategoryTheory.GradedObject.hasZeroMorphisms β = CategoryTheory.Limits.HasZeroMorphisms.mk ⋯ ⋯

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

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

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

Equations

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

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

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.instHasForget (β : Type) (C : Type (u + 1)) [LargeCategory C] [HasForget C] [Limits.HasCoproducts C] [Limits.HasZeroMorphisms C] : HasForget (GradedObject β C)

Equations

• CategoryTheory.GradedObject.instHasForget β C = CategoryTheory.HasForget.mk ((CategoryTheory.GradedObject.total β C).comp (CategoryTheory.forget C))

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

Equations

• CategoryTheory.GradedObject.instHasForget₂ β C = { forget₂ := CategoryTheory.GradedObject.total β C, forget_comp := ⋯ }

@[reducible, inline]

abbrev CategoryTheory.GradedObject.mapObjFun {I : Type u_1} {J : Type u_2} {C : Type u_4} (X : GradedObject I C) (p : I → J) (j : J) (i : ↑(p ⁻¹' {j})) : C

If X : GradedObject I C and p : I → J, X.mapObjFun p j is the family of objects X i for i : I such that p i = j.

Equations

• X.mapObjFun p j i = X ↑i

@[reducible, inline]

abbrev CategoryTheory.GradedObject.HasMap {I : Type u_1} {J : Type u_2} {C : Type u_4} [Category.{u_5, u_4} C] (X : GradedObject I C) (p : I → J) : Prop

Given X : GradedObject I C and p : I → J, X.HasMap p is the condition that for all j : J, the coproduct of all X i such p i = j exists.

Equations

• X.HasMap p = ∀ (j : J), CategoryTheory.Limits.HasCoproduct (X.mapObjFun p j)

theorem CategoryTheory.GradedObject.hasMap_of_iso {I : Type u_1} {J : Type u_2} {C : Type u_4} [Category.{u_5, u_4} C] {X Y : GradedObject I C} (e : X ≅ Y) (p : I → J) [X.HasMap p] : Y.HasMap p

noncomputable def CategoryTheory.GradedObject.mapObj {I : Type u_1} {J : Type u_2} {C : Type u_4} [Category.{u_5, u_4} C] (X : GradedObject I C) (p : I → J) [X.HasMap p] : GradedObject J C

Given X : GradedObject I C and p : I → J, X.mapObj p is the graded object by J which in degree j consists of the coproduct of the X i such that p i = j.

Equations

• X.mapObj p j = ∐ X.mapObjFun p j

noncomputable def CategoryTheory.GradedObject.ιMapObj {I : Type u_1} {J : Type u_2} {C : Type u_4} [Category.{u_5, u_4} C] (X : GradedObject I C) (p : I → J) [X.HasMap p] (i : I) (j : J) (hij : p i = j) : X i ⟶ X.mapObj p j

The canonical inclusion X i ⟶ X.mapObj p j when i : I and j : J are such that p i = j.

Equations

• X.ιMapObj p i j hij = CategoryTheory.Limits.Sigma.ι (X.mapObjFun p j) ⟨i, hij⟩

@[reducible, inline]

abbrev CategoryTheory.GradedObject.CofanMapObjFun {I : Type u_1} {J : Type u_2} {C : Type u_4} [Category.{u_5, u_4} C] (X : GradedObject I C) (p : I → J) (j : J) : Type (max (max u_4 u_5) u_1)

Given X : GradedObject I C, p : I → J and j : J, CofanMapObjFun X p j is the type Cofan (X.mapObjFun p j). The point object of such colimits cofans are isomorphic to X.mapObj p j, see CofanMapObjFun.iso.

Equations

• X.CofanMapObjFun p j = CategoryTheory.Limits.Cofan (X.mapObjFun p j)

def CategoryTheory.GradedObject.CofanMapObjFun.mk {I : Type u_1} {J : Type u_2} {C : Type u_4} [Category.{u_5, u_4} C] (X : GradedObject I C) (p : I → J) (j : J) (pt : C) (ι' : (i : I) → p i = j → (X i ⟶ pt)) : X.CofanMapObjFun p j

Constructor for CofanMapObjFun X p j.

Equations

• CategoryTheory.GradedObject.CofanMapObjFun.mk X p j pt ι' = CategoryTheory.Limits.Cofan.mk pt fun (x : ↑(p ⁻¹' {j})) => match x with | ⟨i, hi⟩ => ι' i hi

noncomputable def CategoryTheory.GradedObject.cofanMapObj {I : Type u_1} {J : Type u_2} {C : Type u_4} [Category.{u_5, u_4} C] (X : GradedObject I C) (p : I → J) [X.HasMap p] (j : J) : X.CofanMapObjFun p j

The tautological cofan corresponding to the coproduct decomposition of X.mapObj p j.

Equations

• X.cofanMapObj p j = CategoryTheory.GradedObject.CofanMapObjFun.mk X p j (X.mapObj p j) fun (i : I) (hi : p i = j) => X.ιMapObj p i j hi

noncomputable def CategoryTheory.GradedObject.isColimitCofanMapObj {I : Type u_1} {J : Type u_2} {C : Type u_4} [Category.{u_5, u_4} C] (X : GradedObject I C) (p : I → J) [X.HasMap p] (j : J) : Limits.IsColimit (X.cofanMapObj p j)

Given X : GradedObject I C, p : I → J and j : J, X.mapObj p j satisfies the universal property of the coproduct of those X i such that p i = j.

Equations

• X.isColimitCofanMapObj p j = CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Discrete.functor (X.mapObjFun p j))

theorem CategoryTheory.GradedObject.mapObj_ext {I : Type u_1} {J : Type u_2} {C : Type u_4} [Category.{u_5, u_4} C] (X : GradedObject I C) (p : I → J) [X.HasMap p] {A : C} {j : J} (f g : X.mapObj p j ⟶ A) (hfg : ∀ (i : I) (hij : p i = j), CategoryStruct.comp (X.ιMapObj p i j hij) f = CategoryStruct.comp (X.ιMapObj p i j hij) g) : f = g

noncomputable def CategoryTheory.GradedObject.descMapObj {I : Type u_1} {J : Type u_2} {C : Type u_4} [Category.{u_5, u_4} C] (X : GradedObject I C) (p : I → J) [X.HasMap p] {A : C} {j : J} (φ : (i : I) → p i = j → (X i ⟶ A)) : X.mapObj p j ⟶ A

This is the morphism X.mapObj p j ⟶ A constructed from a family of morphisms X i ⟶ A for all i : I such that p i = j.

Equations

• X.descMapObj p φ = CategoryTheory.Limits.Cofan.IsColimit.desc (X.isColimitCofanMapObj p j) fun (x : ↑(p ⁻¹' {j})) => match x with | ⟨i, hi⟩ => φ i hi

@[simp]

theorem CategoryTheory.GradedObject.ι_descMapObj {I : Type u_1} {J : Type u_2} {C : Type u_4} [Category.{u_5, u_4} C] (X : GradedObject I C) (p : I → J) [X.HasMap p] {A : C} {j : J} (φ : (i : I) → p i = j → (X i ⟶ A)) (i : I) (hi : p i = j) : CategoryStruct.comp (X.ιMapObj p i j hi) (X.descMapObj p φ) = φ i hi

@[simp]

theorem CategoryTheory.GradedObject.ι_descMapObj_assoc {I : Type u_1} {J : Type u_2} {C : Type u_4} [Category.{u_5, u_4} C] (X : GradedObject I C) (p : I → J) [X.HasMap p] {A : C} {j : J} (φ : (i : I) → p i = j → (X i ⟶ A)) (i : I) (hi : p i = j) {Z : C} (h : A ⟶ Z) : CategoryStruct.comp (X.ιMapObj p i j hi) (CategoryStruct.comp (X.descMapObj p φ) h) = CategoryStruct.comp (φ i hi) h

theorem CategoryTheory.GradedObject.CofanMapObjFun.hasMap {I : Type u_1} {J : Type u_2} {C : Type u_4} [Category.{u_5, u_4} C] (X : GradedObject I C) (p : I → J) (c : (j : J) → X.CofanMapObjFun p j) (hc : (j : J) → Limits.IsColimit (c j)) : X.HasMap p

noncomputable def CategoryTheory.GradedObject.CofanMapObjFun.iso {I : Type u_1} {J : Type u_2} {C : Type u_4} [Category.{u_5, u_4} C] {X : GradedObject I C} {p : I → J} {j : J} [X.HasMap p] {c : X.CofanMapObjFun p j} (hc : Limits.IsColimit c) : c.pt ≅ X.mapObj p j

If c : CofanMapObjFun X p j is a colimit cofan, this is the induced isomorphism c.pt ≅ X.mapObj p j.

Equations

• CategoryTheory.GradedObject.CofanMapObjFun.iso hc = hc.coconePointUniqueUpToIso (X.isColimitCofanMapObj p j)

@[simp]

theorem CategoryTheory.GradedObject.CofanMapObjFun.inj_iso_hom {I : Type u_1} {J : Type u_2} {C : Type u_4} [Category.{u_5, u_4} C] {X : GradedObject I C} {p : I → J} {j : J} [X.HasMap p] {c : X.CofanMapObjFun p j} (hc : Limits.IsColimit c) (i : I) (hi : p i = j) : CategoryStruct.comp (Limits.Cofan.inj c ⟨i, hi⟩) (iso hc).hom = X.ιMapObj p i j hi

@[simp]

theorem CategoryTheory.GradedObject.CofanMapObjFun.inj_iso_hom_assoc {I : Type u_1} {J : Type u_2} {C : Type u_4} [Category.{u_5, u_4} C] {X : GradedObject I C} {p : I → J} {j : J} [X.HasMap p] {c : X.CofanMapObjFun p j} (hc : Limits.IsColimit c) (i : I) (hi : p i = j) {Z : C} (h : X.mapObj p j ⟶ Z) : CategoryStruct.comp (Limits.Cofan.inj c ⟨i, hi⟩) (CategoryStruct.comp (iso hc).hom h) = CategoryStruct.comp (X.ιMapObj p i j hi) h

@[simp]

theorem CategoryTheory.GradedObject.CofanMapObjFun.ιMapObj_iso_inv {I : Type u_1} {J : Type u_2} {C : Type u_4} [Category.{u_5, u_4} C] {X : GradedObject I C} {p : I → J} {j : J} [X.HasMap p] {c : X.CofanMapObjFun p j} (hc : Limits.IsColimit c) (i : I) (hi : p i = j) : CategoryStruct.comp (X.ιMapObj p i j hi) (iso hc).inv = Limits.Cofan.inj c ⟨i, hi⟩

@[simp]

theorem CategoryTheory.GradedObject.CofanMapObjFun.ιMapObj_iso_inv_assoc {I : Type u_1} {J : Type u_2} {C : Type u_4} [Category.{u_5, u_4} C] {X : GradedObject I C} {p : I → J} {j : J} [X.HasMap p] {c : X.CofanMapObjFun p j} (hc : Limits.IsColimit c) (i : I) (hi : p i = j) {Z : C} (h : c.pt ⟶ Z) : CategoryStruct.comp (X.ιMapObj p i j hi) (CategoryStruct.comp (iso hc).inv h) = CategoryStruct.comp (Limits.Cofan.inj c ⟨i, hi⟩) h

noncomputable def CategoryTheory.GradedObject.mapMap {I : Type u_1} {J : Type u_2} {C : Type u_4} [Category.{u_5, u_4} C] {X Y : GradedObject I C} (φ : X ⟶ Y) (p : I → J) [X.HasMap p] [Y.HasMap p] : X.mapObj p ⟶ Y.mapObj p

The canonical morphism of J-graded objects X.mapObj p ⟶ Y.mapObj p induced by a morphism X ⟶ Y of I-graded objects and a map p : I → J.

Equations

• CategoryTheory.GradedObject.mapMap φ p j = X.descMapObj p fun (i : I) (hi : p i = j) => CategoryTheory.CategoryStruct.comp (φ i) (Y.ιMapObj p i j hi)

@[simp]

theorem CategoryTheory.GradedObject.ι_mapMap {I : Type u_1} {J : Type u_2} {C : Type u_4} [Category.{u_5, u_4} C] {X Y : GradedObject I C} (φ : X ⟶ Y) (p : I → J) [X.HasMap p] [Y.HasMap p] (i : I) (j : J) (hij : p i = j) : CategoryStruct.comp (X.ιMapObj p i j hij) (mapMap φ p j) = CategoryStruct.comp (φ i) (Y.ιMapObj p i j hij)

@[simp]

theorem CategoryTheory.GradedObject.ι_mapMap_assoc {I : Type u_1} {J : Type u_2} {C : Type u_4} [Category.{u_5, u_4} C] {X Y : GradedObject I C} (φ : X ⟶ Y) (p : I → J) [X.HasMap p] [Y.HasMap p] (i : I) (j : J) (hij : p i = j) {Z : C} (h : Y.mapObj p j ⟶ Z) : CategoryStruct.comp (X.ιMapObj p i j hij) (CategoryStruct.comp (mapMap φ p j) h) = CategoryStruct.comp (φ i) (CategoryStruct.comp (Y.ιMapObj p i j hij) h)

theorem CategoryTheory.GradedObject.congr_mapMap {I : Type u_1} {J : Type u_2} {C : Type u_4} [Category.{u_5, u_4} C] {X Y : GradedObject I C} (p : I → J) [X.HasMap p] [Y.HasMap p] (φ₁ φ₂ : X ⟶ Y) (h : φ₁ = φ₂) : mapMap φ₁ p = mapMap φ₂ p

@[simp]

theorem CategoryTheory.GradedObject.mapMap_id {I : Type u_1} {J : Type u_2} {C : Type u_4} [Category.{u_5, u_4} C] (X : GradedObject I C) (p : I → J) [X.HasMap p] : mapMap (CategoryStruct.id X) p = CategoryStruct.id (X.mapObj p)

@[simp]

theorem CategoryTheory.GradedObject.mapMap_comp {I : Type u_1} {J : Type u_2} {C : Type u_4} [Category.{u_5, u_4} C] {X Y Z : GradedObject I C} (φ : X ⟶ Y) (ψ : Y ⟶ Z) (p : I → J) [X.HasMap p] [Y.HasMap p] [Z.HasMap p] : mapMap (CategoryStruct.comp φ ψ) p = CategoryStruct.comp (mapMap φ p) (mapMap ψ p)

theorem CategoryTheory.GradedObject.mapMap_comp_assoc {I : Type u_1} {J : Type u_2} {C : Type u_4} [Category.{u_5, u_4} C] {X Y Z : GradedObject I C} (φ : X ⟶ Y) (ψ : Y ⟶ Z) (p : I → J) [X.HasMap p] [Y.HasMap p] [Z.HasMap p] {Z✝ : GradedObject J C} (h : Z.mapObj p ⟶ Z✝) : CategoryStruct.comp (mapMap (CategoryStruct.comp φ ψ) p) h = CategoryStruct.comp (mapMap φ p) (CategoryStruct.comp (mapMap ψ p) h)

noncomputable def CategoryTheory.GradedObject.mapIso {I : Type u_1} {J : Type u_2} {C : Type u_4} [Category.{u_5, u_4} C] {X Y : GradedObject I C} (e : X ≅ Y) (p : I → J) [X.HasMap p] [Y.HasMap p] : X.mapObj p ≅ Y.mapObj p

The isomorphism of J-graded objects X.mapObj p ≅ Y.mapObj p induced by an isomorphism X ≅ Y of graded objects and a map p : I → J.

Equations

• CategoryTheory.GradedObject.mapIso e p = { hom := CategoryTheory.GradedObject.mapMap e.hom p, inv := CategoryTheory.GradedObject.mapMap e.inv p, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.GradedObject.mapIso_hom {I : Type u_1} {J : Type u_2} {C : Type u_4} [Category.{u_5, u_4} C] {X Y : GradedObject I C} (e : X ≅ Y) (p : I → J) [X.HasMap p] [Y.HasMap p] (i : J) : (mapIso e p).hom i = mapMap e.hom p i

@[simp]

theorem CategoryTheory.GradedObject.mapIso_inv {I : Type u_1} {J : Type u_2} {C : Type u_4} [Category.{u_5, u_4} C] {X Y : GradedObject I C} (e : X ≅ Y) (p : I → J) [X.HasMap p] [Y.HasMap p] (i : J) : (mapIso e p).inv i = mapMap e.inv p i

noncomputable def CategoryTheory.GradedObject.map {I : Type u_1} {J : Type u_2} (C : Type u_4) [Category.{u_5, u_4} C] (p : I → J) [∀ (j : J), Limits.HasColimitsOfShape (Discrete ↑(p ⁻¹' {j})) C] : Functor (GradedObject I C) (GradedObject J C)

Given a map p : I → J, this is the functor GradedObject I C ⥤ GradedObject J C which sends an I-object X to the graded object X.mapObj p which in degree j : J is given by the coproduct of those X i such that p i = j.

Equations

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

@[simp]

theorem CategoryTheory.GradedObject.map_obj {I : Type u_1} {J : Type u_2} (C : Type u_4) [Category.{u_5, u_4} C] (p : I → J) [∀ (j : J), Limits.HasColimitsOfShape (Discrete ↑(p ⁻¹' {j})) C] (X : GradedObject I C) : (map C p).obj X = X.mapObj p

@[simp]

theorem CategoryTheory.GradedObject.map_map {I : Type u_1} {J : Type u_2} (C : Type u_4) [Category.{u_5, u_4} C] (p : I → J) [∀ (j : J), Limits.HasColimitsOfShape (Discrete ↑(p ⁻¹' {j})) C] {X✝ Y✝ : GradedObject I C} (φ : X✝ ⟶ Y✝) (i : J) : (map C p).map φ i = mapMap φ p i

def CategoryTheory.GradedObject.cofanMapObjComp {I : Type u_1} {J : Type u_2} {K : Type u_3} {C : Type u_4} [Category.{u_5, u_4} C] (X : GradedObject I C) (p : I → J) (q : J → K) (r : I → K) (hpqr : ∀ (i : I), q (p i) = r i) (k : K) (c : (j : J) → q j = k → X.CofanMapObjFun p j) (c' : Limits.Cofan fun (j : ↑(q ⁻¹' {k})) => (c ↑j ⋯).pt) : X.CofanMapObjFun r k

Given maps p : I → J, q : J → K and r : I → K such that q.comp p = r, X : GradedObject I C, k : K, the datum of cofans X.CofanMapObjFun p j for all j : J and of a cofan for all the points of these cofans, this is a cofan of type X.CofanMapObjFun r k, which is a colimit (see isColimitCofanMapObjComp) if the given cofans are.

Equations

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

def CategoryTheory.GradedObject.isColimitCofanMapObjComp {I : Type u_1} {J : Type u_2} {K : Type u_3} {C : Type u_4} [Category.{u_5, u_4} C] (X : GradedObject I C) (p : I → J) (q : J → K) (r : I → K) (hpqr : ∀ (i : I), q (p i) = r i) (k : K) (c : (j : J) → q j = k → X.CofanMapObjFun p j) (hc : (j : J) → (hj : q j = k) → Limits.IsColimit (c j hj)) (c' : Limits.Cofan fun (j : ↑(q ⁻¹' {k})) => (c ↑j ⋯).pt) (hc' : Limits.IsColimit c') : Limits.IsColimit (X.cofanMapObjComp p q r hpqr k c c')

Given maps p : I → J, q : J → K and r : I → K such that q.comp p = r, X : GradedObject I C, k : K, the cofan constructed by cofanMapObjComp is a colimit. In other words, if we have, for all j : J such that hj : q j = k, a colimit cofan c j hj which computes the coproduct of the X i such that p i = j, and also a colimit cofan which computes the coproduct of the points of these c j hj, then the point of this latter cofan computes the coproduct of the X i such that r i = k.

Equations

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

theorem CategoryTheory.GradedObject.hasMap_comp {I : Type u_1} {J : Type u_2} {K : Type u_3} {C : Type u_4} [Category.{u_5, u_4} C] (X : GradedObject I C) (p : I → J) [X.HasMap p] (q : J → K) (r : I → K) (hpqr : ∀ (i : I), q (p i) = r i) [(X.mapObj p).HasMap q] : X.HasMap r

noncomputable def CategoryTheory.GradedObject.ιMapObjOrZero {I : Type u_1} {J : Type u_2} {C : Type u_4} [Category.{u_5, u_4} C] (X : GradedObject I C) (p : I → J) [X.HasMap p] [Limits.HasZeroMorphisms C] [DecidableEq J] (i : I) (j : J) : X i ⟶ X.mapObj p j

The canonical inclusion X i ⟶ X.mapObj p j when p i = j, the zero morphism otherwise.

Equations

• X.ιMapObjOrZero p i j = if h : p i = j then X.ιMapObj p i j h else 0

theorem CategoryTheory.GradedObject.ιMapObjOrZero_eq {I : Type u_1} {J : Type u_2} {C : Type u_4} [Category.{u_5, u_4} C] (X : GradedObject I C) (p : I → J) [X.HasMap p] [Limits.HasZeroMorphisms C] [DecidableEq J] (i : I) (j : J) (h : p i = j) : X.ιMapObjOrZero p i j = X.ιMapObj p i j h

theorem CategoryTheory.GradedObject.ιMapObjOrZero_eq_zero {I : Type u_1} {J : Type u_2} {C : Type u_4} [Category.{u_5, u_4} C] (X : GradedObject I C) (p : I → J) [X.HasMap p] [Limits.HasZeroMorphisms C] [DecidableEq J] (i : I) (j : J) (h : p i ≠ j) : X.ιMapObjOrZero p i j = 0

@[simp]

theorem CategoryTheory.GradedObject.ιMapObjOrZero_mapMap {I : Type u_1} {J : Type u_2} {C : Type u_4} [Category.{u_5, u_4} C] {X Y : GradedObject I C} (φ : X ⟶ Y) (p : I → J) [X.HasMap p] [Y.HasMap p] [Limits.HasZeroMorphisms C] [DecidableEq J] (i : I) (j : J) : CategoryStruct.comp (X.ιMapObjOrZero p i j) (mapMap φ p j) = CategoryStruct.comp (φ i) (Y.ιMapObjOrZero p i j)

@[simp]

theorem CategoryTheory.GradedObject.ιMapObjOrZero_mapMap_assoc {I : Type u_1} {J : Type u_2} {C : Type u_4} [Category.{u_5, u_4} C] {X Y : GradedObject I C} (φ : X ⟶ Y) (p : I → J) [X.HasMap p] [Y.HasMap p] [Limits.HasZeroMorphisms C] [DecidableEq J] (i : I) (j : J) {Z : C} (h : Y.mapObj p j ⟶ Z) : CategoryStruct.comp (X.ιMapObjOrZero p i j) (CategoryStruct.comp (mapMap φ p j) h) = CategoryStruct.comp (φ i) (CategoryStruct.comp (Y.ιMapObjOrZero p i j) h)