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₂}  :
C J C

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) :
X).op

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ᵒᵖ) :
= 𝟙 X).left_op.obj 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.