Filtered colimits in concrete categories #
In this file, we provide analogues to some of the API in the
CategoryTheory.Limits.Types.FilteredColimit namespace, for concrete categories for which the
forgetful functor preserves filtered colimits.
theorem
CategoryTheory.Limits.IsColimit.eq_iff
{J : Type u_1}
{C : Type u_2}
[Category.{v_1, u_1} J]
[Category.{v_2, u_2} C]
{FC : C → C → Type u_3}
{CC : C → Type u_4}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
[PreservesColimitsOfShape J (forget C)]
(F : Functor J C)
[IsFilteredOrEmpty J]
{t : Cocone F}
(ht : IsColimit t)
{i j : J}
{xi : ToType (F.obj i)}
{xj : ToType (F.obj j)}
:
(ConcreteCategory.hom (t.ι.app i)) xi = (ConcreteCategory.hom (t.ι.app j)) xj ↔ ∃ (k : J) (f : i ⟶ k) (g : j ⟶ k), (ConcreteCategory.hom (F.map f)) xi = (ConcreteCategory.hom (F.map g)) xj
theorem
CategoryTheory.Limits.IsColimit.eq_iff'
{J : Type u_1}
{C : Type u_2}
[Category.{v_1, u_1} J]
[Category.{v_2, u_2} C]
{FC : C → C → Type u_3}
{CC : C → Type u_4}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
[PreservesColimitsOfShape J (forget C)]
{F : Functor J C}
[IsFilteredOrEmpty J]
{t : Cocone F}
(ht : IsColimit t)
{i : J}
(x y : ToType (F.obj i))
:
(ConcreteCategory.hom (t.ι.app i)) x = (ConcreteCategory.hom (t.ι.app i)) y ↔ ∃ (j : J) (f : i ⟶ j), (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f)) y
theorem
CategoryTheory.Limits.colimit_eq_iff
{J : Type u_1}
{C : Type u_2}
[Category.{v_1, u_1} J]
[Category.{v_2, u_2} C]
{FC : C → C → Type u_3}
{CC : C → Type u_4}
[(X Y : C) → FunLike (FC X Y) (CC X) (CC Y)]
[ConcreteCategory C FC]
[PreservesColimitsOfShape J (forget C)]
(F : Functor J C)
[IsFilteredOrEmpty J]
[HasColimit F]
{i j : J}
{xi : ToType (F.obj i)}
{xj : ToType (F.obj j)}
:
(ConcreteCategory.hom (colimit.ι F i)) xi = (ConcreteCategory.hom (colimit.ι F j)) xj ↔ ∃ (k : J) (f : i ⟶ k) (g : j ⟶ k), (ConcreteCategory.hom (F.map f)) xi = (ConcreteCategory.hom (F.map g)) xj