The constant functor #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source

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

category_theory.functor.const J = {obj := λ (X : C), {obj := λ (j : J), X, map := λ (j j' : J) (f : j ⟶ j'), 𝟙 X, map_id' := _, map_comp' := _}, map := λ (X Y : C) (f : X ⟶ Y), {app := λ (j : J), f, naturality' := _}, map_id' := _, map_comp' := _}

Instances for category_theory.functor.const

source

@[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

source

@[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

source

@[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

source

@[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)

source

@[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)

source

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' := _}

source

def category_theory.functor.const.op_obj_unop {J : Type u₁} [category_theory.category J] {C : Type u₂} [category_theory.category C] (X : Cᵒᵖ) :

(category_theory.functor.const Jᵒᵖ).obj (opposite.unop X) ≅ ((category_theory.functor.const J).obj X).left_op

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' := _}

source

@[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)

source

@[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)

source

@[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)

source

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' := _}

source

@[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)

source

@[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)

source

@[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] :

category_theory.faithful (category_theory.functor.const J)

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