Facts about (co)limits of functors into concrete categories #
The forgetful fuctor on Type u is the identity; copy the instances on 𝟭 (Type u)
over to forget (Type u).
We currently have two instances for HasForget (Type u):
- A global
HasForgetinstance whereforget (Type u)reduces to𝟭 Type - A locally enabled
ConcreteCategorywhereforget (Type u)is only reducible-with-instances equal to𝟭 Type.
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]
[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]
{FC : C → C → Type u_1}
{CC : C → Type (max w v)}
[(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 (max w v)}
[(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 (max w v)}
[(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)
:
let 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 (max t w)}
[(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 (max t w)}
[(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 (max t w)}
[(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 (max t w)}
[(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