Mathlib.CategoryTheory.Functor.Const

CategoryTheory.Functor.const definition

: C ⥤ J ⥤ C

Full source

/-- The functor sending `X : C` to the constant functor `J ⥤ C` sending everything to `X`.
-/
@[simps]
def const : C ⥤ J ⥤ C where
  obj X :=
    { obj := fun _ => X
      map := fun _ => 𝟙 X }
  map f := { app := fun _ => f }

Constant functor

Informal description

The constant functor `const J : C ⥤ (J ⥤ C)` sends an object $X \in C$ to the functor $J \to C$ that maps every object in $J$ to $X$ and every morphism in $J$ to the identity morphism $\text{id}_X$ on $X$. For a morphism $f : X \to Y$ in $C$, the functor maps it to the natural transformation whose components are all $f$.

CategoryTheory.Functor.const.opObjOp definition

(X : C) : (const Jᵒᵖ).obj (op X) ≅ ((const J).obj X).op

Full source

/-- 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`.
-/
@[simps]
def opObjOp (X : C) : (const Jᵒᵖ).obj (op X) ≅ ((const J).obj X).op where
  hom := { app := fun _ => 𝟙 _ }
  inv := { app := fun _ => 𝟙 _ }

Natural isomorphism between constant functors on opposite objects

Informal description

For any object $X$ in a category $\mathcal{C}$, the constant functor $\mathrm{const}(J^{\mathrm{op}})$ applied to the opposite object $\mathrm{op}(X)$ is naturally isomorphic to the opposite of the constant functor $\mathrm{const}(J)$ applied to $X$. The natural isomorphism consists of identity morphisms in both directions.

CategoryTheory.Functor.const.opObjUnop definition

(X : Cᵒᵖ) : (const Jᵒᵖ).obj (unop X) ≅ ((const J).obj X).leftOp

Full source

/-- 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`.
-/
def opObjUnop (X : Cᵒᵖ) : (const Jᵒᵖ).obj (unop X) ≅ ((const J).obj X).leftOp where
  hom := { app := fun _ => 𝟙 _ }
  inv := { app := fun _ => 𝟙 _ }

-- Lean needs some help with universes here.

Natural isomorphism between constant functors on opposite categories

Informal description

For any object $X$ in the opposite category $C^{\mathrm{op}}$, the constant functor $\mathrm{const}(J^{\mathrm{op}})$ applied to $\mathrm{unop}(X)$ is naturally isomorphic to the left opposite of the constant functor $\mathrm{const}(J)$ applied to $X$. The natural isomorphism consists of identity morphisms in both directions.

CategoryTheory.Functor.const.opObjUnop_hom_app theorem

(X : Cᵒᵖ) (j : Jᵒᵖ) : (opObjUnop.{v₁, v₂} X).hom.app j = 𝟙 _

Full source

@[simp]
theorem opObjUnop_hom_app (X : Cᵒᵖ) (j : Jᵒᵖ) : (opObjUnop.{v₁, v₂} X).hom.app j = 𝟙 _ :=
  rfl

Identity Component of Natural Isomorphism for Opposite Constant Functors

Informal description

For any object $X$ in the opposite category $C^{\mathrm{op}}$ and any object $j$ in the opposite category $J^{\mathrm{op}}$, the component at $j$ of the natural isomorphism homomorphism from the constant functor $\mathrm{const}(J^{\mathrm{op}})$ applied to $\mathrm{unop}(X)$ to the left opposite of the constant functor $\mathrm{const}(J)$ applied to $X$ is the identity morphism on the underlying object.

CategoryTheory.Functor.const.opObjUnop_inv_app theorem

(X : Cᵒᵖ) (j : Jᵒᵖ) : (opObjUnop.{v₁, v₂} X).inv.app j = 𝟙 _

Full source

@[simp]
theorem opObjUnop_inv_app (X : Cᵒᵖ) (j : Jᵒᵖ) : (opObjUnop.{v₁, v₂} X).inv.app j = 𝟙 _ :=
  rfl

Identity Property of Inverse Natural Transformation Components for Opposite Constant Functors

Informal description

For any object $X$ in the opposite category $C^{\mathrm{op}}$ and any object $j$ in the opposite category $J^{\mathrm{op}}$, the component at $j$ of the inverse natural transformation of the isomorphism $\mathrm{const}(J^{\mathrm{op}}).obj (\mathrm{unop}\, X) \cong (\mathrm{const}\, J.obj\, X).\mathrm{leftOp}$ is the identity morphism on $\mathrm{unop}\, X$.

CategoryTheory.Functor.const.unop_functor_op_obj_map theorem

(X : Cᵒᵖ) {j₁ j₂ : J} (f : j₁ ⟶ j₂) : (unop ((Functor.op (const J)).obj X)).map f = 𝟙 (unop X)

Full source

