Limits in the category of types.

We show that the category of types has all (co)limits, by providing the usual concrete models.

We also give a characterisation of filtered colimits in Type, via colimit.ι F i xi = colimit.ι F j xj ↔ ∃ k (f : i ⟶ k) (g : j ⟶ k), F.map f xi = F.map g xj.

Finally, we prove the category of types has categorical images, and that these agree with the range of a function.

We now provide two distinct implementations in the category of types.

The first, in the CategoryTheory.Limits.Types.UnivLE namespace, assumes UnivLE.{v, u} and constructs v-small limits in Type u.

The second, in the CategoryTheory.Limits.Types.TypeMax namespace constructs limits for functors F : J ⥤ TypeMax.{v, u}, for J : Type v. This construction is slightly nicer, as the limit is definitionally just F.sections, rather than Shrink F.sections, which makes an arbitrary choice of u-small representative.

Hopefully we might be able to entirely remove the TypeMax constructions, but for now they are useful glue for the later parts of the library.

@[simp]

theorem CategoryTheory.Limits.Types.UnivLE.limitCone_pt {J : Type v} [CategoryTheory.SmallCategory J] [UnivLE.{v, u} ] (F : CategoryTheory.Functor J (Type u)) : (CategoryTheory.Limits.Types.UnivLE.limitCone F).pt = Shrink ↑(CategoryTheory.Functor.sections F)

@[simp]

theorem CategoryTheory.Limits.Types.UnivLE.limitCone_π_app {J : Type v} [CategoryTheory.SmallCategory J] [UnivLE.{v, u} ] (F : CategoryTheory.Functor J (Type u)) (j : J) (u : ((CategoryTheory.Functor.const J).obj (Shrink ↑(CategoryTheory.Functor.sections F))).obj j) : J.app inst✝ (Type u) CategoryTheory.types ((CategoryTheory.Functor.const J).obj (Shrink ↑(CategoryTheory.Functor.sections F))) F (CategoryTheory.Limits.Types.UnivLE.limitCone F).π j u = ↑(↑(equivShrink ↑(CategoryTheory.Functor.sections F)).symm u) j

noncomputable def CategoryTheory.Limits.Types.UnivLE.limitCone {J : Type v} [CategoryTheory.SmallCategory J] [UnivLE.{v, u} ] (F : CategoryTheory.Functor J (Type u)) : CategoryTheory.Limits.Cone F

(internal implementation) the limit cone of a functor, implemented as flat sections of a pi type

theorem CategoryTheory.Limits.Types.UnivLE.limitCone_pt_ext {J : Type v} [CategoryTheory.SmallCategory J] [UnivLE.{v, u} ] (F : CategoryTheory.Functor J (Type u)) {x : (CategoryTheory.Limits.Types.UnivLE.limitCone F).pt} {y : (CategoryTheory.Limits.Types.UnivLE.limitCone F).pt} (w : ↑(equivShrink ↑(CategoryTheory.Functor.sections F)).symm x = ↑(equivShrink ↑(CategoryTheory.Functor.sections F)).symm y) : x = y

@[simp]

theorem CategoryTheory.Limits.Types.UnivLE.limitConeIsLimit_lift {J : Type v} [CategoryTheory.SmallCategory J] [UnivLE.{v, u} ] (F : CategoryTheory.Functor J (Type u)) (s : CategoryTheory.Limits.Cone F) (v : s.pt) : CategoryTheory.Limits.IsLimit.lift J inst✝ (Type u) CategoryTheory.types F (CategoryTheory.Limits.Types.UnivLE.limitCone F) (CategoryTheory.Limits.Types.UnivLE.limitConeIsLimit F) s v = ↑(equivShrink ↑(CategoryTheory.Functor.sections F)) { val := fun j => J.app inst✝ (Type u) CategoryTheory.types ((CategoryTheory.Functor.const J).obj s.pt) F s.π j v, property := (_ : ∀ {j j' : J} (f : j ⟶ j'), CategoryTheory.CategoryStruct.comp (Type u) CategoryTheory.Category.toCategoryStruct (((CategoryTheory.Functor.const J).obj s.pt).obj j) (F.obj j) (F.obj j') (s.π.app j) (F.map f) v = J.app inst✝ (Type u) CategoryTheory.types ((CategoryTheory.Functor.const J).obj s.pt) F s.π j' v) }

noncomputable def CategoryTheory.Limits.Types.UnivLE.limitConeIsLimit {J : Type v} [CategoryTheory.SmallCategory J] [UnivLE.{v, u} ] (F : CategoryTheory.Functor J (Type u)) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Types.UnivLE.limitCone F)

