Theorems · Definition · category theory

CategoryTheory.GradedObject.mapMap

{I : Type u_1} →
  {J : Type u_2} →
    {C : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_4} C] →
        {X Y : CategoryTheory.GradedObject I C} →
          (X ⟶ Y) → (p : I → J) → [inst_1 : X.HasMap p] → [inst_2 : 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.

Defined in

Mathlib.CategoryTheory.GradedObject

Cited by

22 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.GradedObject.HasMapCategoryTheory.GradedObject.HasMap