@[simp]
theorem unop_functor_op_obj_map (X : Cᵒᵖ) {j₁ j₂ : J} (f : j₁ ⟶ j₂) :
    (unop ((Functor.op (const J)).obj X)).map f = 𝟙 (unop X) :=
  rfl

Identity Mapping Property of the Opposite Constant Functor

Informal description

For any object $X$ in the opposite category $C^{\mathrm{op}}$ and any morphism $f \colon j_1 \to j_2$ in $J$, the morphism mapped by the functor $\mathrm{unop} \circ (\mathrm{const}\, J)^{\mathrm{op}} \circ \mathrm{op}$ applied to $X$ is the identity morphism on $\mathrm{unop}\, X$, i.e., $$(\mathrm{unop} ((\mathrm{const}\, J)^{\mathrm{op}}.obj\, X)).map\, f = \mathrm{id}_{\mathrm{unop}\, X}.$$

CategoryTheory.Functor.constComp definition

(X : C) (F : C ⥤ D) : (const J).obj X ⋙ F ≅ (const J).obj (F.obj X)

Full source

/-- 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). -/
@[simps]
def constComp (X : C) (F : C ⥤ D) : (const J).obj X ⋙ F(const J).obj X ⋙ F ≅ (const J).obj (F.obj X) where
  hom := { app := fun _ => 𝟙 _ }
  inv := { app := fun _ => 𝟙 _ }

Natural isomorphism between composition with constant functor and constant functor of image

Informal description

For any object $X$ in category $\mathcal{C}$ and any functor $F \colon \mathcal{C} \to \mathcal{D}$, the composition of the constant functor $\text{const}_J$ applied to $X$ with $F$ is naturally isomorphic to the constant functor $\text{const}_J$ applied to $F(X)$. The natural isomorphism is given by identity morphisms in both directions, i.e., the components of the natural isomorphism and its inverse are all identity morphisms on $F(X)$.

CategoryTheory.Functor.instFaithfulConstOfNonempty instance

[Nonempty J] : Faithful (const J : C ⥤ J ⥤ C)

Full source

/-- If `J` is nonempty, then the constant functor over `J` is faithful. -/
instance [Nonempty J] : Faithful (const J : C ⥤ J ⥤ C) where
  map_injective e := NatTrans.congr_app e (Classical.arbitrary J)

Faithfulness of the Constant Functor for Nonempty Categories

Informal description

For any nonempty category $J$, the constant functor $\text{const}_J \colon \mathcal{C} \to (J \to \mathcal{C})$ is faithful. That is, for any two morphisms $f, g \colon X \to Y$ in $\mathcal{C}$, if $\text{const}_J(f) = \text{const}_J(g)$, then $f = g$.

CategoryTheory.Functor.compConstIso definition

(F : C ⥤ D) : F ⋙ Functor.const J ≅ Functor.const J ⋙ (whiskeringRight J C D).obj F

Full source

/-- The canonical isomorphism
`F ⋙ Functor.const J ≅ Functor.const F ⋙ (whiskeringRight J _ _).obj L`. -/
@[simps!]
def compConstIso (F : C ⥤ D) :
    F ⋙ Functor.const JF ⋙ Functor.const J ≅ Functor.const J ⋙ (whiskeringRight J C D).obj F :=
  NatIso.ofComponents
    (fun X => NatIso.ofComponents (fun _ => Iso.refl _) (by simp))
    (by aesop_cat)

Isomorphism between functor composition with constant functor and right whiskering

Informal description

The canonical isomorphism between the functors $F \circ \text{const}_J$ and $\text{const}_J \circ (\text{whiskeringRight}_J(F))$, where $\text{const}_J$ is the constant functor and $\text{whiskeringRight}_J$ is the right whiskering functor. This isomorphism is constructed componentwise using the identity isomorphism.

CategoryTheory.Functor.constCompWhiskeringLeftIso definition

(F : J ⥤ D) : const D ⋙ (whiskeringLeft J D C).obj F ≅ const J

Full source

/-- The canonical isomorphism
`const D ⋙ (whiskeringLeft J _ _).obj F ≅ const J` -/
@[simps!]
def constCompWhiskeringLeftIso (F : J ⥤ D) :
    constconst D ⋙ (whiskeringLeft J D C).obj Fconst D ⋙ (whiskeringLeft J D C).obj F ≅ const J :=
  NatIso.ofComponents fun X => NatIso.ofComponents fun Y => Iso.refl _

Isomorphism between constant functor compositions with left whiskering

Informal description

The canonical isomorphism between the functors `const D ⋙ (whiskeringLeft J D C).obj F` and `const J`, where `const D` is the constant functor sending objects to `D`, `whiskeringLeft` is the left whiskering functor, and `F` is a functor from `J` to `D`. This isomorphism is constructed componentwise using the identity isomorphism.