(internal implementation) the fact that the proposed limit cone is the limit

@[simp]

theorem CategoryTheory.Limits.Types.limitCone_pt {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TypeMax) : (CategoryTheory.Limits.Types.limitCone F).pt = ↑(CategoryTheory.Functor.sections F)

@[simp]

theorem CategoryTheory.Limits.Types.limitCone_π_app {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TypeMax) (j : J) (u : ((CategoryTheory.Functor.const J).obj ↑(CategoryTheory.Functor.sections F)).obj j) : J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj ↑(CategoryTheory.Functor.sections F)) F (CategoryTheory.Limits.Types.limitCone F).π j u = ↑u j

noncomputable def CategoryTheory.Limits.Types.limitCone {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TypeMax) : CategoryTheory.Limits.Cone F

(internal implementation) the limit cone of a functor, implemented as flat sections of a pi type

@[simp]

theorem CategoryTheory.Limits.Types.limitConeIsLimit_lift_coe {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TypeMax) (s : CategoryTheory.Limits.Cone F) (v : s.pt) (j : J) : ↑(CategoryTheory.Limits.IsLimit.lift J inst✝ TypeMax CategoryTheory.types F (CategoryTheory.Limits.Types.limitCone F) (CategoryTheory.Limits.Types.limitConeIsLimit F) s v) j = J.app inst✝ TypeMax CategoryTheory.types ((CategoryTheory.Functor.const J).obj s.pt) F s.π j v

noncomputable def CategoryTheory.Limits.Types.limitConeIsLimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TypeMax) : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Types.limitCone F)

(internal implementation) the fact that the proposed limit cone is the limit

The results in this section have a UnivLE.{v, u} hypothesis, but as they only use the constructions from the CategoryTheory.Limits.Types.UnivLE namespace in their definitions (rather than their statements), we leave them in the main CategoryTheory.Limits.Types namespace.

noncomputable def CategoryTheory.Limits.Types.isLimitEquivSections {J : Type v} [CategoryTheory.SmallCategory J] [UnivLE.{v, u} ] {F : CategoryTheory.Functor J (Type u)} {c : CategoryTheory.Limits.Cone F} (t : CategoryTheory.Limits.IsLimit c) : c.pt ≃ ↑(CategoryTheory.Functor.sections F)

The equivalence between a limiting cone of F in Type u and the "concrete" definition as the sections of F.

@[simp]

theorem CategoryTheory.Limits.Types.isLimitEquivSections_apply {J : Type v} [CategoryTheory.SmallCategory J] [UnivLE.{v, u} ] {F : CategoryTheory.Functor J (Type u)} {c : CategoryTheory.Limits.Cone F} (t : CategoryTheory.Limits.IsLimit c) (j : J) (x : c.pt) : ↑(↑(CategoryTheory.Limits.Types.isLimitEquivSections t) x) j = J.app inst✝ (Type u) CategoryTheory.types ((CategoryTheory.Functor.const J).obj c.pt) F c.π j x

@[simp]

theorem CategoryTheory.Limits.Types.isLimitEquivSections_symm_apply {J : Type v} [CategoryTheory.SmallCategory J] [UnivLE.{v, u} ] {F : CategoryTheory.Functor J (Type u)} {c : CategoryTheory.Limits.Cone F} (t : CategoryTheory.Limits.IsLimit c) (x : ↑(CategoryTheory.Functor.sections F)) (j : J) : J.app inst✝ (Type u) CategoryTheory.types ((CategoryTheory.Functor.const J).obj c.pt) F c.π j (↑(CategoryTheory.Limits.Types.isLimitEquivSections t).symm x) = ↑x j

instance CategoryTheory.Limits.Types.hasLimitsOfSize [UnivLE.{v, u} ] : CategoryTheory.Limits.HasLimitsOfSize.{v, v, u, u + 1} (Type u)

The category of types has all limits.

More specifically, when UnivLE.{v, u}, the category Type u has all v-small limits.

See https://stacks.math.columbia.edu/tag/002U.

