Facts about (co)limits of functors into concrete categories #
theorem
CategoryTheory.Limits.Concrete.small_sections_of_hasLimit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
[(CategoryTheory.forget C).IsCorepresentable]
{J : Type w}
[CategoryTheory.Category.{t, w} J]
(G : CategoryTheory.Functor J C)
[CategoryTheory.Limits.HasLimit G]
:
Small.{v, max v w} ↑(G.comp (CategoryTheory.forget C)).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}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{J : Type w}
[CategoryTheory.Category.{t, w} 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).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.Category.{t, w} 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).obj D.pt)
(y : (CategoryTheory.forget C).obj D.pt)
:
theorem
CategoryTheory.Limits.Concrete.limit_ext
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{J : Type w}
[CategoryTheory.Category.{t, w} J]
(F : CategoryTheory.Functor J C)
[CategoryTheory.Limits.PreservesLimit F (CategoryTheory.forget C)]
[CategoryTheory.Limits.HasLimit F]
(x : (CategoryTheory.forget C).obj (CategoryTheory.Limits.limit F))
(y : (CategoryTheory.forget C).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.surjective_π_app_zero_of_surjective_map
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
[CategoryTheory.Limits.PreservesLimitsOfShape ℕᵒᵖ (CategoryTheory.forget C)]
{F : CategoryTheory.Functor ℕᵒᵖ C}
{c : CategoryTheory.Limits.Cone F}
(hc : CategoryTheory.Limits.IsLimit c)
(hF : ∀ (n : ℕ), Function.Surjective ⇑(F.map (CategoryTheory.homOfLE ⋯).op))
:
Function.Surjective ⇑(c.π.app (Opposite.op 0))
Given surjections ⋯ ⟶ Xₙ₊₁ ⟶ Xₙ ⟶ ⋯ ⟶ X₀ in a concrete category whose forgetful functor
preserves sequential limits, the projection map lim Xₙ ⟶ X₀ is surjective.
theorem
CategoryTheory.Limits.Concrete.from_union_surjective_of_isColimit
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{J : Type w}
[CategoryTheory.Category.{r, w} 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).obj (F.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 w}
[CategoryTheory.Category.{r, w} 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).obj D.pt)
:
∃ (j : J) (y : (CategoryTheory.forget C).obj (F.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 w}
[CategoryTheory.Category.{r, w} J]
(F : CategoryTheory.Functor J C)
[CategoryTheory.Limits.PreservesColimit F (CategoryTheory.forget C)]
[CategoryTheory.Limits.HasColimit F]
(x : (CategoryTheory.forget C).obj (CategoryTheory.Limits.colimit F))
:
∃ (j : J) (y : (CategoryTheory.forget C).obj (F.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 w}
[CategoryTheory.Category.{r, w} J]
(F : CategoryTheory.Functor J C)
{D : CategoryTheory.Limits.Cocone F}
{i : J}
{j : J}
(x : (CategoryTheory.forget C).obj (F.obj i))
(y : (CategoryTheory.forget C).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}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{J : Type w}
[CategoryTheory.Category.{r, w} J]
(F : CategoryTheory.Functor J C)
[CategoryTheory.Limits.HasColimit F]
{i : J}
{j : J}
(x : (CategoryTheory.forget C).obj (F.obj i))
(y : (CategoryTheory.forget C).obj (F.obj j))
(h : ∃ (k : J) (f : i ⟶ k) (g : j ⟶ k), (F.map f) x = (F.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 w}
[CategoryTheory.Category.{r, w} 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).obj (F.obj i))
(y : (CategoryTheory.forget C).obj (F.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 w}
[CategoryTheory.Category.{r, w} 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).obj (F.obj i))
(y : (CategoryTheory.forget C).obj (F.obj j))
:
theorem
CategoryTheory.Limits.Concrete.colimit_exists_of_rep_eq
{C : Type u}
[CategoryTheory.Category.{v, u} C]
[CategoryTheory.ConcreteCategory C]
{J : Type w}
[CategoryTheory.Category.{r, w} 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).obj (F.obj i))
(y : (CategoryTheory.forget C).obj (F.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 w}
[CategoryTheory.Category.{r, w} 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).obj (F.obj i))
(y : (CategoryTheory.forget C).obj (F.obj j))
:
(CategoryTheory.Limits.colimit.ι F i) x = (CategoryTheory.Limits.colimit.ι F j) y ↔ ∃ (k : J) (f : i ⟶ k) (g : j ⟶ k), (F.map f) x = (F.map g) y