Filtered colimits of types #
In this file, given a functor F : J ⥤ Type w₀ from a filtered category J,
we compute the equivalence relation generated by
F.ColimitTypeRel on (j : J) × (F.obj j).
Given c : CoconeTypes F, we deduce a lemma
Functor.CoconeTypes.injective_descColimitType_iff_of_isFiltered which gives
a concrete condition under which the map
F.descColimitType c : F.ColimitType → c.pt is injective, which is an
important step when proving c.IsColimit.
theorem
CategoryTheory.Functor.eqvGen_colimitTypeRel_iff_of_isFiltered
{J : Type u}
[Category.{v, u} J]
[IsFiltered J]
(F : Functor J (Type w₀))
(x y : (j : J) × F.obj j)
:
theorem
CategoryTheory.Functor.ιColimitType_eq_iff_of_isFiltered
{J : Type u}
[Category.{v, u} J]
[IsFiltered J]
(F : Functor J (Type w₀))
{j j' : J}
(x : F.obj j)
(y : F.obj j')
:
F.ιColimitType j x = F.ιColimitType j' y ↔ ∃ (k : J) (f : j ⟶ k) (f' : j' ⟶ k), F.map f x = F.map f' y
theorem
CategoryTheory.Functor.ιColimitType_eq_iff_of_isFiltered'
{J : Type u}
[Category.{v, u} J]
[IsFiltered J]
(F : Functor J (Type w₀))
{j : J}
(x y : F.obj j)
:
More precise variant of the lemma ιColimitType_eq_iff_of_isFiltered
in the case both x and y and in the same type F.obj j.
theorem
CategoryTheory.Functor.CoconeTypes.descColimitType_injective_iff_of_isFiltered
{J : Type u}
[Category.{v, u} J]
[IsFiltered J]
{F : Functor J (Type w₀)}
(c : F.CoconeTypes)
:
theorem
CategoryTheory.Functor.CoconeTypes.descColimitType_injective_iff_of_isFiltered'
{J : Type u}
[Category.{v, u} J]
[IsFiltered J]
{F : Functor J (Type w₀)}
(c : F.CoconeTypes)
:
Variant of descColimitType_injective_iff_of_isFiltered where we
assume both elements x and x' are in the same type F.obj j.