instance CategoryTheory.Limits.Types.hasLimit {J : Type v} [CategoryTheory.SmallCategory J] [UnivLE.{v, u} ] (F : CategoryTheory.Functor J (Type u)) : CategoryTheory.Limits.HasLimit F

noncomputable def CategoryTheory.Limits.Types.limitEquivSections {J : Type v} [CategoryTheory.SmallCategory J] [UnivLE.{v, u} ] (F : CategoryTheory.Functor J (Type u)) : CategoryTheory.Limits.limit F ≃ ↑(CategoryTheory.Functor.sections F)

The equivalence between the abstract limit of F in TypeMax.{v, u} and the "concrete" definition as the sections of F.

@[simp]

theorem CategoryTheory.Limits.Types.limitEquivSections_apply {J : Type v} [CategoryTheory.SmallCategory J] [UnivLE.{v, u} ] (F : CategoryTheory.Functor J (Type u)) (x : CategoryTheory.Limits.limit F) (j : J) : ↑(↑(CategoryTheory.Limits.Types.limitEquivSections F) x) j = CategoryTheory.Limits.limit.π J inst✝ (Type u) CategoryTheory.types F (_ : CategoryTheory.Limits.HasLimit F) j x

@[simp]

theorem CategoryTheory.Limits.Types.limitEquivSections_symm_apply {J : Type v} [CategoryTheory.SmallCategory J] [UnivLE.{v, u} ] (F : CategoryTheory.Functor J (Type u)) (x : ↑(CategoryTheory.Functor.sections F)) (j : J) : CategoryTheory.Limits.limit.π J inst✝ (Type u) CategoryTheory.types F (_ : CategoryTheory.Limits.HasLimit F) j (↑(CategoryTheory.Limits.Types.limitEquivSections F).symm x) = ↑x j

noncomputable def CategoryTheory.Limits.Types.Limit.mk {J : Type v} [CategoryTheory.SmallCategory J] [UnivLE.{v, u} ] (F : CategoryTheory.Functor J (Type u)) (x : (j : J) → F.obj j) (h : ∀ (j j' : J) (f : j ⟶ j'), J.map CategoryTheory.CategoryStruct.toQuiver (Type u) CategoryTheory.CategoryStruct.toQuiver F.toPrefunctor j j' f (x j) = x j') : CategoryTheory.Limits.limit F

Construct a term of limit F : Type u from a family of terms x : Π j, F.obj j which are "coherent": ∀ (j j') (f : j ⟶ j'), F.map f (x j) = x j'.

@[simp]

theorem CategoryTheory.Limits.Types.Limit.π_mk {J : Type v} [CategoryTheory.SmallCategory J] [UnivLE.{v, u} ] (F : CategoryTheory.Functor J (Type u)) (x : (j : J) → F.obj j) (h : ∀ (j j' : J) (f : j ⟶ j'), J.map CategoryTheory.CategoryStruct.toQuiver (Type u) CategoryTheory.CategoryStruct.toQuiver F.toPrefunctor j j' f (x j) = x j') (j : J) : CategoryTheory.Limits.limit.π J inst✝ (Type u) CategoryTheory.types F (_ : CategoryTheory.Limits.HasLimit F) j (CategoryTheory.Limits.Types.Limit.mk F x h) = x j

theorem CategoryTheory.Limits.Types.limit_ext {J : Type v} [CategoryTheory.SmallCategory J] [UnivLE.{v, u} ] (F : CategoryTheory.Functor J (Type u)) (x : CategoryTheory.Limits.limit F) (y : CategoryTheory.Limits.limit F) (w : ∀ (j : J), CategoryTheory.Limits.limit.π J inst✝ (Type u) CategoryTheory.types F (_ : CategoryTheory.Limits.HasLimit F) j x = CategoryTheory.Limits.limit.π J inst✝ (Type u) CategoryTheory.types F (_ : CategoryTheory.Limits.HasLimit F) j y) : x = y

theorem CategoryTheory.Limits.Types.limit_ext' {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J (Type v)) (x : CategoryTheory.Limits.limit F) (y : CategoryTheory.Limits.limit F) (w : ∀ (j : J), CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types F (_ : CategoryTheory.Limits.HasLimit F) j x = CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types F (_ : CategoryTheory.Limits.HasLimit F) j y) : x = y

