Theorems · Definition · category theory

CategoryTheory.GradedObject.mapObjFun

{I : Type u_1} →
  {J : Type u_2} → {C : Type u_4} → CategoryTheory.GradedObject I C → (p : I → J) → (j : J) → ↑(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.

Defined in

Mathlib.CategoryTheory.GradedObject

Cited by

13 results in Mathlib

Foundations

Depth 5 from the axioms · uses no axioms