Colimits in the category of types

We show that the category of types has all colimits, by providing the usual concrete models.

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

The relation defining the quotient type which implements the colimit of a functor F : J ⥤ Type u. See CategoryTheory.Limits.Types.Quot.

Equations

• CategoryTheory.Limits.Types.Quot.Rel F p p' = ∃ (f : p.fst ⟶ p'.fst), p'.snd = F.map f p.snd

def CategoryTheory.Limits.Types.Quot {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) : Type (max v u)

A quotient type implementing the colimit of a functor F : J ⥤ Type u, as pairs ⟨j, x⟩ where x : F.obj j, modulo the equivalence relation generated by ⟨j, x⟩ ~ ⟨j', x'⟩ whenever there is a morphism f : j ⟶ j' so F.map f x = x'.

Equations

• CategoryTheory.Limits.Types.Quot F = Quot (CategoryTheory.Limits.Types.Quot.Rel F)

instance CategoryTheory.Limits.Types.instSmallQuot {J : Type v} [Category.{w, v} J] [Small.{u, v} J] (F : Functor J (Type u)) : Small.{u, max u v} (Quot F)

def CategoryTheory.Limits.Types.Quot.ι {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) (j : J) : F.obj j → Quot F

Inclusion into the quotient type implementing the colimit.

Equations

• CategoryTheory.Limits.Types.Quot.ι F j x = Quot.mk (CategoryTheory.Limits.Types.Quot.Rel F) ⟨j, x⟩

theorem CategoryTheory.Limits.Types.Quot.jointly_surjective {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} (x : Quot F) : ∃ (j : J) (y : F.obj j), x = ι F j y

def CategoryTheory.Limits.Types.Quot.desc {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} (c : Cocone F) : Quot F → c.pt

(implementation detail) Part of the universal property of the colimit cocone, but without assuming that Quot F lives in the correct universe.

Equations

• CategoryTheory.Limits.Types.Quot.desc c = Quot.lift (fun (x : (j : J) × F.obj j) => c.ι.app x.fst x.snd) ⋯

@[simp]

theorem CategoryTheory.Limits.Types.Quot.ι_desc {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} (c : Cocone F) (j : J) (x : F.obj j) : desc c (ι F j x) = c.ι.app j x

@[simp]

theorem CategoryTheory.Limits.Types.Quot.map_ι {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} {j j' : J} {f : j ⟶ j'} (x : F.obj j) : ι F j' (F.map f x) = ι F j x