theorem CategoryTheory.Limits.Types.limit_ext_iff {J : Type v} [CategoryTheory.SmallCategory J] [UnivLE.{v, u} ] (F : CategoryTheory.Functor J (Type u)) (x : CategoryTheory.Limits.limit F) (y : CategoryTheory.Limits.limit F) : x = y ↔ ∀ (j : J), CategoryTheory.Limits.limit.π J inst✝ (Type u) CategoryTheory.types F (_ : CategoryTheory.Limits.HasLimit F) j x = CategoryTheory.Limits.limit.π J inst✝ (Type u) CategoryTheory.types F (_ : CategoryTheory.Limits.HasLimit F) j y

theorem CategoryTheory.Limits.Types.limit_ext_iff' {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J (Type v)) (x : CategoryTheory.Limits.limit F) (y : CategoryTheory.Limits.limit F) : x = y ↔ ∀ (j : J), CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types F (_ : CategoryTheory.Limits.HasLimit F) j x = CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types F (_ : CategoryTheory.Limits.HasLimit F) j y

theorem CategoryTheory.Limits.Types.Limit.w_apply {J : Type v} [CategoryTheory.SmallCategory J] [UnivLE.{v, u} ] {F : CategoryTheory.Functor J (Type u)} {j : J} {j' : J} {x : CategoryTheory.Limits.limit F} (f : j ⟶ j') : J.map CategoryTheory.CategoryStruct.toQuiver (Type u) CategoryTheory.CategoryStruct.toQuiver F.toPrefunctor j j' f (CategoryTheory.Limits.limit.π J inst✝ (Type u) CategoryTheory.types F (_ : CategoryTheory.Limits.HasLimit F) j x) = CategoryTheory.Limits.limit.π J inst✝ (Type u) CategoryTheory.types F (_ : CategoryTheory.Limits.HasLimit F) j' x

theorem CategoryTheory.Limits.Types.Limit.lift_π_apply {J : Type v} [CategoryTheory.SmallCategory J] [UnivLE.{v, u} ] (F : CategoryTheory.Functor J (Type u)) (s : CategoryTheory.Limits.Cone F) (j : J) (x : s.pt) : CategoryTheory.Limits.limit.π J inst✝ (Type u) CategoryTheory.types F (_ : CategoryTheory.Limits.HasLimit F) j (CategoryTheory.Limits.limit.lift J inst✝ (Type u) CategoryTheory.types F (_ : CategoryTheory.Limits.HasLimit F) s x) = J.app inst✝ (Type u) CategoryTheory.types ((CategoryTheory.Functor.const J).obj s.pt) F s.π j x

theorem CategoryTheory.Limits.Types.Limit.map_π_apply {J : Type v} [CategoryTheory.SmallCategory J] [UnivLE.{v, u} ] {F : CategoryTheory.Functor J (Type u)} {G : CategoryTheory.Functor J (Type u)} (α : F ⟶ G) (j : J) (x : CategoryTheory.Limits.limit F) : CategoryTheory.Limits.limit.π J inst✝ (Type u) CategoryTheory.types G (_ : CategoryTheory.Limits.HasLimit G) j (CategoryTheory.Limits.limMap α x) = J.app inst✝ (Type u) CategoryTheory.types F G α j (CategoryTheory.Limits.limit.π J inst✝ (Type u) CategoryTheory.types F (_ : CategoryTheory.Limits.HasLimit F) j x)

@[simp]

