Theorems · Theorem · category theory

CategoryTheory.ReflPrefunctor.map_id

∀ {V : Type u₁} [inst : CategoryTheory.ReflQuiver V] {W : Type u₂} [inst_1 : CategoryTheory.ReflQuiver W]
  (self : V ⥤rq W) (X : V), self.map (CategoryTheory.ReflQuiver.id X) = CategoryTheory.ReflQuiver.id (self.obj X)

A functor preserves identity morphisms.

Defined in

Mathlib.Combinatorics.Quiver.ReflQuiver

Cited by

0 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

CategoryTheory.ReflQuiverCategoryTheory.ReflQuiver