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.

source

@[simp]

theorem CategoryTheory.Functor.const_obj_obj (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] (X : C) :

∀ (x : J), ((CategoryTheory.Functor.const J).obj X).obj x = X

source

@[simp]

theorem CategoryTheory.Functor.const_obj_map (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] (X : C) :

∀ {X_1 Y : J} (x : X_1 ⟶ Y), ((CategoryTheory.Functor.const J).obj X).map x = CategoryTheory.CategoryStruct.id X

source

@[simp]

theorem CategoryTheory.Functor.const_map_app (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] :

∀ {X Y : C} (f : X ⟶ Y) (x : J), ((CategoryTheory.Functor.const J).map f).app x = f

source

def CategoryTheory.Functor.const (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] :

CategoryTheory.Functor C (CategoryTheory.Functor J C)

The functor sending X : C to the constant functor J ⥤ C sending everything to X.

Equations

One or more equations did not get rendered due to their size.

source

@[simp]

theorem CategoryTheory.Functor.const.opObjOp_inv_app {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] (X : C) :

∀ (x : Jᵒᵖ), (CategoryTheory.Functor.const.opObjOp X).inv.app x = CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.const J).obj X).op.obj x)

source

@[simp]

theorem CategoryTheory.Functor.const.opObjOp_hom_app {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] (X : C) :

∀ (x : Jᵒᵖ), (CategoryTheory.Functor.const.opObjOp X).hom.app x = CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.const Jᵒᵖ).obj (Opposite.op X)).obj x)

source

def CategoryTheory.Functor.const.opObjOp {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] (X : C) :

(CategoryTheory.Functor.const Jᵒᵖ).obj (Opposite.op X) ≅ ((CategoryTheory.Functor.const J).obj X).op

The constant 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

One or more equations did not get rendered due to their size.

source

def CategoryTheory.Functor.const.opObjUnop {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] (X : Cᵒᵖ) :

(CategoryTheory.Functor.const Jᵒᵖ).obj (Opposite.unop X) ≅ ((CategoryTheory.Functor.const J).obj X).leftOp

The constant 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

One or more equations did not get rendered due to their size.

source

@[simp]

theorem CategoryTheory.Functor.const.opObjUnop_hom_app {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] (X : Cᵒᵖ) (j : Jᵒᵖ) :

(CategoryTheory.Functor.const.opObjUnop X).hom.app j = CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.const Jᵒᵖ).obj (Opposite.unop X)).obj j)

source

@[simp]

theorem CategoryTheory.Functor.const.opObjUnop_inv_app {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] (X : Cᵒᵖ) (j : Jᵒᵖ) :

(CategoryTheory.Functor.const.opObjUnop X).inv.app j = CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.const J).obj X).leftOp.obj j)

source

@[simp]

theorem CategoryTheory.Functor.const.unop_functor_op_obj_map {J : Type u₁} [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] (X : Cᵒᵖ) {j₁ : J} {j₂ : J} (f : j₁ ⟶ j₂) :

(Opposite.unop ((CategoryTheory.Functor.const J).op.obj X)).map f = CategoryTheory.CategoryStruct.id (Opposite.unop X)

source

@[simp]

theorem CategoryTheory.Functor.constComp_inv_app (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] (X : C) (F : CategoryTheory.Functor C D) :

∀ (x : J), (CategoryTheory.Functor.constComp J X F).inv.app x = CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.const J).obj (F.obj X)).obj x)

source

@[simp]

theorem CategoryTheory.Functor.constComp_hom_app (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] (X : C) (F : CategoryTheory.Functor C D) :

∀ (x : J), (CategoryTheory.Functor.constComp J X F).hom.app x = CategoryTheory.CategoryStruct.id ((((CategoryTheory.Functor.const J).obj X).comp F).obj x)

source

def CategoryTheory.Functor.constComp (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] (X : C) (F : CategoryTheory.Functor C D) :

((CategoryTheory.Functor.const J).obj X).comp F ≅ (CategoryTheory.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