mathlib documentation

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ā‚) [category_theory.category J] {C : Type uā‚‚} [category_theory.category 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.