mathlib documentation

category_theory.const

def category_theory.functor.const (J : Type u₁) [category_theory.category J] {C : Type u₂} [category_theory.category C] :
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₁} [category_theory.category J] {C : Type u₂} [category_theory.category C] (X : C) (j : J) :

@[simp]
theorem category_theory.functor.const.obj_map {J : Type u₁} [category_theory.category J] {C : Type u₂} [category_theory.category C] (X : C) {j j' : J} (f : j j') :

@[simp]
theorem category_theory.functor.const.map_app {J : Type u₁} [category_theory.category J] {C : Type u₂} [category_theory.category C] {X Y : C} (f : X Y) (j : J) :

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

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.unop_functor_op_obj_map {J : Type u₁} [category_theory.category J] {C : Type u₂} [category_theory.category C] (X : Cᵒᵖ) {j₁ j₂ : J} (f : j₁ j₂) :

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₁) [category_theory.category J] {C : Type u₂} [category_theory.category C] {D : Type u₃} [category_theory.category D] (X : C) (F : C D) (_x : J) :

@[simp]
theorem category_theory.functor.const_comp_inv_app (J : Type u₁) [category_theory.category J] {C : Type u₂} [category_theory.category C] {D : Type u₃} [category_theory.category D] (X : C) (F : C D) (_x : J) :

@[instance]

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