Theorems · Definition · category theory

CategoryTheory.GradedObject.map

{I : Type u_1} →
  {J : Type u_2} →
    (C : Type u_4) →
      [inst : CategoryTheory.Category.{v_1, u_4} C] →
        (p : I → J) →
          [∀ (j : J), CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete ↑(p ⁻¹' {j})) C] →
            CategoryTheory.Functor (CategoryTheory.GradedObject I C) (CategoryTheory.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.

Defined in

Mathlib.CategoryTheory.GradedObject

Cited by

2 results in Mathlib

Foundations

Depth 34 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.Limits.HasColimitsOfShape