mathlib documentation

category_theory.limits.concrete_category

Facts about (co)limits of functors into concrete categories

source
@[simp]
theorem category_theory.limits.cone.w_apply {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] [category_theory.concrete_category C] {F : J ⥤ C} (s : category_theory.limits.cone F) {j j' : J} (f : j ⟶ j') (x : ↥(s.X)) :
⇑(F.map f) (⇑(s.π.app j) x) = ⇑(s.π.app j') x

Naturality of a cone over functors to a concrete category.

source
@[simp]
theorem category_theory.limits.cone.w_forget_apply {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] [category_theory.concrete_category C] (F : J ⥤ C) (s : category_theory.limits.cone (F ⋙ category_theory.forget C)) {j j' : J} (f : j ⟶ j') (x : s.X) :
⇑(F.map f) (s.π.app j x) = s.π.app j' x

source
@[simp]
theorem category_theory.limits.cocone.w_apply {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] [category_theory.concrete_category C] {F : J ⥤ C} (s : category_theory.limits.cocone F) {j j' : J} (f : j ⟶ j') (x : ↥(F.obj j)) :
⇑(s.ι.app j') (⇑(F.map f) x) = ⇑(s.ι.app j) x

Naturality of a cocone over functors into a concrete category.

source
@[simp]
theorem category_theory.limits.cocone.w_forget_apply {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] [category_theory.concrete_category C] (F : J ⥤ C) (s : category_theory.limits.cocone (F ⋙ category_theory.forget C)) {j j' : J} (f : j ⟶ j') (x : ↥(F.obj j)) :
s.ι.app j' (⇑(F.map f) x) = s.ι.app j x

source
@[simp]
theorem category_theory.limits.limit.lift_π_apply {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] [category_theory.concrete_category C] (F : J ⥤ C) [category_theory.limits.has_limit F] (s : category_theory.limits.cone F) (j : J) (x : ↥(s.X)) :
⇑(category_theory.limits.limit.π F j) (⇑(category_theory.limits.limit.lift F s) x) = ⇑(s.π.app j) x

source
@[simp]
theorem category_theory.limits.limit.w_apply {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] [category_theory.concrete_category C] (F : J ⥤ C) [category_theory.limits.has_limit F] {j j' : J} (f : j ⟶ j') (x : ↥(category_theory.limits.limit F)) :
⇑(F.map f) (⇑(category_theory.limits.limit.π F j) x) = ⇑(category_theory.limits.limit.π F j') x

source
@[simp]
theorem category_theory.limits.colimit.ι_desc_apply {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] [category_theory.concrete_category C] (F : J ⥤ C) [category_theory.limits.has_colimit F] (s : category_theory.limits.cocone F) (j : J) (x : ↥(F.obj j)) :
⇑(category_theory.limits.colimit.desc F s) (⇑(category_theory.limits.colimit.ι F j) x) = ⇑(s.ι.app j) x

source
@[simp]
theorem category_theory.limits.colimit.w_apply {J : Type v} [category_theory.small_category J] {C : Type u} [category_theory.category C] [category_theory.concrete_category C] (F : J ⥤ C) [category_theory.limits.has_colimit F] {j j' : J} (f : j ⟶ j') (x : ↥(F.obj j)) :
⇑(category_theory.limits.colimit.ι F j') (⇑(F.map f) x) = ⇑(category_theory.limits.colimit.ι F j) x