def
category_theory.functor.const
(J : Type u₁)
[category_theory.category J]
{C : Type u₂}
[category_theory.category C] :
The functor sending X : C to the constant functor J ⥤ C sending everything to X.
@[simp]
theorem
category_theory.functor.const.obj_obj
{J : Type u₁}
[category_theory.category J]
{C : Type u₂}
[category_theory.category C]
(X : C)
(j : J) :
((category_theory.functor.const J).obj X).obj j = X
@[simp]
theorem
category_theory.functor.const.obj_map
{J : Type u₁}
[category_theory.category J]
{C : Type u₂}
[category_theory.category C]
(X : C)
{j j' : J}
(f : j ⟶ j') :
((category_theory.functor.const J).obj X).map f = 𝟙 X
@[simp]
theorem
category_theory.functor.const.map_app
{J : Type u₁}
[category_theory.category J]
{C : Type u₂}
[category_theory.category C]
{X Y : C}
(f : X ⟶ Y)
(j : J) :
((category_theory.functor.const J).map f).app j = f
def
category_theory.functor.const.op_obj_op
{J : Type u₁}
[category_theory.category J]
{C : Type u₂}
[category_theory.category C]
(X : C) :
(category_theory.functor.const Jᵒᵖ).obj (opposite.op X) ≅ ((category_theory.functor.const J).obj X).op
The contant 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
- category_theory.functor.const.op_obj_op X = {hom := {app := λ (j : Jᵒᵖ), 𝟙 (((category_theory.functor.const Jᵒᵖ).obj (opposite.op X)).obj j), naturality' := _}, inv := {app := λ (j : Jᵒᵖ), 𝟙 (((category_theory.functor.const J).obj X).op.obj j), naturality' := _}, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.functor.const.op_obj_op_hom_app
{J : Type u₁}
[category_theory.category J]
{C : Type u₂}
[category_theory.category C]
(X : C)
(j : Jᵒᵖ) :
(category_theory.functor.const.op_obj_op X).hom.app j = 𝟙 (((category_theory.functor.const Jᵒᵖ).obj (opposite.op X)).obj j)
@[simp]
theorem
category_theory.functor.const.op_obj_op_inv_app
{J : Type u₁}
[category_theory.category J]
{C : Type u₂}
[category_theory.category C]
(X : C)
(j : Jᵒᵖ) :
(category_theory.functor.const.op_obj_op X).inv.app j = 𝟙 (((category_theory.functor.const J).obj X).op.obj j)
def
category_theory.functor.const.op_obj_unop
{J : Type u₁}
[category_theory.category J]
{C : Type u₂}
[category_theory.category C]
(X : Cᵒᵖ) :
(category_theory.functor.const Jᵒᵖ).obj (opposite.unop X) ≅ ((category_theory.functor.const J).obj X).left_op
The contant 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
- category_theory.functor.const.op_obj_unop X = {hom := {app := λ (j : Jᵒᵖ), 𝟙 (((category_theory.functor.const Jᵒᵖ).obj (opposite.unop X)).obj j), naturality' := _}, inv := {app := λ (j : Jᵒᵖ), 𝟙 (((category_theory.functor.const J).obj X).left_op.obj j), naturality' := _}, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.functor.const.op_obj_unop_hom_app
{J : Type u₁}
[category_theory.category J]
{C : Type u₂}
[category_theory.category C]
(X : Cᵒᵖ)
(j : Jᵒᵖ) :
(category_theory.functor.const.op_obj_unop X).hom.app j = 𝟙 (((category_theory.functor.const Jᵒᵖ).obj (opposite.unop X)).obj j)
@[simp]
theorem
category_theory.functor.const.op_obj_unop_inv_app
{J : Type u₁}
[category_theory.category J]
{C : Type u₂}
[category_theory.category C]
(X : Cᵒᵖ)
(j : Jᵒᵖ) :
(category_theory.functor.const.op_obj_unop X).inv.app j = 𝟙 (((category_theory.functor.const J).obj X).left_op.obj j)
@[simp]
theorem
category_theory.functor.const.unop_functor_op_obj_map
{J : Type u₁}
[category_theory.category J]
{C : Type u₂}
[category_theory.category C]
(X : Cᵒᵖ)
{j₁ j₂ : J}
(f : j₁ ⟶ j₂) :
(opposite.unop ((category_theory.functor.const J).op.obj X)).map f = 𝟙 (opposite.unop X)
@[simp]
theorem
category_theory.functor.const_comp_inv_app
(J : Type u₁)
[category_theory.category J]
{C : Type u₂}
[category_theory.category C]
{D : Type u₃}
[category_theory.category D]
(X : C)
(F : C ⥤ D)
(_x : J) :
(category_theory.functor.const_comp J X F).inv.app _x = 𝟙 (((category_theory.functor.const J).obj (F.obj X)).obj _x)
def
category_theory.functor.const_comp
(J : Type u₁)
[category_theory.category J]
{C : Type u₂}
[category_theory.category C]
{D : Type u₃}
[category_theory.category D]
(X : C)
(F : C ⥤ D) :
(category_theory.functor.const J).obj X ⋙ F ≅ (category_theory.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
- category_theory.functor.const_comp J X F = {hom := {app := λ (_x : J), 𝟙 (((category_theory.functor.const J).obj X ⋙ F).obj _x), naturality' := _}, inv := {app := λ (_x : J), 𝟙 (((category_theory.functor.const J).obj (F.obj X)).obj _x), naturality' := _}, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.functor.const_comp_hom_app
(J : Type u₁)
[category_theory.category J]
{C : Type u₂}
[category_theory.category C]
{D : Type u₃}
[category_theory.category D]
(X : C)
(F : C ⥤ D)
(_x : J) :
(category_theory.functor.const_comp J X F).hom.app _x = 𝟙 (((category_theory.functor.const J).obj X ⋙ F).obj _x)