# Facts about (co)limits of functors into concrete categories #

theorem CategoryTheory.Limits.Concrete.small_sections_of_hasLimit {C : Type u} [.Corepresentable] {J : Type w} (G : ) :
Small.{v, max v w} (G.comp ).sections

If a functor G : J ⥤ C to a concrete category has a limit and that forget C is corepresentable, then G ⋙ forget C).sections is small.

theorem CategoryTheory.Limits.Concrete.to_product_injective_of_isLimit {C : Type u} {J : Type w} (F : ) {D : } (hD : ) :
Function.Injective fun (x : .obj D.pt) (j : J) => (D.app j) x
theorem CategoryTheory.Limits.Concrete.isLimit_ext {C : Type u} {J : Type w} (F : ) {D : } (hD : ) (x : .obj D.pt) (y : .obj D.pt) :
(∀ (j : J), (D.app j) x = (D.app j) y)x = y
theorem CategoryTheory.Limits.Concrete.limit_ext {C : Type u} {J : Type w} (F : ) (x : .obj ) (y : .obj ) :
(∀ (j : J), = )x = y
theorem CategoryTheory.Limits.Concrete.from_union_surjective_of_isColimit {C : Type u} {J : Type w} (F : ) {D : } (hD : ) :
let ff := fun (a : (j : J) × .obj (F.obj j)) => (D.app a.fst) a.snd;
theorem CategoryTheory.Limits.Concrete.isColimit_exists_rep {C : Type u} {J : Type w} (F : ) {D : } (hD : ) (x : .obj D.pt) :
∃ (j : J) (y : .obj (F.obj j)), (D.app j) y = x
theorem CategoryTheory.Limits.Concrete.colimit_exists_rep {C : Type u} {J : Type w} (F : ) (x : ) :
∃ (j : J) (y : .obj (F.obj j)), = x
theorem CategoryTheory.Limits.Concrete.isColimit_rep_eq_of_exists {C : Type u} {J : Type w} (F : ) {D : } {i : J} {j : J} (x : .obj (F.obj i)) (y : .obj (F.obj j)) (h : ∃ (k : J) (f : i k) (g : j k), (F.map f) x = (F.map g) y) :
(D.app i) x = (D.app j) y
theorem CategoryTheory.Limits.Concrete.colimit_rep_eq_of_exists {C : Type u} {J : Type w} (F : ) {i : J} {j : J} (x : .obj (F.obj i)) (y : .obj (F.obj j)) (h : ∃ (k : J) (f : i k) (g : j k), (F.map f) x = (F.map g) y) :
=
theorem CategoryTheory.Limits.Concrete.isColimit_exists_of_rep_eq {C : Type u} {J : Type w} (F : ) {D : } {i : J} {j : J} (hD : ) (x : .obj (F.obj i)) (y : .obj (F.obj j)) (h : (D.app i) x = (D.app j) y) :
∃ (k : J) (f : i k) (g : j k), (F.map f) x = (F.map g) y
theorem CategoryTheory.Limits.Concrete.isColimit_rep_eq_iff_exists {C : Type u} {J : Type w} (F : ) {D : } {i : J} {j : J} (hD : ) (x : .obj (F.obj i)) (y : .obj (F.obj j)) :
(D.app i) x = (D.app j) y ∃ (k : J) (f : i k) (g : j k), (F.map f) x = (F.map g) y
theorem CategoryTheory.Limits.Concrete.colimit_exists_of_rep_eq {C : Type u} {J : Type w} (F : ) {i : J} {j : J} (x : .obj (F.obj i)) (y : .obj (F.obj j)) (h : = ) :
∃ (k : J) (f : i k) (g : j k), (F.map f) x = (F.map g) y
theorem CategoryTheory.Limits.Concrete.colimit_rep_eq_iff_exists {C : Type u} {J : Type w} (F : ) {i : J} {j : J} (x : .obj (F.obj i)) (y : .obj (F.obj j)) :
= ∃ (k : J) (f : i k) (g : j k), (F.map f) x = (F.map g) y