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_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).toPrefunctor.map f).app x = f

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).toPrefunctor.obj X).toPrefunctor.map x = CategoryTheory.CategoryStruct.id X

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).toPrefunctor.obj X).toPrefunctor.obj x = X

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.

Instances For

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) (j : Jᵒᵖ) :

(CategoryTheory.Functor.const.opObjOp X).inv.app j = CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.const J).toPrefunctor.obj X).op.toPrefunctor.obj j)

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) (j : Jᵒᵖ) :

(CategoryTheory.Functor.const.opObjOp X).hom.app j = CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.const Jᵒᵖ).toPrefunctor.obj (Opposite.op X)).toPrefunctor.obj j)

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

Instances For

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ᵒᵖ).toPrefunctor.obj X.unop ≅ ((CategoryTheory.Functor.const J).toPrefunctor.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.

Instances For

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ᵒᵖ).toPrefunctor.obj X.unop).toPrefunctor.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).toPrefunctor.obj X).leftOp.toPrefunctor.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₂) :

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

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