Facts about (co)limits of functors into concrete categories #
theorem
CategoryTheory.Limits.Concrete.to_product_injective_of_isLimit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{J : Type w}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J C)
[CategoryTheory.Limits.PreservesLimit F (CategoryTheory.forget C)]
{D : CategoryTheory.Limits.Cone F}
(hD : CategoryTheory.Limits.IsLimit D)
:
Function.Injective fun (x : (CategoryTheory.forget C).toPrefunctor.obj D.pt) (j : J) => (D.π.app j) x
theorem
CategoryTheory.Limits.Concrete.isLimit_ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{J : Type w}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J C)
[CategoryTheory.Limits.PreservesLimit F (CategoryTheory.forget C)]
{D : CategoryTheory.Limits.Cone F}
(hD : CategoryTheory.Limits.IsLimit D)
(x : (CategoryTheory.forget C).toPrefunctor.obj D.pt)
(y : (CategoryTheory.forget C).toPrefunctor.obj D.pt)
:
theorem
CategoryTheory.Limits.Concrete.limit_ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{J : Type w}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J C)
[CategoryTheory.Limits.PreservesLimit F (CategoryTheory.forget C)]
[CategoryTheory.Limits.HasLimit F]
(x : (CategoryTheory.forget C).toPrefunctor.obj (CategoryTheory.Limits.limit F))
(y : (CategoryTheory.forget C).toPrefunctor.obj (CategoryTheory.Limits.limit F))
:
(∀ (j : J), (CategoryTheory.Limits.limit.π F j) x = (CategoryTheory.Limits.limit.π F j) y) → x = y
theorem
CategoryTheory.Limits.Concrete.from_union_surjective_of_isColimit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J C)
[CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget C)]
{D : CategoryTheory.Limits.Cocone F}
(hD : CategoryTheory.Limits.IsColimit D)
:
let ff := fun (a : (j : J) × (CategoryTheory.forget C).toPrefunctor.obj (F.toPrefunctor.obj j)) =>
(D.ι.app a.fst) a.snd;
Function.Surjective ff
theorem
CategoryTheory.Limits.Concrete.isColimit_exists_rep
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J C)
[CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget C)]
{D : CategoryTheory.Limits.Cocone F}
(hD : CategoryTheory.Limits.IsColimit D)
(x : (CategoryTheory.forget C).toPrefunctor.obj D.pt)
:
∃ (j : J) (y : (CategoryTheory.forget C).toPrefunctor.obj (F.toPrefunctor.obj j)), (D.ι.app j) y = x
theorem
CategoryTheory.Limits.Concrete.colimit_exists_rep
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J C)
[CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget C)]
[CategoryTheory.Limits.HasColimit F]
(x : (CategoryTheory.forget C).toPrefunctor.obj (CategoryTheory.Limits.colimit F))
:
∃ (j : J) (y : (CategoryTheory.forget C).toPrefunctor.obj (F.toPrefunctor.obj j)),
(CategoryTheory.Limits.colimit.ι F j) y = x
theorem
CategoryTheory.Limits.Concrete.isColimit_rep_eq_of_exists
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J C)
[CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget C)]
{D : CategoryTheory.Limits.Cocone F}
{i : J}
{j : J}
(hD : CategoryTheory.Limits.IsColimit D)
(x : (CategoryTheory.forget C).toPrefunctor.obj (F.toPrefunctor.obj i))
(y : (CategoryTheory.forget C).toPrefunctor.obj (F.toPrefunctor.obj j))
(h : ∃ (k : J) (f : i ⟶ k) (g : j ⟶ k), (F.toPrefunctor.map f) x = (F.toPrefunctor.map g) y)
:
(D.ι.app i) x = (D.ι.app j) y
theorem
CategoryTheory.Limits.Concrete.colimit_rep_eq_of_exists
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J C)
[CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget C)]
[CategoryTheory.Limits.HasColimit F]
{i : J}
{j : J}
(x : (CategoryTheory.forget C).toPrefunctor.obj (F.toPrefunctor.obj i))
(y : (CategoryTheory.forget C).toPrefunctor.obj (F.toPrefunctor.obj j))
(h : ∃ (k : J) (f : i ⟶ k) (g : j ⟶ k), (F.toPrefunctor.map f) x = (F.toPrefunctor.map g) y)
:
(CategoryTheory.Limits.colimit.ι F i) x = (CategoryTheory.Limits.colimit.ι F j) y
theorem
CategoryTheory.Limits.Concrete.isColimit_exists_of_rep_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J C)
[CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget C)]
[CategoryTheory.IsFiltered J]
{D : CategoryTheory.Limits.Cocone F}
{i : J}
{j : J}
(hD : CategoryTheory.Limits.IsColimit D)
(x : (CategoryTheory.forget C).toPrefunctor.obj (F.toPrefunctor.obj i))
(y : (CategoryTheory.forget C).toPrefunctor.obj (F.toPrefunctor.obj j))
(h : (D.ι.app i) x = (D.ι.app j) y)
:
theorem
CategoryTheory.Limits.Concrete.isColimit_rep_eq_iff_exists
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J C)
[CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget C)]
[CategoryTheory.IsFiltered J]
{D : CategoryTheory.Limits.Cocone F}
{i : J}
{j : J}
(hD : CategoryTheory.Limits.IsColimit D)
(x : (CategoryTheory.forget C).toPrefunctor.obj (F.toPrefunctor.obj i))
(y : (CategoryTheory.forget C).toPrefunctor.obj (F.toPrefunctor.obj j))
:
theorem
CategoryTheory.Limits.Concrete.colimit_exists_of_rep_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J C)
[CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget C)]
[CategoryTheory.IsFiltered J]
[CategoryTheory.Limits.HasColimit F]
{i : J}
{j : J}
(x : (CategoryTheory.forget C).toPrefunctor.obj (F.toPrefunctor.obj i))
(y : (CategoryTheory.forget C).toPrefunctor.obj (F.toPrefunctor.obj j))
(h : (CategoryTheory.Limits.colimit.ι F i) x = (CategoryTheory.Limits.colimit.ι F j) y)
:
theorem
CategoryTheory.Limits.Concrete.colimit_rep_eq_iff_exists
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{J : Type v}
[CategoryTheory.SmallCategory J]
(F : CategoryTheory.Functor J C)
[CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget C)]
[CategoryTheory.IsFiltered J]
[CategoryTheory.Limits.HasColimit F]
{i : J}
{j : J}
(x : (CategoryTheory.forget C).toPrefunctor.obj (F.toPrefunctor.obj i))
(y : (CategoryTheory.forget C).toPrefunctor.obj (F.toPrefunctor.obj j))
:
(CategoryTheory.Limits.colimit.ι F i) x = (CategoryTheory.Limits.colimit.ι F j) y ↔ ∃ (k : J) (f : i ⟶ k) (g : j ⟶ k), (F.toPrefunctor.map f) x = (F.toPrefunctor.map g) y