Facts about (co)limits of functors into concrete categories #
theorem
CategoryTheory.Limits.Concrete.small_sections_of_hasLimit
{C : Type u}
[Category.{v, u} C]
[HasForget C]
[(forget C).IsCorepresentable]
{J : Type w}
[Category.{t, w} J]
(G : Functor J C)
[HasLimit G]
:
Small.{v, max v w} ↑(G.comp (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}
[Category.{v, u} C]
[HasForget C]
{J : Type w}
[Category.{t, w} J]
(F : Functor J C)
[PreservesLimit F (forget C)]
{D : Cone F}
(hD : IsLimit D)
:
Function.Injective fun (x : (forget C).obj D.pt) (j : J) => (D.π.app j) x
theorem
CategoryTheory.Limits.Concrete.isLimit_ext
{C : Type u}
[Category.{v, u} C]
[HasForget C]
{J : Type w}
[Category.{t, w} J]
(F : Functor J C)
[PreservesLimit F (forget C)]
{D : Cone F}
(hD : IsLimit D)
(x y : (forget C).obj D.pt)
:
theorem
CategoryTheory.Limits.Concrete.limit_ext
{C : Type u}
[Category.{v, u} C]
[HasForget C]
{J : Type w}
[Category.{t, w} J]
(F : Functor J C)
[PreservesLimit F (forget C)]
[HasLimit F]
(x y : (forget C).obj (limit F))
:
theorem
CategoryTheory.Limits.Concrete.surjective_π_app_zero_of_surjective_map
{C : Type u}
[Category.{v, u} C]
[HasForget C]
[PreservesLimitsOfShape ℕᵒᵖ (forget C)]
{F : Functor ℕᵒᵖ C}
{c : Cone F}
(hc : IsLimit c)
(hF : ∀ (n : ℕ), Function.Surjective ⇑(F.map (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}
[Category.{v, u} C]
[HasForget C]
{J : Type w}
[Category.{r, w} J]
(F : Functor J C)
[PreservesColimit F (forget C)]
{D : Cocone F}
(hD : IsColimit D)
:
let ff := fun (a : (j : J) × (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}
[Category.{v, u} C]
[HasForget C]
{J : Type w}
[Category.{r, w} J]
(F : Functor J C)
[PreservesColimit F (forget C)]
{D : Cocone F}
(hD : IsColimit D)
(x : (forget C).obj D.pt)
:
theorem
CategoryTheory.Limits.Concrete.colimit_exists_rep
{C : Type u}
[Category.{v, u} C]
[HasForget C]
{J : Type w}
[Category.{r, w} J]
(F : Functor J C)
[PreservesColimit F (forget C)]
[HasColimit F]
(x : (forget C).obj (colimit F))
:
theorem
CategoryTheory.Limits.Concrete.isColimit_rep_eq_of_exists
{C : Type u}
[Category.{v, u} C]
[HasForget C]
{J : Type w}
[Category.{r, w} J]
(F : Functor J C)
{D : Cocone F}
{i j : J}
(x : (forget C).obj (F.obj i))
(y : (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}
[Category.{v, u} C]
[HasForget C]
{J : Type w}
[Category.{r, w} J]
(F : Functor J C)
[HasColimit F]
{i j : J}
(x : (forget C).obj (F.obj i))
(y : (forget C).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}
[Category.{v, u} C]
[HasForget C]
{J : Type w}
[Category.{r, w} J]
(F : Functor J C)
[PreservesColimit F (forget C)]
[IsFiltered J]
{D : Cocone F}
{i j : J}
(hD : IsColimit D)
(x : (forget C).obj (F.obj i))
(y : (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}
[Category.{v, u} C]
[HasForget C]
{J : Type w}
[Category.{r, w} J]
(F : Functor J C)
[PreservesColimit F (forget C)]
[IsFiltered J]
{D : Cocone F}
{i j : J}
(hD : IsColimit D)
(x : (forget C).obj (F.obj i))
(y : (forget C).obj (F.obj j))
:
theorem
CategoryTheory.Limits.Concrete.colimit_exists_of_rep_eq
{C : Type u}
[Category.{v, u} C]
[HasForget C]
{J : Type w}
[Category.{r, w} J]
(F : Functor J C)
[PreservesColimit F (forget C)]
[IsFiltered J]
[HasColimit F]
{i j : J}
(x : (forget C).obj (F.obj i))
(y : (forget C).obj (F.obj j))
(h : (colimit.ι F i) x = (colimit.ι F j) y)
:
theorem
CategoryTheory.Limits.Concrete.colimit_rep_eq_iff_exists
{C : Type u}
[Category.{v, u} C]
[HasForget C]
{J : Type w}
[Category.{r, w} J]
(F : Functor J C)
[PreservesColimit F (forget C)]
[IsFiltered J]
[HasColimit F]
{i j : J}
(x : (forget C).obj (F.obj i))
(y : (forget C).obj (F.obj j))
: