Limit properties relating to the (co)yoneda embedding. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We calculate the colimit of Y ↦ (X ⟶ Y), which is just punit.
(This is used in characterising cofinal functors.)
We also show the (co)yoneda embeddings preserve limits and jointly reflect them.
def
category_theory.coyoneda.colimit_cocone
{C : Type v}
[category_theory.small_category C]
(X : Cᵒᵖ) :
The colimit cocone over coyoneda.obj X, with cocone point punit.
Equations
- category_theory.coyoneda.colimit_cocone X = {X := punit, ι := {app := λ (X_1 : C), id (λ (ᾰ : (category_theory.coyoneda.obj X).obj X_1), id (λ (X : Cᵒᵖ) (X_1 : C) (ᾰ : opposite.unop X ⟶ X_1), punit.star) X X_1 ᾰ), naturality' := _}}
@[simp]
theorem
category_theory.coyoneda.colimit_cocone_X
{C : Type v}
[category_theory.small_category C]
(X : Cᵒᵖ) :
@[simp]
theorem
category_theory.coyoneda.colimit_cocone_ι_app
{C : Type v}
[category_theory.small_category C]
(X : Cᵒᵖ)
(X_1 : C)
(ᾰ : (category_theory.coyoneda.obj X).obj X_1) :
(category_theory.coyoneda.colimit_cocone X).ι.app X_1 ᾰ = id (λ (ᾰ : (category_theory.coyoneda.obj X).obj X_1), id (λ (X : Cᵒᵖ) (X_1 : C) (ᾰ : opposite.unop X ⟶ X_1), punit.star) X X_1 ᾰ) ᾰ
def
category_theory.coyoneda.colimit_cocone_is_colimit
{C : Type v}
[category_theory.small_category C]
(X : Cᵒᵖ) :
The proposed colimit cocone over coyoneda.obj X is a colimit cocone.
Equations
- category_theory.coyoneda.colimit_cocone_is_colimit X = {desc := λ (s : category_theory.limits.cocone (category_theory.coyoneda.obj X)) (x : (category_theory.coyoneda.colimit_cocone X).X), s.ι.app (opposite.unop X) (𝟙 (opposite.unop X)), fac' := _, uniq' := _}
@[simp]
theorem
category_theory.coyoneda.colimit_cocone_is_colimit_desc
{C : Type v}
[category_theory.small_category C]
(X : Cᵒᵖ)
(s : category_theory.limits.cocone (category_theory.coyoneda.obj X))
(x : (category_theory.coyoneda.colimit_cocone X).X) :
(category_theory.coyoneda.colimit_cocone_is_colimit X).desc s x = s.ι.app (opposite.unop X) (𝟙 (opposite.unop X))
@[protected, instance]
noncomputable
def
category_theory.coyoneda.colimit_coyoneda_iso
{C : Type v}
[category_theory.small_category C]
(X : Cᵒᵖ) :
The colimit of coyoneda.obj X is isomorphic to punit.
@[protected, instance]
The yoneda embedding yoneda.obj X : Cᵒᵖ ⥤ Type v for X : C preserves limits.
Equations
- category_theory.yoneda_preserves_limits X = {preserves_limits_of_shape := λ (J : Type v) (𝒥 : category_theory.category J), {preserves_limit := λ (K : J ⥤ Cᵒᵖ), {preserves := λ (c : category_theory.limits.cone K) (t : category_theory.limits.is_limit c), {lift := λ (s : category_theory.limits.cone (K ⋙ category_theory.yoneda.obj X)) (x : s.X), (t.lift {X := opposite.op X, π := {app := λ (j : J), quiver.hom.op (s.π.app j x), naturality' := _}}).unop, fac' := _, uniq' := _}}}}
@[protected, instance]
The coyoneda embedding coyoneda.obj X : C ⥤ Type v for X : Cᵒᵖ preserves limits.
Equations
- category_theory.coyoneda_preserves_limits X = {preserves_limits_of_shape := λ (J : Type v) (𝒥 : category_theory.category J), {preserves_limit := λ (K : J ⥤ C), {preserves := λ (c : category_theory.limits.cone K) (t : category_theory.limits.is_limit c), {lift := λ (s : category_theory.limits.cone (K ⋙ category_theory.coyoneda.obj X)) (x : s.X), t.lift {X := opposite.unop X, π := {app := λ (j : J), s.π.app j x, naturality' := _}}, fac' := _, uniq' := _}}}}
def
category_theory.yoneda_jointly_reflects_limits
{C : Type u}
[category_theory.category C]
(J : Type w)
[category_theory.small_category J]
(K : J ⥤ Cᵒᵖ)
(c : category_theory.limits.cone K)
(t : Π (X : C), category_theory.limits.is_limit ((category_theory.yoneda.obj X).map_cone c)) :
The yoneda embeddings jointly reflect limits.
Equations
- category_theory.yoneda_jointly_reflects_limits J K c t = let s' : Π (s : category_theory.limits.cone K), category_theory.limits.cone (K ⋙ category_theory.yoneda.obj (opposite.unop s.X)) := λ (s : category_theory.limits.cone K), {X := punit, π := {app := λ (j : J) (_x : ((category_theory.functor.const J).obj punit).obj j), (s.π.app j).unop, naturality' := _}} in {lift := λ (s : category_theory.limits.cone K), quiver.hom.op ((t (opposite.unop s.X)).lift (s' s) punit.star), fac' := _, uniq' := _}
def
category_theory.coyoneda_jointly_reflects_limits
{C : Type u}
[category_theory.category C]
(J : Type w)
[category_theory.small_category J]
(K : J ⥤ C)
(c : category_theory.limits.cone K)
(t : Π (X : Cᵒᵖ), category_theory.limits.is_limit ((category_theory.coyoneda.obj X).map_cone c)) :
The coyoneda embeddings jointly reflect limits.
Equations
- category_theory.coyoneda_jointly_reflects_limits J K c t = let s' : Π (s : category_theory.limits.cone K), category_theory.limits.cone (K ⋙ category_theory.coyoneda.obj (opposite.op s.X)) := λ (s : category_theory.limits.cone K), {X := punit, π := {app := λ (j : J) (_x : ((category_theory.functor.const J).obj punit).obj j), s.π.app j, naturality' := _}} in {lift := λ (s : category_theory.limits.cone K), (t (opposite.op s.X)).lift (s' s) punit.star, fac' := _, uniq' := _}
@[protected, instance]
@[protected, instance]
@[protected, instance]
def
category_theory.yoneda_functor_reflects_limits
{D : Type u}
[category_theory.small_category D] :
@[protected, instance]