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.
@[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) :
((category_theory.functor.const J).obj X).obj j = X
@[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') :
((category_theory.functor.const J).obj X).map f = š X
@[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) :
((category_theory.functor.const J).map f).app j = f
def
category_theory.functor.const.op_obj_op
{J : Type uā}
[category_theory.category J]
{C : Type uā}
[category_theory.category C]
(X : C) :
(category_theory.functor.const Jįµįµ).obj (opposite.op X) ā
((category_theory.functor.const J).obj 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
- category_theory.functor.const.op_obj_op X = {hom := {app := Ī» (j : Jįµįµ), š (((category_theory.functor.const Jįµįµ).obj (opposite.op X)).obj j), naturality' := _}, inv := {app := Ī» (j : Jįµįµ), š (((category_theory.functor.const J).obj X).op.obj j), naturality' := _}, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.functor.const.op_obj_op_hom_app
{J : Type uā}
[category_theory.category J]
{C : Type uā}
[category_theory.category C]
(X : C)
(j : Jįµįµ) :
(category_theory.functor.const.op_obj_op X).hom.app j = š (((category_theory.functor.const Jįµįµ).obj (opposite.op X)).obj j)
@[simp]
theorem
category_theory.functor.const.op_obj_op_inv_app
{J : Type uā}
[category_theory.category J]
{C : Type uā}
[category_theory.category C]
(X : C)
(j : Jįµįµ) :
(category_theory.functor.const.op_obj_op X).inv.app j = š (((category_theory.functor.const J).obj X).op.obj j)
def
category_theory.functor.const.op_obj_unop
{J : Type uā}
[category_theory.category J]
{C : Type uā}
[category_theory.category C]
(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
- category_theory.functor.const.op_obj_unop X = {hom := {app := Ī» (j : Jįµįµ), š (((category_theory.functor.const Jįµįµ).obj (opposite.unop X)).obj j), naturality' := _}, inv := {app := Ī» (j : Jįµįµ), š (((category_theory.functor.const J).obj X).left_op.obj j), naturality' := _}, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.functor.const.op_obj_unop_hom_app
{J : Type uā}
[category_theory.category J]
{C : Type uā}
[category_theory.category C]
(X : Cįµįµ)
(j : Jįµįµ) :
(category_theory.functor.const.op_obj_unop X).hom.app j = š (((category_theory.functor.const Jįµįµ).obj (opposite.unop X)).obj j)
@[simp]
theorem
category_theory.functor.const.op_obj_unop_inv_app
{J : Type uā}
[category_theory.category J]
{C : Type uā}
[category_theory.category C]
(X : Cįµįµ)
(j : Jįµįµ) :
(category_theory.functor.const.op_obj_unop X).inv.app j = š (((category_theory.functor.const J).obj X).left_op.obj j)
@[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ā) :
(opposite.unop ((category_theory.functor.const J).op.obj X)).map f = š (opposite.unop X)
def
category_theory.functor.const_comp
(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) :
(category_theory.functor.const J).obj X ā F ā
(category_theory.functor.const J).obj (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
- category_theory.functor.const_comp J X F = {hom := {app := Ī» (_x : J), š (((category_theory.functor.const J).obj X ā F).obj _x), naturality' := _}, inv := {app := Ī» (_x : J), š (((category_theory.functor.const J).obj (F.obj X)).obj _x), naturality' := _}, hom_inv_id' := _, inv_hom_id' := _}
@[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) :
(category_theory.functor.const_comp J X F).hom.app _x = š (((category_theory.functor.const J).obj X ā F).obj _x)
@[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) :
(category_theory.functor.const_comp J X F).inv.app _x = š (((category_theory.functor.const J).obj (F.obj X)).obj _x)
@[protected, instance]
def
category_theory.functor.const.category_theory.faithful
(J : Type uā)
[category_theory.category J]
{C : Type uā}
[category_theory.category C]
[nonempty J] :
If J is nonempty, then the constant functor over J is faithful.