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 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_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

@[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✝ Y✝ : J} (x✝ : X✝ ⟶ Y✝) : ((CategoryTheory.Functor.const J).obj X).map x✝ = CategoryTheory.CategoryStruct.id X

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

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.

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

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

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.

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

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

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

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

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

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

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

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

@[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.constCompWhiskeringLeftIso (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 J D) : (CategoryTheory.Functor.const D).comp ((CategoryTheory.whiskeringLeft J D C).obj F) ≅ CategoryTheory.Functor.const J

The canonical isomorphism const D ⋙ (whiskeringLeft J _ _).obj F ≅ const J.

Equations

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

@[simp]

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

@[simp]

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