Theorems · Definition · category theory

CategoryTheory.GradedObject.HasMap

{I : Type u_1} →
  {J : Type u_2} →
    {C : Type u_4} → [CategoryTheory.Category.{v_1, u_4} C] → CategoryTheory.GradedObject I C → (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.

Defined in

Mathlib.CategoryTheory.GradedObject

Cited by

99 results in Mathlib

Foundations

Depth 14 from the axioms, rests on 89 definitions · uses propext

Assumes

CategoryTheory.Category