mathlib3 documentation

category_theory.category.Cat.limit

The category of small categories has all small limits. #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

An object in the limit consists of a family of objects, which are carried to one another by the functors in the diagram. A morphism between two such objects is a family of morphisms between the corresponding objects, which are carried to one another by the action on morphisms of the functors in the diagram.

Future work #

Can the indexing category live in a lower universe?

source
@[protected, instance]
def category_theory.Cat.has_limits.category_objects {J : Type v} [category_theory.small_category J] {F : J ⥤ category_theory.Cat} {j : J} :
category_theory.small_category ((F ⋙ category_theory.Cat.objects).obj j)
Equations
source
noncomputable def category_theory.Cat.has_limits.hom_diagram {J : Type v} [category_theory.small_category J] {F : J ⥤ category_theory.Cat} (X : category_theory.limits.limit (F ⋙ category_theory.Cat.objects)) (Y : category_theory.limits.limit (F ⋙ category_theory.Cat.objects)) :
J ⥤ Type v

Auxiliary definition: the diagram whose limit gives the morphism space between two objects of the limit category.

Equations
source
@[simp]
theorem category_theory.Cat.has_limits.hom_diagram_map {J : Type v} [category_theory.small_category J] {F : J ⥤ category_theory.Cat} (X : category_theory.limits.limit (F ⋙ category_theory.Cat.objects)) (Y : category_theory.limits.limit (F ⋙ category_theory.Cat.objects)) (j j' : J) (f : j ⟶ j') (g : category_theory.limits.limit.π (F ⋙ category_theory.Cat.objects) j X ⟶ category_theory.limits.limit.π (F ⋙ category_theory.Cat.objects) j Y) :
(category_theory.Cat.has_limits.hom_diagram X Y).map f g = category_theory.eq_to_hom _ ≫ (F.map f).map g ≫ category_theory.eq_to_hom _
source
@[simp]
theorem category_theory.Cat.has_limits.hom_diagram_obj {J : Type v} [category_theory.small_category J] {F : J ⥤ category_theory.Cat} (X : category_theory.limits.limit (F ⋙ category_theory.Cat.objects)) (Y : category_theory.limits.limit (F ⋙ category_theory.Cat.objects)) (j : J) :
(category_theory.Cat.has_limits.hom_diagram X Y).obj j = (category_theory.limits.limit.π (F ⋙ category_theory.Cat.objects) j X ⟶ category_theory.limits.limit.π (F ⋙ category_theory.Cat.objects) j Y)
source
@[simp]
theorem category_theory.Cat.has_limits.category_theory.limits.limit.category_theory.category_id {J : Type v} [category_theory.small_category J] (F : J ⥤ category_theory.Cat) (X : category_theory.limits.limit (F ⋙ category_theory.Cat.objects)) :
𝟙 X = category_theory.limits.types.limit.mk (category_theory.Cat.has_limits.hom_diagram X X) (λ (j : J), 𝟙 (category_theory.limits.limit.π (F ⋙ category_theory.Cat.objects) j X)) _
source
@[protected, instance]
noncomputable def category_theory.Cat.has_limits.category_theory.limits.limit.category_theory.category {J : Type v} [category_theory.small_category J] (F : J ⥤ category_theory.Cat) :
category_theory.category (category_theory.limits.limit (F ⋙ category_theory.Cat.objects))
Equations
source
@[simp]
theorem category_theory.Cat.has_limits.category_theory.limits.limit.category_theory.category_comp {J : Type v} [category_theory.small_category J] (F : J ⥤ category_theory.Cat) (X Y Z : category_theory.limits.limit (F ⋙ category_theory.Cat.objects)) (f : X ⟶ Y) (g : Y ⟶ Z) :
f ≫ g = category_theory.limits.types.limit.mk (category_theory.Cat.has_limits.hom_diagram X Z) (λ (j : J), category_theory.limits.limit.π (category_theory.Cat.has_limits.hom_diagram X Y) j f ≫ category_theory.limits.limit.π (category_theory.Cat.has_limits.hom_diagram Y Z) j g) _
source
@[simp]
theorem category_theory.Cat.has_limits.limit_cone_X_α {J : Type v} [category_theory.small_category J] (F : J ⥤ category_theory.Cat) :
↥(category_theory.Cat.has_limits.limit_cone_X F) = category_theory.limits.limit (F ⋙ category_theory.Cat.objects)
source
noncomputable def category_theory.Cat.has_limits.limit_cone_X {J : Type v} [category_theory.small_category J] (F : J ⥤ category_theory.Cat) :
category_theory.Cat

Auxiliary definition: the limit category.

