Documentation

Mathlib.CategoryTheory.Limits.TypesFiltered

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} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) (x : (j : J) × F.obj j) (y : (j : J) × F.obj j) :

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
Instances For
    noncomputable def CategoryTheory.Limits.Types.FilteredColimit.isColimitOf {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) (t : CategoryTheory.Limits.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) :

    Recognizing filtered colimits of types.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      theorem CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [CategoryTheory.IsFilteredOrEmpty J] [CategoryTheory.Limits.HasColimit F] {t : CategoryTheory.Limits.Cocone F} (ht : CategoryTheory.Limits.IsColimit t) {i : J} {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