# 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
• = (βC)
Instances For
instance CategoryTheory.inhabitedGradedObject (β : Type w) (C : Type u) [] :
Equations
• = { default := fun (x : β) => default }
@[reducible, inline]
abbrev CategoryTheory.GradedObjectWithShift {β : Type w} [] :
β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
Instances For
@[simp]
theorem CategoryTheory.GradedObject.categoryOfGradedObjects_id {C : Type u} (β : Type w) (X : (i : β) → (fun (x : β) => C) i) (i : β) :
@[simp]
∀ {X Y Z : (i : β) → (fun (x : β) => C) i} (f : X Y) (g : Y Z) (i : β), = CategoryTheory.CategoryStruct.comp (f i) (g i)
Equations
theorem CategoryTheory.GradedObject.hom_ext {C : Type u} {β : Type u_1} {X : } {Y : } (f : X Y) (g : X Y) (h : ∀ (x : β), f x = g x) :
f = g
@[simp]
theorem CategoryTheory.GradedObject.eval_obj {C : Type u} {β : Type w} (b : β) (X : ) :
.obj X = X b
@[simp]
theorem CategoryTheory.GradedObject.eval_map {C : Type u} {β : Type w} (b : β) :
∀ {X Y : } (f : X Y), .map f = f b
def CategoryTheory.GradedObject.eval {C : Type u} {β : Type w} (b : β) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem CategoryTheory.GradedObject.isoMk_hom {C : Type u} {β : Type u_1} (X : ) (Y : ) (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} {β : Type u_1} (X : ) (Y : ) (e : (i : β) → X i Y i) (i : β) :
(X.isoMk Y e).inv i = (e i).inv
def CategoryTheory.GradedObject.isoMk {C : Type u} {β : Type u_1} (X : ) (Y : ) (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 := }
Instances For
theorem CategoryTheory.GradedObject.isIso_of_isIso_apply {C : Type u} {β : Type u_1} {X : } {Y : } (f : X Y) [hf : ∀ (i : β), CategoryTheory.IsIso (f i)] :
instance CategoryTheory.GradedObject.isIso_apply_of_isIso {C : Type u} {β : Type u_1} {X : } {Y : } (f : X Y) (i : β) :
Equations
• =
@[simp]
theorem CategoryTheory.Iso.hom_inv_id_eval_assoc {C : Type u_1} {J : Type u_4} [] {X : } {Y : } (e : X Y) (j : J) {Z : C} (h : X j Z) :
@[simp]
theorem CategoryTheory.Iso.hom_inv_id_eval {C : Type u_1} {J : Type u_4} [] {X : } {Y : } (e : X Y) (j : J) :
@[simp]
theorem CategoryTheory.Iso.inv_hom_id_eval_assoc {C : Type u_1} {J : Type u_4} [] {X : } {Y : } (e : X Y) (j : J) {Z : C} (h : Y j Z) :
@[simp]
theorem CategoryTheory.Iso.inv_hom_id_eval {C : Type u_1} {J : Type u_4} [] {X : } {Y : } (e : X Y) (j : J) :
@[simp]
theorem CategoryTheory.Iso.map_hom_inv_id_eval_assoc {C : Type u_1} {D : Type u_2} {J : Type u_4} [] [] {X : } {Y : } (e : X Y) (F : ) (j : J) {Z : D} (h : F.obj (X j) Z) :
@[simp]
theorem CategoryTheory.Iso.map_hom_inv_id_eval {C : Type u_1} {D : Type u_2} {J : Type u_4} [] [] {X : } {Y : } (e : X Y) (F : ) (j : J) :
CategoryTheory.CategoryStruct.comp (F.map (e.hom j)) (F.map (e.inv j)) = CategoryTheory.CategoryStruct.id (F.obj (X j))
@[simp]
theorem CategoryTheory.Iso.map_inv_hom_id_eval_assoc {C : Type u_1} {D : Type u_2} {J : Type u_4} [] [] {X : } {Y : } (e : X Y) (F : ) (j : J) {Z : D} (h : F.obj (Y j) Z) :
@[simp]
theorem CategoryTheory.Iso.map_inv_hom_id_eval {C : Type u_1} {D : Type u_2} {J : Type u_4} [] [] {X : } {Y : } (e : X Y) (F : ) (j : J) :
CategoryTheory.CategoryStruct.comp (F.map (e.inv j)) (F.map (e.hom j)) = CategoryTheory.CategoryStruct.id (F.obj (Y j))
@[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} [] [] [] {X : } {Y : } (e : X Y✝) (F : ) (j : J) (Y : D) {Z : E} (h : (F.obj (X j)).obj Y Z) :
CategoryTheory.CategoryStruct.comp ((F.map (e.hom j)).app Y) (CategoryTheory.CategoryStruct.comp ((F.map (e.inv j)).app Y) 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} [] [] [] {X : } {Y : } (e : X Y✝) (F : ) (j : J) (Y : D) :
CategoryTheory.CategoryStruct.comp ((F.map (e.hom j)).app Y) ((F.map (e.inv j)).app Y) = CategoryTheory.CategoryStruct.id ((F.obj (X 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} [] [] [] {X : } {Y : } (e : X Y✝) (F : ) (j : J) (Y : D) {Z : E} (h : (F.obj (Y✝ j)).obj Y Z) :
CategoryTheory.CategoryStruct.comp ((F.map (e.inv j)).app Y) (CategoryTheory.CategoryStruct.comp ((F.map (e.hom 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} [] [] [] {X : } {Y : } (e : X Y✝) (F : ) (j : J) (Y : D) :
CategoryTheory.CategoryStruct.comp ((F.map (e.inv j)).app Y) ((F.map (e.hom j)).app Y) = CategoryTheory.CategoryStruct.id ((F.obj (Y✝ j)).obj Y)
@[reducible, inline]
abbrev CategoryTheory.GradedObject.comap (C : Type u) {I : Type u_1} {J : Type u_2} (h : JI) :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.GradedObject.eqToHom_proj (C : Type u) {I : Type u_1} {x : } {x' : } (h : x = x') (i : I) :
@[simp]
theorem CategoryTheory.GradedObject.comapEq_inv_app (C : Type u) {β : Type w} {γ : Type w} {f : βγ} {g : βγ} (h : f = g) (X : ) (b : β) :
.inv.app X b =
@[simp]
theorem CategoryTheory.GradedObject.comapEq_hom_app (C : Type u) {β : Type w} {γ : Type w} {f : βγ} {g : βγ} (h : f = g) (X : ) (b : β) :
.hom.app X b =
def CategoryTheory.GradedObject.comapEq (C : Type u) {β : Type w} {γ : Type w} {f : βγ} {g : βγ} (h : f = 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.
Instances For
theorem CategoryTheory.GradedObject.comapEq_symm (C : Type u) {β : Type w} {γ : Type w} {f : βγ} {g : βγ} (h : f = g) :
theorem CategoryTheory.GradedObject.comapEq_trans (C : Type u) {β : Type w} {γ : Type w} {f : βγ} {g : βγ} {h : βγ} (k : f = g) (l : g = h) :
theorem CategoryTheory.GradedObject.eqToHom_apply (C : Type u) {β : Type w} {X : βC} {Y : βC} (h : X = Y) (b : β) :
@[simp]
theorem CategoryTheory.GradedObject.comapEquiv_functor (C : Type u) {β : Type w} {γ : Type w} (e : β γ) :
.functor =
@[simp]
theorem CategoryTheory.GradedObject.comapEquiv_inverse (C : Type u) {β : Type w} {γ : Type w} (e : β γ) :
.inverse =
@[simp]
theorem CategoryTheory.GradedObject.comapEquiv_unitIso (C : Type u) {β : Type w} {γ : Type w} (e : β γ) :
.unitIso = ≪≫ (CategoryTheory.Pi.comapComp (fun (x : β) => C) e e.symm).symm
@[simp]
theorem CategoryTheory.GradedObject.comapEquiv_counitIso (C : Type u) {β : Type w} {γ : Type w} (e : β γ) :
.counitIso = CategoryTheory.Pi.comapComp (fun (x : γ) => C) e.symm e ≪≫
def CategoryTheory.GradedObject.comapEquiv (C : Type u) {β : Type w} {γ : Type w} (e : β γ) :

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.
Instances For
instance CategoryTheory.GradedObject.hasShift {C : Type u} {β : Type u_1} [] (s : β) :
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem CategoryTheory.GradedObject.shiftFunctor_obj_apply {C : Type u} {β : Type u_1} [] (s : β) (X : βC) (t : β) (n : ) :
X t = X (t + n s)
@[simp]
theorem CategoryTheory.GradedObject.shiftFunctor_map_apply {C : Type u} {β : Type u_1} [] (s : β) {X : } {Y : } (f : X Y) (t : β) (n : ) :
f t = f (t + n s)
instance CategoryTheory.GradedObject.instZeroHomOfHasZeroMorphisms {C : Type u} (β : Type w) (X : ) (Y : ) :
Zero (X Y)
Equations
• = { zero := fun (x : β) => 0 }
@[simp]
theorem CategoryTheory.GradedObject.zero_apply {C : Type u} (β : Type w) (X : ) (Y : ) (b : β) :
0 b = 0
Equations
Equations
• =
noncomputable def CategoryTheory.GradedObject.total (β : Type) (C : Type u) :

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.
Instances For
instance CategoryTheory.GradedObject.instFaithfulTotal (β : Type) (C : Type u) :
.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.

Equations
• =
Equations
Equations
• = { forget₂ := , forget_comp := }
@[reducible, inline]
abbrev CategoryTheory.GradedObject.mapObjFun {I : Type u_1} {J : Type u_2} {C : Type u_4} (X : ) (p : IJ) (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
Instances For
@[reducible, inline]
abbrev CategoryTheory.GradedObject.HasMap {I : Type u_1} {J : Type u_2} {C : Type u_4} [] (X : ) (p : IJ) :

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
Instances For
theorem CategoryTheory.GradedObject.hasMap_of_iso {I : Type u_1} {J : Type u_2} {C : Type u_4} [] {X : } {Y : } (e : X Y) (p : IJ) [X.HasMap p] :
Y.HasMap p
noncomputable def CategoryTheory.GradedObject.mapObj {I : Type u_1} {J : Type u_2} {C : Type u_4} [] (X : ) (p : IJ) [X.HasMap p] :

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
Instances For
noncomputable def CategoryTheory.GradedObject.ιMapObj {I : Type u_1} {J : Type u_2} {C : Type u_4} [] (X : ) (p : IJ) [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
Instances For
@[reducible, inline]
abbrev CategoryTheory.GradedObject.CofanMapObjFun {I : Type u_1} {J : Type u_2} {C : Type u_4} [] (X : ) (p : IJ) (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
Instances For
def CategoryTheory.GradedObject.CofanMapObjFun.mk {I : Type u_1} {J : Type u_2} {C : Type u_4} [] (X : ) (p : IJ) (j : J) (pt : C) (ι' : (i : I) → p i = j(X i pt)) :
X.CofanMapObjFun p j

Constructor for CofanMapObjFun X p j.

Equations
Instances For
noncomputable def CategoryTheory.GradedObject.cofanMapObj {I : Type u_1} {J : Type u_2} {C : Type u_4} [] (X : ) (p : IJ) [X.HasMap p] (j : J) :
X.CofanMapObjFun p j

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

Equations
Instances For
noncomputable def CategoryTheory.GradedObject.isColimitCofanMapObj {I : Type u_1} {J : Type u_2} {C : Type u_4} [] (X : ) (p : IJ) [X.HasMap p] (j : 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
Instances For
theorem CategoryTheory.GradedObject.mapObj_ext {I : Type u_1} {J : Type u_2} {C : Type u_4} [] (X : ) (p : IJ) [X.HasMap p] {A : C} {j : J} (f : X.mapObj p j A) (g : X.mapObj p j A) (hfg : ∀ (i : I) (hij : p i = j), CategoryTheory.CategoryStruct.comp (X.ιMapObj p i j hij) f = CategoryTheory.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} [] (X : ) (p : IJ) [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
Instances For
@[simp]
theorem CategoryTheory.GradedObject.ι_descMapObj_assoc {I : Type u_1} {J : Type u_2} {C : Type u_4} [] (X : ) (p : IJ) [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) :
@[simp]
theorem CategoryTheory.GradedObject.ι_descMapObj {I : Type u_1} {J : Type u_2} {C : Type u_4} [] (X : ) (p : IJ) [X.HasMap p] {A : C} {j : J} (φ : (i : I) → p i = j(X i A)) (i : I) (hi : p i = j) :
CategoryTheory.CategoryStruct.comp (X.ιMapObj p i j hi) (X.descMapObj p φ) = φ i hi
theorem CategoryTheory.GradedObject.CofanMapObjFun.hasMap {I : Type u_1} {J : Type u_2} {C : Type u_4} [] (X : ) (p : IJ) (c : (j : J) → X.CofanMapObjFun p j) (hc : (j : J) → ) :
X.HasMap p
noncomputable def CategoryTheory.GradedObject.CofanMapObjFun.iso {I : Type u_1} {J : Type u_2} {C : Type u_4} [] {X : } {p : IJ} {j : J} [X.HasMap p] {c : X.CofanMapObjFun p j} (hc : ) :
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
• = hc.coconePointUniqueUpToIso (X.isColimitCofanMapObj p j)
Instances For
@[simp]
theorem CategoryTheory.GradedObject.CofanMapObjFun.inj_iso_hom_assoc {I : Type u_1} {J : Type u_2} {C : Type u_4} [] {X : } {p : IJ} {j : J} [X.HasMap p] {c : X.CofanMapObjFun p j} (hc : ) (i : I) (hi : p i = j) {Z : C} (h : X.mapObj p j Z) :
= CategoryTheory.CategoryStruct.comp (X.ιMapObj p i j hi) h
@[simp]
theorem CategoryTheory.GradedObject.CofanMapObjFun.inj_iso_hom {I : Type u_1} {J : Type u_2} {C : Type u_4} [] {X : } {p : IJ} {j : J} [X.HasMap p] {c : X.CofanMapObjFun p j} (hc : ) (i : I) (hi : p i = j) :
= X.ιMapObj p i j hi
@[simp]
theorem CategoryTheory.GradedObject.CofanMapObjFun.ιMapObj_iso_inv_assoc {I : Type u_1} {J : Type u_2} {C : Type u_4} [] {X : } {p : IJ} {j : J} [X.HasMap p] {c : X.CofanMapObjFun p j} (hc : ) (i : I) (hi : p i = j) {Z : C} (h : c.pt Z) :
CategoryTheory.CategoryStruct.comp (X.ιMapObj p i j hi) =
@[simp]
theorem CategoryTheory.GradedObject.CofanMapObjFun.ιMapObj_iso_inv {I : Type u_1} {J : Type u_2} {C : Type u_4} [] {X : } {p : IJ} {j : J} [X.HasMap p] {c : X.CofanMapObjFun p j} (hc : ) (i : I) (hi : p i = j) :
noncomputable def CategoryTheory.GradedObject.mapMap {I : Type u_1} {J : Type u_2} {C : Type u_4} [] {X : } {Y : } (φ : X Y) (p : IJ) [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
Instances For
@[simp]
theorem CategoryTheory.GradedObject.ι_mapMap_assoc {I : Type u_1} {J : Type u_2} {C : Type u_4} [] {X : } {Y : } (φ : X Y) (p : IJ) [X.HasMap p] [Y.HasMap p] (i : I) (j : J) (hij : p i = j) {Z : C} (h : Y.mapObj p j Z) :
@[simp]
theorem CategoryTheory.GradedObject.ι_mapMap {I : Type u_1} {J : Type u_2} {C : Type u_4} [] {X : } {Y : } (φ : X Y) (p : IJ) [X.HasMap p] [Y.HasMap p] (i : I) (j : J) (hij : p i = j) :
CategoryTheory.CategoryStruct.comp (X.ιMapObj p i j hij) = CategoryTheory.CategoryStruct.comp (φ i) (Y.ιMapObj p i j hij)
theorem CategoryTheory.GradedObject.congr_mapMap {I : Type u_1} {J : Type u_2} {C : Type u_4} [] {X : } {Y : } (p : IJ) [X.HasMap p] [Y.HasMap p] (φ₁ : X Y) (φ₂ : X Y) (h : φ₁ = φ₂) :
@[simp]
theorem CategoryTheory.GradedObject.mapMap_id {I : Type u_1} {J : Type u_2} {C : Type u_4} [] (X : ) (p : IJ) [X.HasMap p] :
theorem CategoryTheory.GradedObject.mapMap_comp_assoc {I : Type u_1} {J : Type u_2} {C : Type u_4} [] {X : } {Y : } {Z : } (φ : X Y) (ψ : Y Z✝) (p : IJ) [X.HasMap p] [Y.HasMap p] [Z✝.HasMap p] {Z : } (h : Z✝.mapObj p Z) :
@[simp]
theorem CategoryTheory.GradedObject.mapMap_comp {I : Type u_1} {J : Type u_2} {C : Type u_4} [] {X : } {Y : } {Z : } (φ : X Y) (ψ : Y Z) (p : IJ) [X.HasMap p] [Y.HasMap p] [Z.HasMap p] :
@[simp]
theorem CategoryTheory.GradedObject.mapIso_inv {I : Type u_1} {J : Type u_2} {C : Type u_4} [] {X : } {Y : } (e : X Y) (p : IJ) [X.HasMap p] [Y.HasMap p] (i : J) :
.inv i =
@[simp]
theorem CategoryTheory.GradedObject.mapIso_hom {I : Type u_1} {J : Type u_2} {C : Type u_4} [] {X : } {Y : } (e : X Y) (p : IJ) [X.HasMap p] [Y.HasMap p] (i : J) :
.hom i =
noncomputable def CategoryTheory.GradedObject.mapIso {I : Type u_1} {J : Type u_2} {C : Type u_4} [] {X : } {Y : } (e : X Y) (p : IJ) [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
• = { hom := , inv := , hom_inv_id := , inv_hom_id := }
Instances For
@[simp]
theorem CategoryTheory.GradedObject.map_obj {I : Type u_1} {J : Type u_2} (C : Type u_4) [] (p : IJ) [∀ (j : J), ] (X : ) :
.obj X = X.mapObj p
@[simp]
theorem CategoryTheory.GradedObject.map_map {I : Type u_1} {J : Type u_2} (C : Type u_4) [] (p : IJ) [∀ (j : J), ] :
∀ {X Y : } (φ : X Y) (i : J), .map φ i =
noncomputable def CategoryTheory.GradedObject.map {I : Type u_1} {J : Type u_2} (C : Type u_4) [] (p : IJ) [∀ (j : J), ] :

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.
Instances For
def CategoryTheory.GradedObject.cofanMapObjComp {I : Type u_1} {J : Type u_2} {K : Type u_3} {C : Type u_4} [] (X : ) (p : IJ) (q : JK) (r : IK) (hpqr : ∀ (i : I), q (p i) = r i) (k : K) (c : (j : J) → q j = kX.CofanMapObjFun p j) (c' : CategoryTheory.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.
Instances For
def CategoryTheory.GradedObject.isColimitCofanMapObjComp {I : Type u_1} {J : Type u_2} {K : Type u_3} {C : Type u_4} [] (X : ) (p : IJ) (q : JK) (r : IK) (hpqr : ∀ (i : I), q (p i) = r i) (k : K) (c : (j : J) → q j = kX.CofanMapObjFun p j) (hc : (j : J) → (hj : q j = k) → CategoryTheory.Limits.IsColimit (c j hj)) (c' : CategoryTheory.Limits.Cofan fun (j : (q ⁻¹' {k})) => (c j ).pt) (hc' : ) :
CategoryTheory.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.
Instances For
theorem CategoryTheory.GradedObject.hasMap_comp {I : Type u_1} {J : Type u_2} {K : Type u_3} {C : Type u_4} [] (X : ) (p : IJ) [X.HasMap p] (q : JK) (r : IK) (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} [] (X : ) (p : IJ) [X.HasMap p] [] (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
Instances For
theorem CategoryTheory.GradedObject.ιMapObjOrZero_eq {I : Type u_1} {J : Type u_2} {C : Type u_4} [] (X : ) (p : IJ) [X.HasMap p] [] (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} [] (X : ) (p : IJ) [X.HasMap p] [] (i : I) (j : J) (h : p i j) :
X.ιMapObjOrZero p i j = 0
@[simp]
theorem CategoryTheory.GradedObject.ιMapObjOrZero_mapMap_assoc {I : Type u_1} {J : Type u_2} {C : Type u_4} [] {X : } {Y : } (φ : X Y) (p : IJ) [X.HasMap p] [Y.HasMap p] [] (i : I) (j : J) {Z : C} (h : Y.mapObj p j Z) :
@[simp]
theorem CategoryTheory.GradedObject.ιMapObjOrZero_mapMap {I : Type u_1} {J : Type u_2} {C : Type u_4} [] {X : } {Y : } (φ : X Y) (p : IJ) [X.HasMap p] [Y.HasMap p] [] (i : I) (j : J) :
CategoryTheory.CategoryStruct.comp (X.ιMapObjOrZero p i j) = CategoryTheory.CategoryStruct.comp (φ i) (Y.ιMapObjOrZero p i j)