# mathlibdocumentation

category_theory.const

# The constant functor #

const J : C ā„¤ (J ā„¤ C) is the functor that sends an object X : C to the functor J ā„¤ C sending every object in J to X, and every morphism to š X.

When J is nonempty, const is faithful.

We have (const J).obj X ā F ā (const J).obj (F.obj X) for any F : C ā„¤ D.

def category_theory.functor.const (J : Type uā) {C : Type uā}  :

The functor sending X : C to the constant functor J ā„¤ C sending everything to X.

Equations
@[simp]
theorem category_theory.functor.const.obj_obj {J : Type uā} {C : Type uā} (X : C) (j : J) :
X).obj j = X
@[simp]
theorem category_theory.functor.const.obj_map {J : Type uā} {C : Type uā} (X : C) {j j' : J} (f : j ā¶ j') :
X).map f = š X
@[simp]
theorem category_theory.functor.const.map_app {J : Type uā} {C : Type uā} {X Y : C} (f : X ā¶ Y) (j : J) :
f).app j = f
def category_theory.functor.const.op_obj_op {J : Type uā} {C : Type uā} (X : C) :

The contant functor Jįµįµ ā„¤ Cįµįµ sending everything to op X is (naturally isomorphic to) the opposite of the constant functor J ā„¤ C sending everything to X.

Equations
@[simp]
theorem category_theory.functor.const.op_obj_op_hom_app {J : Type uā} {C : Type uā} (X : C) (j : Jįµįµ) :
@[simp]
theorem category_theory.functor.const.op_obj_op_inv_app {J : Type uā} {C : Type uā} (X : C) (j : Jįµįµ) :
= š X).op.obj j)
def category_theory.functor.const.op_obj_unop {J : Type uā} {C : Type uā} (X : Cįµįµ) :

The contant functor Jįµįµ ā„¤ C sending everything to unop X is (naturally isomorphic to) the opposite of the constant functor J ā„¤ Cįµįµ sending everything to X.

Equations
@[simp]
theorem category_theory.functor.const.op_obj_unop_hom_app {J : Type uā} {C : Type uā} (X : Cįµįµ) (j : Jįµįµ) :
@[simp]
theorem category_theory.functor.const.op_obj_unop_inv_app {J : Type uā} {C : Type uā} (X : Cįµįµ) (j : Jįµįµ) :
@[simp]
theorem category_theory.functor.const.unop_functor_op_obj_map {J : Type uā} {C : Type uā} (X : Cįµįµ) {jā jā : J} (f : jā ā¶ jā) :
def category_theory.functor.const_comp (J : Type uā) {C : Type uā} {D : Type uā} (X : C) (F : C ā„¤ D) :
ā (F.obj X)

These are actually equal, of course, but not definitionally equal (the equality requires F.map (š _) = š _). A natural isomorphism is more convenient than an equality between functors (compare id_to_iso).

Equations
@[simp]
theorem category_theory.functor.const_comp_hom_app (J : Type uā) {C : Type uā} {D : Type uā} (X : C) (F : C ā„¤ D) (_x : J) :
.app _x = š X ā F).obj _x)
@[simp]
theorem category_theory.functor.const_comp_inv_app (J : Type uā) {C : Type uā} {D : Type uā} (X : C) (F : C ā„¤ D) (_x : J) :
.app _x = š (F.obj X)).obj _x)
@[protected, instance]
def category_theory.functor.const.category_theory.faithful (J : Type uā) {C : Type uā} [nonempty J] :

If J is nonempty, then the constant functor over J is faithful.