Equations
source
@[simp]
theorem category_theory.Cat.has_limits.limit_cone_X_str {J : Type v} [category_theory.small_category J] (F : J ⥤ category_theory.Cat) :
(category_theory.Cat.has_limits.limit_cone_X F).str = category_theory.Cat.has_limits.category_theory.limits.limit.category_theory.category F
source
@[simp]
theorem category_theory.Cat.has_limits.limit_cone_X_2 {J : Type v} [category_theory.small_category J] (F : J ⥤ category_theory.Cat) :
(category_theory.Cat.has_limits.limit_cone F).X = category_theory.Cat.has_limits.limit_cone_X F
source
@[simp]
theorem category_theory.Cat.has_limits.limit_cone_π_app_map {J : Type v} [category_theory.small_category J] (F : J ⥤ category_theory.Cat) (j : J) (X Y : ↥(((category_theory.functor.const J).obj (category_theory.Cat.has_limits.limit_cone_X F)).obj j)) (ᾰ : category_theory.limits.limit (category_theory.Cat.has_limits.hom_diagram X Y)) :
((category_theory.Cat.has_limits.limit_cone F).π.app j).map ᾰ = category_theory.limits.limit.π (category_theory.Cat.has_limits.hom_diagram X Y) j ᾰ
source
@[simp]
theorem category_theory.Cat.has_limits.limit_cone_π_app_obj {J : Type v} [category_theory.small_category J] (F : J ⥤ category_theory.Cat) (j : J) (ᾰ : category_theory.limits.limit (F ⋙ category_theory.Cat.objects)) :
((category_theory.Cat.has_limits.limit_cone F).π.app j).obj ᾰ = category_theory.limits.limit.π (F ⋙ category_theory.Cat.objects) j ᾰ
source
noncomputable def category_theory.Cat.has_limits.limit_cone {J : Type v} [category_theory.small_category J] (F : J ⥤ category_theory.Cat) :
category_theory.limits.cone F

Auxiliary definition: the cone over the limit category.

Equations
source
@[simp]
theorem category_theory.Cat.has_limits.limit_cone_lift_map {J : Type v} [category_theory.small_category J] (F : J ⥤ category_theory.Cat) (s : category_theory.limits.cone F) (X Y : ↥(s.X)) (f : X ⟶ Y) :
(category_theory.Cat.has_limits.limit_cone_lift F s).map f = category_theory.limits.types.limit.mk (category_theory.Cat.has_limits.hom_diagram (category_theory.limits.limit.lift (F ⋙ category_theory.Cat.objects) {X := ↥(s.X), π := {app := λ (j : J), (s.π.app j).obj, naturality' := _}} X) (category_theory.limits.limit.lift (F ⋙ category_theory.Cat.objects) {X := ↥(s.X), π := {app := λ (j : J), (s.π.app j).obj, naturality' := _}} Y)) (λ (j : J), category_theory.eq_to_hom _ ≫ (s.π.app j).map f ≫ category_theory.eq_to_hom _) _
source
noncomputable def category_theory.Cat.has_limits.limit_cone_lift {J : Type v} [category_theory.small_category J] (F : J ⥤ category_theory.Cat) (s : category_theory.limits.cone F) :
s.X ⟶ category_theory.Cat.has_limits.limit_cone_X F

Auxiliary definition: the universal morphism to the proposed limit cone.

Equations
source
@[simp]
theorem category_theory.Cat.has_limits.limit_cone_lift_obj {J : Type v} [category_theory.small_category J] (F : J ⥤ category_theory.Cat) (s : category_theory.limits.cone F) (ᾰ : {X := ↥(s.X), π := {app := λ (j : J), (s.π.app j).obj, naturality' := _}}.X) :
(category_theory.Cat.has_limits.limit_cone_lift F s).obj ᾰ = category_theory.limits.limit.lift (F ⋙ category_theory.Cat.objects) {X := ↥(s.X), π := {app := λ (j : J), (s.π.app j).obj, naturality' := _}} ᾰ
source
@[simp]
theorem category_theory.Cat.has_limits.limit_π_hom_diagram_eq_to_hom {J : Type v} [category_theory.small_category J] {F : J ⥤ category_theory.Cat} (X Y : category_theory.limits.limit (F ⋙ category_theory.Cat.objects)) (j : J) (h : X = Y) :
category_theory.limits.limit.π (category_theory.Cat.has_limits.hom_diagram X Y) j (category_theory.eq_to_hom h) = category_theory.eq_to_hom _
source
noncomputable def category_theory.Cat.has_limits.limit_cone_is_limit {J : Type v} [category_theory.small_category J] (F : J ⥤ category_theory.Cat) :
category_theory.limits.is_limit (category_theory.Cat.has_limits.limit_cone F)

Auxiliary definition: the proposed cone is a limit cone.

Equations
source
@[protected, instance]
def category_theory.Cat.category_theory.limits.has_limits  :
category_theory.limits.has_limits category_theory.Cat

The category of small categories has all small limits.

source
@[protected, instance]
noncomputable def category_theory.Cat.objects.category_theory.limits.preserves_limits  :
category_theory.limits.preserves_limits category_theory.Cat.objects
Equations