theorem CategoryTheory.Limits.Types.Limit.w_apply' {J : Type v} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J (Type v)} {j : J} {j' : J} {x : CategoryTheory.Limits.limit F} (f : j ⟶ j') : J.map CategoryTheory.CategoryStruct.toQuiver (Type v) CategoryTheory.CategoryStruct.toQuiver F.toPrefunctor j j' f (CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types F (_ : CategoryTheory.Limits.HasLimit F) j x) = CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types F (_ : CategoryTheory.Limits.HasLimit F) j' x

@[simp]

theorem CategoryTheory.Limits.Types.Limit.lift_π_apply' {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J (Type v)) (s : CategoryTheory.Limits.Cone F) (j : J) (x : s.pt) : CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types F (_ : CategoryTheory.Limits.HasLimit F) j (CategoryTheory.Limits.limit.lift J inst✝ (Type v) CategoryTheory.types F (_ : CategoryTheory.Limits.HasLimit F) s x) = J.app inst✝ (Type v) CategoryTheory.types ((CategoryTheory.Functor.const J).obj s.pt) F s.π j x

@[simp]

theorem CategoryTheory.Limits.Types.Limit.map_π_apply' {J : Type v} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J (Type v)} {G : CategoryTheory.Functor J (Type v)} (α : F ⟶ G) (j : J) (x : CategoryTheory.Limits.limit F) : CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types G (_ : CategoryTheory.Limits.HasLimit G) j (CategoryTheory.Limits.limMap α x) = J.app inst✝ (Type v) CategoryTheory.types F G α j (CategoryTheory.Limits.limit.π J inst✝ (Type v) CategoryTheory.types F (_ : CategoryTheory.Limits.HasLimit F) j x)

In this section we verify that instances are available as expected.

def CategoryTheory.Limits.Types.Quot.Rel {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TypeMax) : (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.

def CategoryTheory.Limits.Types.Quot {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TypeMax) : TypeMax

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'.

def CategoryTheory.Limits.Types.colimitCocone {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TypeMax) : CategoryTheory.Limits.Cocone F

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

def CategoryTheory.Limits.Types.colimitCoconeIsColimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TypeMax) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Types.colimitCocone F)

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

instance CategoryTheory.Limits.Types.hasColimitsOfSize : CategoryTheory.Limits.HasColimitsOfSize.{v, v, max u v, max (u + 1) (v + 1)} TypeMax

The category of types has all colimits.

See https://stacks.math.columbia.edu/tag/002U.

instance CategoryTheory.Limits.Types.instHasColimitsTypeTypes : CategoryTheory.Limits.HasColimits (Type u)

instance CategoryTheory.Limits.Types.hasColimit {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TypeMax) : CategoryTheory.Limits.HasColimit F

instance CategoryTheory.Limits.Types.hasColimit' {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J (Type v)) : CategoryTheory.Limits.HasColimit F

noncomputable def CategoryTheory.Limits.Types.colimitEquivQuot {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TypeMax) : CategoryTheory.Limits.colimit F ≃ CategoryTheory.Limits.Types.Quot F

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

@[simp]

theorem CategoryTheory.Limits.Types.colimitEquivQuot_symm_apply {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TypeMax) (j : J) (x : F.obj j) : ↑(CategoryTheory.Limits.Types.colimitEquivQuot F).symm (Quot.mk (CategoryTheory.Limits.Types.Quot.Rel F) { fst := j, snd := x }) = CategoryTheory.Limits.colimit.ι J inst✝ TypeMax CategoryTheory.types F (_ : CategoryTheory.Limits.HasColimit F) j x

@[simp]

theorem CategoryTheory.Limits.Types.colimitEquivQuot_apply {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TypeMax) (j : J) (x : F.obj j) : ↑(CategoryTheory.Limits.Types.colimitEquivQuot F) (CategoryTheory.Limits.colimit.ι J inst✝ TypeMax CategoryTheory.types F (_ : CategoryTheory.Limits.HasColimit F) j x) = Quot.mk (CategoryTheory.Limits.Types.Quot.Rel F) { fst := j, snd := x }

theorem CategoryTheory.Limits.Types.Colimit.w_apply {J : Type v} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J TypeMax} {j : J} {j' : J} {x : F.obj j} (f : j ⟶ j') : CategoryTheory.Limits.colimit.ι J inst✝ TypeMax CategoryTheory.types F (_ : CategoryTheory.Limits.HasColimit F) j' (J.map CategoryTheory.CategoryStruct.toQuiver TypeMax CategoryTheory.CategoryStruct.toQuiver F.toPrefunctor j j' f x) = CategoryTheory.Limits.colimit.ι J inst✝ TypeMax CategoryTheory.types F (_ : CategoryTheory.Limits.HasColimit F) j x

theorem CategoryTheory.Limits.Types.Colimit.ι_desc_apply {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TypeMax) (s : CategoryTheory.Limits.Cocone F) (j : J) (x : F.obj j) : CategoryTheory.Limits.colimit.desc J inst✝ TypeMax CategoryTheory.types F (_ : CategoryTheory.Limits.HasColimit F) s (CategoryTheory.Limits.colimit.ι J inst✝ TypeMax CategoryTheory.types F (_ : CategoryTheory.Limits.HasColimit F) j x) = J.app inst✝ TypeMax CategoryTheory.types F ((CategoryTheory.Functor.const J).obj s.pt) s.ι j x

