CategoryTheory.Functor.const_obj_map
theorem CategoryTheory.Functor.const_obj_map :
ā (J : Type uā) [inst : CategoryTheory.Category.{vā, uā} J] {C : Type uā}
[inst_1 : CategoryTheory.Category.{vā, uā} C] (X : C) {X_1 Y : J} (x : X_1 ā¶ Y),
((CategoryTheory.Functor.const J).obj X).map x = CategoryTheory.CategoryStruct.id X
The theorem `CategoryTheory.Functor.const_obj_map` states that for any type `J` with a category structure, any type `C` with a category structure, and any object `X` of type `C`, for any two objects `X_1` and `Y` of type `J` and a morphism `x` from `X_1` to `Y`, the map induced by the constant functor at `X` applied to the morphism `x` is equal to the identity morphism on `X`. In other words, the constant functor sends every morphism in the domain category to the identity morphism in the codomain category.
More concisely: For any category structures on types J and C, and any object X of C, the constant functor from J to C maps every morphism from an object X1 to an object Y in J to the identity morphism on X in C.
|