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.

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

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

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

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.

@[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) (j : Jᵒᵖ) : (CategoryTheory.Functor.const.opObjOp X).inv.app j = CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.const J).obj X).op.obj j)

@[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) (j : Jᵒᵖ) : (CategoryTheory.Functor.const.opObjOp X).hom.app j = CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.const Jᵒᵖ).obj (Opposite.op X)).obj j)

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.

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 X.unop ≅ ((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.

@[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 X.unop).obj j)

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

@[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₂) : ((CategoryTheory.Functor.const J).op.obj X).unop.map f = CategoryTheory.CategoryStruct.id X.unop

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

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

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

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

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

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

Equations

• ⋯ = ⋯

@[simp]

theorem CategoryTheory.Functor.compConstIso_hom_app_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] (F : CategoryTheory.Functor C D) (X : C) (X : J) : ((CategoryTheory.Functor.compConstIso J F).hom.app X✝).app X = CategoryTheory.CategoryStruct.id (F.obj X✝)

@[simp]

theorem CategoryTheory.Functor.compConstIso_inv_app_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] (F : CategoryTheory.Functor C D) (X : C) (X : J) : ((CategoryTheory.Functor.compConstIso J F).inv.app X✝).app X = CategoryTheory.CategoryStruct.id (F.obj X✝)

def CategoryTheory.Functor.compConstIso (J : Type u₁) [CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [CategoryTheory.Category.{v₂, u₂} C] {D : Type u₃} [CategoryTheory.Category.{v₃, u₃} D] (F : CategoryTheory.Functor C D) : CategoryTheory.Functor.comp F (CategoryTheory.Functor.const J) ≅ CategoryTheory.Functor.comp (CategoryTheory.Functor.const J) ((CategoryTheory.whiskeringRight J C D).obj F)

The canonical isomorphism F ⋙ Functor.const J ≅ Functor.const F ⋙ (whiskeringRight J _ _).obj L.

Equations

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