Documentation

Mathlib.CategoryTheory.Limits.ConcreteCategory.Basic

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.

source
๐Ÿ“ coverage
instance CategoryTheory.Types.instFullForgetTypeHom :
(forget (Type u)).Full
source
๐Ÿ“ coverage
instance CategoryTheory.Types.instPreservesLimitsOfSizeForgetTypeHom :
Limits.PreservesLimitsOfSize.{u_1, u_2, u, u, u + 1, u + 1} (forget (Type u))
source
๐Ÿ“ coverage
instance CategoryTheory.Types.instPreservesColimitsOfSizeForgetTypeHom :
Limits.PreservesColimitsOfSize.{u_1, u_2, u, u, u + 1, u + 1} (forget (Type u))
source
๐Ÿ“ coverage
instance CategoryTheory.Types.instReflectsLimitsOfSizeForgetTypeHom :
Limits.ReflectsLimitsOfSize.{u_1, u_2, u, u, u + 1, u + 1} (forget (Type u))
source
๐Ÿ“ coverage
instance CategoryTheory.Types.instReflectsColimitsOfSizeForgetTypeHom :
Limits.ReflectsColimitsOfSize.{u_1, u_2, u, u, u + 1, u + 1} (forget (Type u))
source
๐Ÿ“ coverage
instance CategoryTheory.Types.instIsEquivalenceForgetTypeHom :
(forget (Type u)).IsEquivalence
source
๐Ÿ“ coverage
instance CategoryTheory.Types.instIsCorepresentableForgetTypeHom :
(forget (Type u)).IsCorepresentable
source
๐Ÿ“ coverage
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.

source
๐Ÿ“ coverage
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
source
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
source
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
source
๐Ÿ“ coverage
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.

source
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
source
๐Ÿ“ coverage
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) :
โˆƒ (j : J) (y : ToType (F.obj j)), (ConcreteCategory.hom (D.ฮน.app j)) y = x
source
๐Ÿ“ coverage
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
source
๐Ÿ“ coverage
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) :
(ConcreteCategory.hom (D.ฮน.app i)) x = (ConcreteCategory.hom (D.ฮน.app j)) y
source
๐Ÿ“ coverage
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) :
(ConcreteCategory.hom (colimit.ฮน F i)) x = (ConcreteCategory.hom (colimit.ฮน F j)) y
source
๐Ÿ“ coverage
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
source
๐Ÿ“ coverage
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
source
๐Ÿ“ coverage
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
source
๐Ÿ“ coverage
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