theorem CategoryTheory.Limits.Types.Colimit.ι_map_apply {J : Type v} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J TypeMax} {G : CategoryTheory.Functor J TypeMax} (α : F ⟶ G) (j : J) (x : F.obj j) : CategoryTheory.Limits.colim.map α (CategoryTheory.Limits.colimit.ι J inst✝ TypeMax CategoryTheory.types F (_ : CategoryTheory.Limits.HasColimit F) j x) = CategoryTheory.Limits.colimit.ι J inst✝ TypeMax CategoryTheory.types G (_ : CategoryTheory.Limits.HasColimit G) j (J.app inst✝ TypeMax CategoryTheory.types F G α j x)

@[simp]

theorem CategoryTheory.Limits.Types.Colimit.w_apply' {J : Type v} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J (Type v)} {j : J} {j' : J} {x : F.obj j} (f : j ⟶ j') : CategoryTheory.Limits.colimit.ι J inst✝ (Type v) CategoryTheory.types F (_ : CategoryTheory.Limits.HasColimit F) j' (J.map CategoryTheory.CategoryStruct.toQuiver (Type v) CategoryTheory.CategoryStruct.toQuiver F.toPrefunctor j j' f x) = CategoryTheory.Limits.colimit.ι J inst✝ (Type v) CategoryTheory.types F (_ : CategoryTheory.Limits.HasColimit F) j x

@[simp]

theorem CategoryTheory.Limits.Types.Colimit.ι_desc_apply' {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J (Type v)) (s : CategoryTheory.Limits.Cocone F) (j : J) (x : F.obj j) : CategoryTheory.Limits.colimit.desc J inst✝ (Type v) CategoryTheory.types F (_ : CategoryTheory.Limits.HasColimit F) s (CategoryTheory.Limits.colimit.ι J inst✝ (Type v) CategoryTheory.types F (_ : CategoryTheory.Limits.HasColimit F) j x) = J.app inst✝ (Type v) CategoryTheory.types F ((CategoryTheory.Functor.const J).obj s.pt) s.ι j x

@[simp]

theorem CategoryTheory.Limits.Types.Colimit.ι_map_apply' {J : Type v} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J (Type v)} {G : CategoryTheory.Functor J (Type v)} (α : F ⟶ G) (j : J) (x : F.obj j) : CategoryTheory.Limits.colim.map α (CategoryTheory.Limits.colimit.ι J inst✝ (Type v) CategoryTheory.types F (_ : CategoryTheory.Limits.HasColimit F) j x) = CategoryTheory.Limits.colimit.ι J inst✝ (Type v) CategoryTheory.types G (_ : CategoryTheory.Limits.HasColimit G) j (J.app inst✝ (Type v) CategoryTheory.types F G α j x)

theorem CategoryTheory.Limits.Types.colimit_sound {J : Type v} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J TypeMax} {j : J} {j' : J} {x : F.obj j} {x' : F.obj j'} (f : j ⟶ j') (w : J.map CategoryTheory.CategoryStruct.toQuiver TypeMax CategoryTheory.CategoryStruct.toQuiver F.toPrefunctor j j' f x = x') : CategoryTheory.Limits.colimit.ι J inst✝ TypeMax CategoryTheory.types F (_ : CategoryTheory.Limits.HasColimit F) j x = CategoryTheory.Limits.colimit.ι J inst✝ TypeMax CategoryTheory.types F (_ : CategoryTheory.Limits.HasColimit F) j' x'

theorem CategoryTheory.Limits.Types.colimit_sound' {J : Type v} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J TypeMax} {j : J} {j' : J} {x : F.obj j} {x' : F.obj j'} {j'' : J} (f : j ⟶ j'') (f' : j' ⟶ j'') (w : J.map CategoryTheory.CategoryStruct.toQuiver TypeMax CategoryTheory.CategoryStruct.toQuiver F.toPrefunctor j j'' f x = J.map CategoryTheory.CategoryStruct.toQuiver TypeMax CategoryTheory.CategoryStruct.toQuiver F.toPrefunctor j' j'' f' x') : CategoryTheory.Limits.colimit.ι J inst✝ TypeMax CategoryTheory.types F (_ : CategoryTheory.Limits.HasColimit F) j x = CategoryTheory.Limits.colimit.ι J inst✝ TypeMax CategoryTheory.types F (_ : CategoryTheory.Limits.HasColimit F) j' x'

theorem CategoryTheory.Limits.Types.colimit_eq {J : Type v} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J TypeMax} {j : J} {j' : J} {x : F.obj j} {x' : F.obj j'} (w : CategoryTheory.Limits.colimit.ι J inst✝ TypeMax CategoryTheory.types F (_ : CategoryTheory.Limits.HasColimit F) j x = CategoryTheory.Limits.colimit.ι J inst✝ TypeMax CategoryTheory.types F (_ : CategoryTheory.Limits.HasColimit F) j' x') : EqvGen (CategoryTheory.Limits.Types.Quot.Rel F) { fst := j, snd := x } { fst := j', snd := x' }

theorem CategoryTheory.Limits.Types.jointly_surjective {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TypeMax) {t : CategoryTheory.Limits.Cocone F} (h : CategoryTheory.Limits.IsColimit t) (x : t.pt) : ∃ j y, J.app inst✝ TypeMax CategoryTheory.types F ((CategoryTheory.Functor.const J).obj t.pt) t.ι j y = x

theorem CategoryTheory.Limits.Types.jointly_surjective' {J : Type v} [CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J TypeMax} (x : CategoryTheory.Limits.colimit F) : ∃ j y, CategoryTheory.Limits.colimit.ι J inst✝ TypeMax CategoryTheory.types F (_ : CategoryTheory.Limits.HasColimit F) j y = x

A variant of jointly_surjective for x : colimit F.

def CategoryTheory.Limits.Types.FilteredColimit.Rel {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TypeMax) (x : (j : J) × F.obj j) (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.

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

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

noncomputable def CategoryTheory.Limits.Types.FilteredColimit.isColimitOf {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TypeMax) (t : CategoryTheory.Limits.Cocone F) (hsurj : ∀ (x : t.pt), ∃ i xi, x = J.app inst✝ TypeMax CategoryTheory.types F ((CategoryTheory.Functor.const J).obj t.pt) t.ι i xi) (hinj : ∀ (i j : J) (xi : F.obj i) (xj : F.obj j), J.app inst✝ TypeMax CategoryTheory.types F ((CategoryTheory.Functor.const J).obj t.pt) t.ι i xi = J.app inst✝ TypeMax CategoryTheory.types F ((CategoryTheory.Functor.const J).obj t.pt) t.ι j xj → ∃ k f g, J.map CategoryTheory.CategoryStruct.toQuiver TypeMax CategoryTheory.CategoryStruct.toQuiver F.toPrefunctor i k f xi = J.map CategoryTheory.CategoryStruct.toQuiver TypeMax CategoryTheory.CategoryStruct.toQuiver F.toPrefunctor j k g xj) : CategoryTheory.Limits.IsColimit t

Recognizing filtered colimits of types.

theorem CategoryTheory.Limits.Types.FilteredColimit.rel_equiv {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TypeMax) [CategoryTheory.IsFilteredOrEmpty J] : Equivalence (CategoryTheory.Limits.Types.FilteredColimit.Rel F)

theorem CategoryTheory.Limits.Types.FilteredColimit.rel_eq_eqvGen_quot_rel {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TypeMax) [CategoryTheory.IsFilteredOrEmpty J] : CategoryTheory.Limits.Types.FilteredColimit.Rel F = EqvGen (CategoryTheory.Limits.Types.Quot.Rel F)

theorem CategoryTheory.Limits.Types.FilteredColimit.colimit_eq_iff_aux {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TypeMax) [CategoryTheory.IsFilteredOrEmpty J] {i : J} {j : J} {xi : F.obj i} {xj : F.obj j} : J.app inst✝ TypeMax CategoryTheory.types F ((CategoryTheory.Functor.const J).obj (CategoryTheory.Limits.Types.colimitCocone F).pt) (CategoryTheory.Limits.Types.colimitCocone F).ι i xi = J.app inst✝ TypeMax CategoryTheory.types F ((CategoryTheory.Functor.const J).obj (CategoryTheory.Limits.Types.colimitCocone F).pt) (CategoryTheory.Limits.Types.colimitCocone F).ι j xj ↔ CategoryTheory.Limits.Types.FilteredColimit.Rel F { fst := i, snd := xi } { fst := j, snd := xj }

theorem CategoryTheory.Limits.Types.FilteredColimit.isColimit_eq_iff {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TypeMax) [CategoryTheory.IsFilteredOrEmpty J] {t : CategoryTheory.Limits.Cocone F} (ht : CategoryTheory.Limits.IsColimit t) {i : J} {j : J} {xi : F.obj i} {xj : F.obj j} : J.app inst✝ TypeMax CategoryTheory.types F ((CategoryTheory.Functor.const J).obj t.pt) t.ι i xi = J.app inst✝ TypeMax CategoryTheory.types F ((CategoryTheory.Functor.const J).obj t.pt) t.ι j xj ↔ ∃ k f g, J.map CategoryTheory.CategoryStruct.toQuiver TypeMax CategoryTheory.CategoryStruct.toQuiver F.toPrefunctor i k f xi = J.map CategoryTheory.CategoryStruct.toQuiver TypeMax CategoryTheory.CategoryStruct.toQuiver F.toPrefunctor j k g xj

theorem CategoryTheory.Limits.Types.FilteredColimit.colimit_eq_iff {J : Type v} [CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J TypeMax) [CategoryTheory.IsFilteredOrEmpty J] {i : J} {j : J} {xi : F.obj i} {xj : F.obj j} : CategoryTheory.Limits.colimit.ι J inst✝ TypeMax CategoryTheory.types F (_ : CategoryTheory.Limits.HasColimit F) i xi = CategoryTheory.Limits.colimit.ι J inst✝ TypeMax CategoryTheory.types F (_ : CategoryTheory.Limits.HasColimit F) j xj ↔ ∃ k f g, J.map CategoryTheory.CategoryStruct.toQuiver TypeMax CategoryTheory.CategoryStruct.toQuiver F.toPrefunctor i k f xi = J.map CategoryTheory.CategoryStruct.toQuiver TypeMax CategoryTheory.CategoryStruct.toQuiver F.toPrefunctor j k g xj

def CategoryTheory.Limits.Types.Image {α : Type u} {β : Type u} (f : α ⟶ β) : Type u

the image of a morphism in Type is just Set.range f

instance CategoryTheory.Limits.Types.instInhabitedImage {α : Type u} {β : Type u} (f : α ⟶ β) [Inhabited α] : Inhabited (CategoryTheory.Limits.Types.Image f)

def CategoryTheory.Limits.Types.Image.ι {α : Type u} {β : Type u} (f : α ⟶ β) : CategoryTheory.Limits.Types.Image f ⟶ β

the inclusion of Image f into the target

instance CategoryTheory.Limits.Types.instMonoTypeTypesImageι {α : Type u} {β : Type u} (f : α ⟶ β) : CategoryTheory.Mono (CategoryTheory.Limits.Types.Image.ι f)

noncomputable def CategoryTheory.Limits.Types.Image.lift {α : Type u} {β : Type u} {f : α ⟶ β} (F' : CategoryTheory.Limits.MonoFactorisation f) : CategoryTheory.Limits.Types.Image f ⟶ F'.I

the universal property for the image factorisation

theorem CategoryTheory.Limits.Types.Image.lift_fac {α : Type u} {β : Type u} {f : α ⟶ β} (F' : CategoryTheory.Limits.MonoFactorisation f) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.Image.lift F') F'.m = CategoryTheory.Limits.Types.Image.ι f

def CategoryTheory.Limits.Types.monoFactorisation {α : Type u} {β : Type u} (f : α ⟶ β) : CategoryTheory.Limits.MonoFactorisation f

the factorisation of any morphism in Type through a mono.

noncomputable def CategoryTheory.Limits.Types.isImage {α : Type u} {β : Type u} (f : α ⟶ β) : CategoryTheory.Limits.IsImage (CategoryTheory.Limits.Types.monoFactorisation f)

the factorisation through a mono has the universal property of the image.

instance CategoryTheory.Limits.Types.instHasImageTypeTypes {α : Type u} {β : Type u} (f : α ⟶ β) : CategoryTheory.Limits.HasImage f

instance CategoryTheory.Limits.Types.instHasImagesTypeTypes : CategoryTheory.Limits.HasImages (Type u)

instance CategoryTheory.Limits.Types.instHasImageMapsTypeTypesInstHasImagesTypeTypes : CategoryTheory.Limits.HasImageMaps (Type u)