mathlib documentation

category_theory.functor.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.

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

Equations
Instances for category_theory.functor.const
@[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]
@[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]

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
@[protected, instance]

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