Facts about (co)limits of functors into concrete categories #
The forgetful functor on Type u is the identity; copy the instances on 𝟭 (Type u)
over to forget (Type u).
Since instance synthesis only looks through reducible definitions, we need to help it out by copying over the instances that wouldn't be found otherwise.
theorem
CategoryTheory.Limits.Concrete.small_sections_of_hasLimit
{C : Type u}
[Category.{v, u} C]
{FC : outParam (C → C → Type u_1)}
{CC : outParam (C → Type v)}
[outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))]
[ConcreteCategory C FC]
[(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]
{FC : C → C → Type u_1}
{CC : C → Type r}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
{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 : ToType D.pt) (j : J) => (ConcreteCategory.hom (D.π.app j)) x
theorem
CategoryTheory.Limits.Concrete.isLimit_ext
{C : Type u}
[Category.{v, u} C]
{FC : C → C → Type u_1}
{CC : C → Type r}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
{J : Type w}
[Category.{t, w} J]
(F : Functor J C)
[PreservesLimit F (forget C)]
{D : Cone F}
(hD : IsLimit D)
(x y : ToType D.pt)
:
(∀ (j : J), (ConcreteCategory.hom (D.π.app j)) x = (ConcreteCategory.hom (D.π.app j)) y) → x = y
theorem
CategoryTheory.Limits.Concrete.limit_ext
{C : Type u}
[Category.{v, u} C]
{FC : C → C → Type u_1}
{CC : C → Type r}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
{J : Type w}
[Category.{t, w} J]
(F : Functor J C)
[PreservesLimit F (forget C)]
[HasLimit F]
(x y : ToType (limit F))
:
(∀ (j : J), (ConcreteCategory.hom (limit.π F j)) x = (ConcreteCategory.hom (limit.π F j)) y) → x = y
theorem
CategoryTheory.Limits.Concrete.surjective_π_app_zero_of_surjective_map
{C : Type u}
[Category.{v, u} C]
{FC : C → C → Type u_2}
{CC : C → Type v}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
[PreservesLimitsOfShape ℕᵒᵖ (forget C)]
{F : Functor ℕᵒᵖ C}
{c : Cone F}
(hc : IsLimit c)
(hF : ∀ (n : ℕ), Function.Surjective ⇑(ConcreteCategory.hom (F.map (homOfLE ⋯).op)))
:
Function.Surjective ⇑(ConcreteCategory.hom (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]
{FC : C → C → Type u_1}
{CC : C → Type t}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
{J : Type w}
[Category.{r, w} J]
(F : Functor J C)
[PreservesColimit F (forget C)]
{D : Cocone F}
(hD : IsColimit D)
:
have ff := fun (a : (j : J) × ToType (F.obj j)) => (ConcreteCategory.hom (D.ι.app a.fst)) a.snd;
Function.Surjective ff
theorem
CategoryTheory.Limits.Concrete.isColimit_exists_rep
{C : Type u}
[Category.{v, u} C]
{FC : C → C → Type u_1}
{CC : C → Type t}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
{J : Type w}
[Category.{r, w} J]
(F : Functor J C)
[PreservesColimit F (forget C)]
{D : Cocone F}
(hD : IsColimit D)
(x : ToType D.pt)
:
theorem
CategoryTheory.Limits.Concrete.colimit_exists_rep
{C : Type u}
[Category.{v, u} C]
{FC : C → C → Type u_1}
{CC : C → Type t}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
{J : Type w}
[Category.{r, w} J]
(F : Functor J C)
[PreservesColimit F (forget C)]
[HasColimit F]
(x : ToType (colimit F))
:
∃ (j : J) (y : ToType (F.obj j)), (ConcreteCategory.hom (colimit.ι F j)) y = x
theorem
CategoryTheory.Limits.Concrete.isColimit_rep_eq_of_exists
{C : Type u}
[Category.{v, u} C]
{FC : C → C → Type u_1}
{CC : C → Type t}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
{J : Type w}
[Category.{r, w} J]
(F : Functor J C)
{D : Cocone F}
{i j : J}
(x : ToType (F.obj i))
(y : ToType (F.obj j))
(h : ∃ (k : J) (f : i ⟶ k) (g : j ⟶ k), (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) y)
:
theorem
CategoryTheory.Limits.Concrete.colimit_rep_eq_of_exists
{C : Type u}
[Category.{v, u} C]
{FC : C → C → Type u_1}
{CC : C → Type t}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
{J : Type w}
[Category.{r, w} J]
(F : Functor J C)
[HasColimit F]
{i j : J}
(x : ToType (F.obj i))
(y : ToType (F.obj j))
(h : ∃ (k : J) (f : i ⟶ k) (g : j ⟶ k), (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) y)
:
theorem
CategoryTheory.Limits.Concrete.isColimit_exists_of_rep_eq
{C : Type u}
[Category.{v, u} C]
{FC : C → C → Type u_1}
{CC : C → Type s}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
{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 : ToType (F.obj i))
(y : ToType (F.obj j))
(h : (ConcreteCategory.hom (D.ι.app i)) x = (ConcreteCategory.hom (D.ι.app j)) y)
:
∃ (k : J) (f : i ⟶ k) (g : j ⟶ k), (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) y
theorem
CategoryTheory.Limits.Concrete.isColimit_rep_eq_iff_exists
{C : Type u}
[Category.{v, u} C]
{FC : C → C → Type u_1}
{CC : C → Type s}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
{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 : ToType (F.obj i))
(y : ToType (F.obj j))
:
(ConcreteCategory.hom (D.ι.app i)) x = (ConcreteCategory.hom (D.ι.app j)) y ↔ ∃ (k : J) (f : i ⟶ k) (g : j ⟶ k), (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) y
theorem
CategoryTheory.Limits.Concrete.colimit_exists_of_rep_eq
{C : Type u}
[Category.{v, u} C]
{FC : C → C → Type u_1}
{CC : C → Type s}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
{J : Type w}
[Category.{r, w} J]
(F : Functor J C)
[PreservesColimit F (forget C)]
[IsFiltered J]
[HasColimit F]
{i j : J}
(x : ToType (F.obj i))
(y : ToType (F.obj j))
(h : (ConcreteCategory.hom (colimit.ι F i)) x = (ConcreteCategory.hom (colimit.ι F j)) y)
:
∃ (k : J) (f : i ⟶ k) (g : j ⟶ k), (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) y
theorem
CategoryTheory.Limits.Concrete.colimit_rep_eq_iff_exists
{C : Type u}
[Category.{v, u} C]
{FC : C → C → Type u_1}
{CC : C → Type s}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
{J : Type w}
[Category.{r, w} J]
(F : Functor J C)
[PreservesColimit F (forget C)]
[IsFiltered J]
[HasColimit F]
{i j : J}
(x : ToType (F.obj i))
(y : ToType (F.obj j))
:
(ConcreteCategory.hom (colimit.ι F i)) x = (ConcreteCategory.hom (colimit.ι F j)) y ↔ ∃ (k : J) (f : i ⟶ k) (g : j ⟶ k), (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map g)) y