def CategoryTheory.Limits.Types.quotToQuotUlift {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) : Quot F → Quot (F.comp uliftFunctor.{u', u})

The obvious map from Quot F to Quot (F ⋙ uliftFunctor.{u'}).

Equations

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

@[simp]

theorem CategoryTheory.Limits.Types.quotToQuotUlift_ι {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) (j : J) (x : F.obj j) : quotToQuotUlift F (Quot.ι F j x) = Quot.ι (F.comp uliftFunctor.{u_1, u}) j { down := x }

def CategoryTheory.Limits.Types.quotUliftToQuot {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) : Quot (F.comp uliftFunctor.{u', u}) → Quot F

The obvious map from Quot (F ⋙ uliftFunctor.{u'}) to Quot F.

Equations

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

@[simp]

theorem CategoryTheory.Limits.Types.quotUliftToQuot_ι {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) (j : J) (x : (F.comp uliftFunctor.{u', u}).obj j) : quotUliftToQuot F (Quot.ι (F.comp uliftFunctor.{u', u}) j x) = Quot.ι F j x.down

def CategoryTheory.Limits.Types.quotQuotUliftEquiv {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) : Quot F ≃ Quot (F.comp uliftFunctor.{u', u})

The equivalence between Quot F and Quot (F ⋙ uliftFunctor.{u'}).

Equations

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

theorem CategoryTheory.Limits.Types.Quot.desc_quotQuotUliftEquiv {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} (c : Cocone F) : desc (uliftFunctor.{u', u}.mapCocone c) ∘ ⇑(quotQuotUliftEquiv F) = ULift.up ∘ desc c

def CategoryTheory.Limits.Types.toCocone {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} {α : Type u} (f : Quot F → α) : Cocone F

(implementation detail) A function Quot F → α induces a cocone on F as long as the universes work out.

Equations

• CategoryTheory.Limits.Types.toCocone f = { pt := α, ι := { app := fun (j : J) => f ∘ CategoryTheory.Limits.Types.Quot.ι F j, naturality := ⋯ } }

@[simp]

theorem CategoryTheory.Limits.Types.toCocone_ι_app {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} {α : Type u} (f : Quot F → α) (j : J) (a✝ : F.obj j) : (toCocone f).ι.app j a✝ = (f ∘ Quot.ι F j) a✝

@[simp]

theorem CategoryTheory.Limits.Types.toCocone_pt {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} {α : Type u} (f : Quot F → α) : (toCocone f).pt = α

theorem CategoryTheory.Limits.Types.Quot.desc_toCocone_desc {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} (c : Cocone F) {α : Type u} (f : Quot F → α) (hc : IsColimit c) (x : Quot F) : hc.desc (toCocone f) (desc c x) = f x

theorem CategoryTheory.Limits.Types.isColimit_iff_bijective_desc {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} (c : Cocone F) : Nonempty (IsColimit c) ↔ Function.Bijective (Quot.desc c)

noncomputable def CategoryTheory.Limits.Types.colimitCocone {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [Small.{u, max u v} (Quot F)] : Cocone F

(internal implementation) the colimit cocone of a functor, implemented as a quotient of a sigma type

Equations

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

@[simp]

theorem CategoryTheory.Limits.Types.colimitCocone_ι_app {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [Small.{u, max u v} (Quot F)] (j : J) (x : F.obj j) : (colimitCocone F).ι.app j x = (equivShrink (Quot F)) (Quot.mk (Quot.Rel F) ⟨j, x⟩)

@[simp]

theorem CategoryTheory.Limits.Types.colimitCocone_pt {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [Small.{u, max u v} (Quot F)] : (colimitCocone F).pt = Shrink.{u, max u v} (Quot F)

@[simp]

theorem CategoryTheory.Limits.Types.Quot.desc_colimitCocone {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [Small.{u, max u v} (Quot F)] : desc (colimitCocone F) = ⇑(equivShrink (Quot F))

noncomputable def CategoryTheory.Limits.Types.colimitCoconeIsColimit {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [Small.{u, max u v} (Quot F)] : IsColimit (colimitCocone F)

(internal implementation) the fact that the proposed colimit cocone is the colimit

Equations

• CategoryTheory.Limits.Types.colimitCoconeIsColimit F = ⋯.some

theorem CategoryTheory.Limits.Types.hasColimit_iff_small_quot {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) : HasColimit F ↔ Small.{u, max u v} (Quot F)

theorem CategoryTheory.Limits.Types.small_quot_of_hasColimit {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [HasColimit F] : Small.{u, max u v} (Quot F)

instance CategoryTheory.Limits.Types.hasColimit {J : Type v} [Category.{w, v} J] [Small.{u, v} J] (F : Functor J (Type u)) : HasColimit F

instance CategoryTheory.Limits.Types.hasColimitsOfShape {J : Type v} [Category.{w, v} J] [Small.{u, v} J] : HasColimitsOfShape J (Type u)

@[instance 1300]

instance CategoryTheory.Limits.Types.hasColimitsOfSize [UnivLE.{v, u}] : HasColimitsOfSize.{w, v, u, u + 1} (Type u)

The category of types has all colimits.

Stacks Tag 002U

def CategoryTheory.Limits.Types.TypeMax.colimitCocone {J : Type v} [Category.{w, v} J] (F : Functor J (Type (max v u))) : Cocone F

(internal implementation) the colimit cocone of a functor, implemented as a quotient of a sigma type

Equations

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

@[simp]

theorem CategoryTheory.Limits.Types.TypeMax.colimitCocone_ι_app {J : Type v} [Category.{w, v} J] (F : Functor J (Type (max v u))) (j : J) (x : F.obj j) : (colimitCocone F).ι.app j x = Quot.mk (Quot.Rel F) ⟨j, x⟩

@[simp]

theorem CategoryTheory.Limits.Types.TypeMax.colimitCocone_pt {J : Type v} [Category.{w, v} J] (F : Functor J (Type (max v u))) : (colimitCocone F).pt = Quot F

def CategoryTheory.Limits.Types.TypeMax.colimitCoconeIsColimit {J : Type v} [Category.{w, v} J] (F : Functor J (Type (max v u))) : IsColimit (colimitCocone F)

(internal implementation) the fact that the proposed colimit cocone is the colimit

Equations

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

noncomputable def CategoryTheory.Limits.Types.colimitEquivQuot {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [HasColimit F] : colimit F ≃ Quot F

The equivalence between the abstract colimit of F in Type u and the "concrete" definition as a quotient.

Equations

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

@[simp]

theorem CategoryTheory.Limits.Types.colimitEquivQuot_symm_apply {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [HasColimit F] (j : J) (x : F.obj j) : (colimitEquivQuot F).symm (Quot.mk (Quot.Rel F) ⟨j, x⟩) = colimit.ι F j x

@[simp]

theorem CategoryTheory.Limits.Types.colimitEquivQuot_apply {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [HasColimit F] (j : J) (x : F.obj j) : (colimitEquivQuot F) (colimit.ι F j x) = Quot.mk (Quot.Rel F) ⟨j, x⟩

theorem CategoryTheory.Limits.Types.Colimit.w_apply {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} [HasColimit F] {j j' : J} {x : F.obj j} (f : j ⟶ j') : colimit.ι F j' (F.map f x) = colimit.ι F j x

theorem CategoryTheory.Limits.Types.Colimit.ι_desc_apply {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [HasColimit F] (s : Cocone F) (j : J) (x : F.obj j) : colimit.desc F s (colimit.ι F j x) = s.ι.app j x

theorem CategoryTheory.Limits.Types.Colimit.ι_map_apply {J : Type v} [Category.{w, v} J] {F G : Functor J (Type u)} [HasColimitsOfShape J (Type u)] (α : F ⟶ G) (j : J) (x : F.obj j) : colim.map α (colimit.ι F j x) = colimit.ι G j (α.app j x)

@[simp]

theorem CategoryTheory.Limits.Types.Colimit.w_apply' {J : Type v} [Category.{w, v} J] {F : Functor J (Type v)} {j j' : J} {x : F.obj j} (f : j ⟶ j') : colimit.ι F j' (F.map f x) = colimit.ι F j x

@[simp]

theorem CategoryTheory.Limits.Types.Colimit.ι_desc_apply' {J : Type v} [Category.{w, v} J] (F : Functor J (Type v)) (s : Cocone F) (j : J) (x : F.obj j) : colimit.desc F s (colimit.ι F j x) = s.ι.app j x

@[simp]

theorem CategoryTheory.Limits.Types.Colimit.ι_map_apply' {J : Type v} [Category.{w, v} J] {F G : Functor J (Type v)} (α : F ⟶ G) (j : J) (x : F.obj j) : colim.map α (colimit.ι F j x) = colimit.ι G j (α.app j x)

theorem CategoryTheory.Limits.Types.colimit_sound {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} [HasColimit F] {j j' : J} {x : F.obj j} {x' : F.obj j'} (f : j ⟶ j') (w : F.map f x = x') : colimit.ι F j x = colimit.ι F j' x'

theorem CategoryTheory.Limits.Types.colimit_sound' {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} [HasColimit F] {j j' : J} {x : F.obj j} {x' : F.obj j'} {j'' : J} (f : j ⟶ j'') (f' : j' ⟶ j'') (w : F.map f x = F.map f' x') : colimit.ι F j x = colimit.ι F j' x'

theorem CategoryTheory.Limits.Types.colimit_eq {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} [HasColimit F] {j j' : J} {x : F.obj j} {x' : F.obj j'} (w : colimit.ι F j x = colimit.ι F j' x') : Relation.EqvGen (Quot.Rel F) ⟨j, x⟩ ⟨j', x'⟩

theorem CategoryTheory.Limits.Types.jointly_surjective_of_isColimit {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} {t : Cocone F} (h : IsColimit t) (x : t.pt) : ∃ (j : J) (y : F.obj j), t.ι.app j y = x

theorem CategoryTheory.Limits.Types.jointly_surjective {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) {t : Cocone F} (h : IsColimit t) (x : t.pt) : ∃ (j : J) (y : F.obj j), t.ι.app j y = x

theorem CategoryTheory.Limits.Types.jointly_surjective' {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} [HasColimit F] (x : colimit F) : ∃ (j : J) (y : F.obj j), colimit.ι F j y = x

A variant of jointly_surjective for x : colimit F.

theorem CategoryTheory.Limits.Types.nonempty_of_nonempty_colimit {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} [HasColimit F] : Nonempty (colimit F) → Nonempty J

If a colimit is nonempty, also its index category is nonempty.