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

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

Functor C (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_obj_obj (J : Type u₁) [Category.{v₁, u₁} J] {C : Type u₂} [Category.{v₂, u₂} C] (X : C) (x✝ : J) :

((const J).obj X).obj x✝ = X

source

@[simp]

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

((const J).obj X).map x✝ = CategoryStruct.id X

source

@[simp]

theorem CategoryTheory.Functor.const_map_app (J : Type u₁) [Category.{v₁, u₁} J] {C : Type u₂} [Category.{v₂, u₂} C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (x✝ : J) :

((const J).map f).app x✝ = f

source

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

(const Jᵒᵖ).obj (Opposite.op X) ≅ ((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

@[simp]

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

(opObjOp X).hom.app x✝ = CategoryStruct.id (((const Jᵒᵖ).obj (Opposite.op X)).obj x✝)

source

@[simp]

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

(opObjOp X).inv.app x✝ = CategoryStruct.id (((const J).obj X).op.obj x✝)

source

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

(const Jᵒᵖ).obj (Opposite.unop X) ≅ ((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₁} [Category.{v₁, u₁} J] {C : Type u₂} [Category.{v₂, u₂} C] (X : Cᵒᵖ) (j : Jᵒᵖ) :

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

source

@[simp]

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

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

source

@[simp]

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

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

source

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

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

source

@[simp]

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

(constComp J X F).hom.app x✝ = CategoryStruct.id ((((const J).obj X).comp F).obj x✝)

source

@[simp]

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

(constComp J X F).inv.app x✝ = CategoryStruct.id (((const J).obj (F.obj X)).obj x✝)

source

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

(const J).Faithful

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

source

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

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

source

@[simp]

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

((compConstIso J F).hom.app X).app X✝ = CategoryStruct.id (F.obj X)

source

@[simp]

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

((compConstIso J F).inv.app X).app X✝ = CategoryStruct.id (F.obj X)

source

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

(const D).comp ((whiskeringLeft J D C).obj F) ≅ 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.

source

@[simp]

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

((constCompWhiskeringLeftIso J F).inv.app X).app X✝ = CategoryStruct.id X

source

@[simp]

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

((constCompWhiskeringLeftIso J F).hom.app X).app X✝ = CategoryStruct.id X

Documentation

Mathlib.CategoryTheory.Functor.Const

The constant functor #