Filtered colimits in the category of types.

We give a characterisation of the equality in filtered colimits in Type as a lemma CategoryTheory.Limits.Types.FilteredColimit.colimit_eq_iff: colimit.ι F i xi = colimit.ι F j xj ↔ ∃ k (f : i ⟶ k) (g : j ⟶ k), F.map f xi = F.map g xj.

def CategoryTheory.Limits.Types.FilteredColimit.Rel {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) (x y : (j : J) × F.obj j) : Prop

An alternative relation on Σ j, F.obj j, which generates the same equivalence relation as we use to define the colimit in Type above, but that is more convenient when working with filtered colimits.

Elements in F.obj j and F.obj j' are equivalent if there is some k : J to the right where their images are equal.

Equations

• CategoryTheory.Limits.Types.FilteredColimit.Rel F x y = ∃ (k : J) (f : x.fst ⟶ k) (g : y.fst ⟶ k), F.map f x.snd = F.map g y.snd

theorem CategoryTheory.Limits.Types.FilteredColimit.rel_of_quot_rel {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) (x y : (j : J) × F.obj j) : Quot.Rel F x y → FilteredColimit.Rel F x y

theorem CategoryTheory.Limits.Types.FilteredColimit.eqvGen_quot_rel_of_rel {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) (x y : (j : J) × F.obj j) : FilteredColimit.Rel F x y → Relation.EqvGen (Quot.Rel F) x y

noncomputable def CategoryTheory.Limits.Types.FilteredColimit.isColimitOf {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) (t : Cocone F) (hsurj : ∀ (x : t.pt), ∃ (i : J) (xi : F.obj i), x = t.ι.app i xi) (hinj : ∀ (i j : J) (xi : F.obj i) (xj : F.obj j), t.ι.app i xi = t.ι.app j xj → ∃ (k : J) (f : i ⟶ k) (g : j ⟶ k), F.map f xi = F.map g xj) : IsColimit t

Recognizing filtered colimits of types.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CategoryTheory.Limits.Types.FilteredColimit.isColimitOf' {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [IsFilteredOrEmpty J] (t : Cocone F) (hsurj : ∀ (x : t.pt), ∃ (i : J) (xi : F.obj i), x = t.ι.app i xi) (hinj : ∀ (i : J) (x y : F.obj i), t.ι.app i x = t.ι.app i y → ∃ (k : J) (f : i ⟶ k), F.map f x = F.map f y) : IsColimit t

Recognizing filtered colimits of types. The injectivity condition here is slightly easier to check as compared to isColimitOf.

Equations

• CategoryTheory.Limits.Types.FilteredColimit.isColimitOf' F t hsurj hinj = CategoryTheory.Limits.Types.FilteredColimit.isColimitOf F t hsurj ⋯

theorem CategoryTheory.Limits.Types.FilteredColimit.rel_equiv {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [IsFilteredOrEmpty J] : _root_.Equivalence (FilteredColimit.Rel F)

theorem CategoryTheory.Limits.Types.FilteredColimit.rel_eq_eqvGen_quot_rel {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [IsFilteredOrEmpty J] : FilteredColimit.Rel F = Relation.EqvGen (Quot.Rel F)

theorem CategoryTheory.Limits.Types.FilteredColimit.colimit_eq_iff_aux {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [IsFilteredOrEmpty J] [HasColimit F] {i j : J} {xi : F.obj i} {xj : F.obj j} : (colimitCocone F).ι.app i xi = (colimitCocone F).ι.app j xj ↔ FilteredColimit.Rel F ⟨i, xi⟩ ⟨j, xj⟩

theorem CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [IsFilteredOrEmpty J] {t : Cocone F} (ht : IsColimit t) {i j : J} {xi : F.obj i} {xj : F.obj j} : t.ι.app i xi = t.ι.app j xj ↔ ∃ (k : J) (f : i ⟶ k) (g : j ⟶ k), F.map f xi = F.map g xj

theorem CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff' {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} [IsFilteredOrEmpty J] {t : Cocone F} (ht : IsColimit t) {i : J} (x y : F.obj i) : t.ι.app i x = t.ι.app i y ↔ ∃ (j : J) (f : i ⟶ j), F.map f x = F.map f y

theorem CategoryTheory.Limits.Types.FilteredColimit.colimit_eq_iff {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [IsFilteredOrEmpty J] [HasColimit F] {i j : J} {xi : F.obj i} {xj : F.obj j} : colimit.ι F i xi = colimit.ι F j xj ↔ ∃ (k : J) (f : i ⟶ k) (g : j ⟶ k), F.map f xi = F.map g xj