The colimit type of a functor to types

Given a category J (with J : Type u and [Category.{v} J]) and a functor F : J ⥤ Type w₀, we introduce a type F.ColimitType : Type (max u w₀), which satisfies a certain universal property of the colimit: it is defined as a suitable quotient of Σ j, F.obj j. This universal property is not expressed in a categorical way (as in general Type (max u w₀) is not the same as Type u).

We also introduce a notion of cocone of F : J ⥤ Type w₀, this is F.CoconeTypes, or more precisely Functor.CoconeTypes.{w₁} F, which consists of a candidate colimit type for F which is in Type w₁ (in case w₁ = w₀, we shall show this is the same as the data of c : Cocone F in the categorical sense). Given c : F.CoconeTypes, we also introduce a property c.IsColimit which says that the canonical map F.ColimitType → c.pt is a bijection, and we shall show (TODO) that when w₁ = w₀, it is equivalent to saying that the corresponding cocone in a categorical sense is a colimit.

TODO

• refactor DirectedSystem and the construction of colimits in Type by using Functor.ColimitType.
• add a similar API for limits in Type?

structure CategoryTheory.Functor.CoconeTypes {J : Type u} [Category.{v, u} J] (F : Functor J (Type w₀)) : Type (max (max u w₀) (w₁ + 1))

Given a functor F : J ⥤ Type w₀, this is a "cocone" of F where we allow the point pt to be in a different universe than w.

• pt : Type w₁

  the point of the cocone

• ι (j : J) : F.obj j → self.pt

  a family of maps to pt

• ι_naturality {j j' : J} (f : j ⟶ j') : self.ι j' ∘ ⇑(ConcreteCategory.hom (F.map f)) = self.ι j

@[simp]

theorem CategoryTheory.Functor.CoconeTypes.ι_naturality_apply {J : Type u} [Category.{v, u} J] {F : Functor J (Type w₀)} (c : F.CoconeTypes) {j j' : J} (f : j ⟶ j') (x : F.obj j) : c.ι j' ((ConcreteCategory.hom (F.map f)) x) = c.ι j x

def CategoryTheory.Functor.CoconeTypes.postcomp {J : Type u} [Category.{v, u} J] {F : Functor J (Type w₀)} (c : F.CoconeTypes) {T : Type w₂} (φ : c.pt → T) : F.CoconeTypes

Given c : F.CoconeTypes and a map φ : c.pt → T, this is the cocone for F obtained by postcomposition with φ.

Equations

• c.postcomp φ = { pt := T, ι := fun (j : J) => φ ∘ c.ι j, ι_naturality := ⋯ }

@[simp]

theorem CategoryTheory.Functor.CoconeTypes.postcomp_pt {J : Type u} [Category.{v, u} J] {F : Functor J (Type w₀)} (c : F.CoconeTypes) {T : Type w₂} (φ : c.pt → T) : (c.postcomp φ).pt = T

@[simp]

theorem CategoryTheory.Functor.CoconeTypes.postcomp_ι {J : Type u} [Category.{v, u} J] {F : Functor J (Type w₀)} (c : F.CoconeTypes) {T : Type w₂} (φ : c.pt → T) : (c.postcomp φ).ι = fun (j : J) => φ ∘ c.ι j

def CategoryTheory.Functor.CoconeTypes.precompose {J : Type u} [Category.{v, u} J] {F : Functor J (Type w₀)} (c : F.CoconeTypes) {G : Functor J (Type w₀')} (app : (j : J) → G.obj j → F.obj j) (naturality : ∀ {j j' : J} (f : j ⟶ j'), app j' ∘ ⇑(ConcreteCategory.hom (G.map f)) = ⇑(ConcreteCategory.hom (F.map f)) ∘ app j) : G.CoconeTypes

The cocone for G : J ⥤ Type w₀' that is deduced from a cocone for F : J ⥤ Type w₀ and a natural map G.obj j → F.obj j for all j : J.

Equations

• c.precompose app naturality = { pt := c.pt, ι := fun (j : J) => c.ι j ∘ app j, ι_naturality := ⋯ }

@[simp]

theorem CategoryTheory.Functor.CoconeTypes.precompose_pt {J : Type u} [Category.{v, u} J] {F : Functor J (Type w₀)} (c : F.CoconeTypes) {G : Functor J (Type w₀')} (app : (j : J) → G.obj j → F.obj j) (naturality : ∀ {j j' : J} (f : j ⟶ j'), app j' ∘ ⇑(ConcreteCategory.hom (G.map f)) = ⇑(ConcreteCategory.hom (F.map f)) ∘ app j) : (c.precompose app naturality).pt = c.pt

@[simp]

theorem CategoryTheory.Functor.CoconeTypes.precompose_ι {J : Type u} [Category.{v, u} J] {F : Functor J (Type w₀)} (c : F.CoconeTypes) {G : Functor J (Type w₀')} (app : (j : J) → G.obj j → F.obj j) (naturality : ∀ {j j' : J} (f : j ⟶ j'), app j' ∘ ⇑(ConcreteCategory.hom (G.map f)) = ⇑(ConcreteCategory.hom (F.map f)) ∘ app j) : (c.precompose app naturality).ι = fun (j : J) => c.ι j ∘ app j

def CategoryTheory.Functor.CoconeTypes.precomp {J : Type u} [Category.{v, u} J] {F : Functor J (Type w₀)} (c : F.CoconeTypes) {J' : Type u_1} [Category.{v_1, u_1} J'] (G : Functor J' J) : (G.comp F).CoconeTypes

Given F : J ⥤ w₀, c : F.CoconeTypes and G : J' ⥤ J, this is the induced cocone in (G ⋙ F).CoconeTypes.

Equations

• c.precomp G = { pt := c.pt, ι := fun (x : J') => c.ι (G.obj x), ι_naturality := ⋯ }

@[simp]

theorem CategoryTheory.Functor.CoconeTypes.precomp_ι {J : Type u} [Category.{v, u} J] {F : Functor J (Type w₀)} (c : F.CoconeTypes) {J' : Type u_1} [Category.{v_1, u_1} J'] (G : Functor J' J) (x✝ : J') (a✝ : F.obj (G.obj x✝)) : (c.precomp G).ι x✝ a✝ = c.ι (G.obj x✝) a✝

@[simp]

theorem CategoryTheory.Functor.CoconeTypes.precomp_pt {J : Type u} [Category.{v, u} J] {F : Functor J (Type w₀)} (c : F.CoconeTypes) {J' : Type u_1} [Category.{v_1, u_1} J'] (G : Functor J' J) : (c.precomp G).pt = c.pt

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

Given F : J ⥤ Type w₀, this is the relation Σ j, F.obj j which generates an equivalence relation such that the quotient identifies to the colimit type of F.

Equations

• F.ColimitTypeRel p p' = ∃ (f : p.fst ⟶ p'.fst), p'.snd = (CategoryTheory.ConcreteCategory.hom (F.map f)) p.snd

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

The colimit type of a functor F : J ⥤ Type w₀. (It may not be in Type w₀.)

Equations

• F.ColimitType = Quot F.ColimitTypeRel

def CategoryTheory.Functor.ιColimitType {J : Type u} [Category.{v, u} J] (F : Functor J (Type w₀)) (j : J) (x : F.obj j) : F.ColimitType

The canonical maps F.obj j → F.ColimitType.

Equations

• F.ιColimitType j x = Quot.mk F.ColimitTypeRel ⟨j, x⟩

theorem CategoryTheory.Functor.ιColimitType_eq_iff {J : Type u} [Category.{v, u} 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 ↔ Relation.EqvGen F.ColimitTypeRel ⟨j, x⟩ ⟨j', y⟩

theorem CategoryTheory.Functor.ιColimitType_eq_of_map_eq_map {J : Type u} [Category.{v, u} J] (F : Functor J (Type w₀)) {j j' : J} (x : F.obj j) (y : F.obj j') {k : J} (f : j ⟶ k) (f' : j' ⟶ k) (H : (ConcreteCategory.hom (F.map f)) x = (ConcreteCategory.hom (F.map f')) y) : F.ιColimitType j x = F.ιColimitType j' y

theorem CategoryTheory.Functor.ιColimitType_jointly_surjective {J : Type u} [Category.{v, u} J] (F : Functor J (Type w₀)) (t : F.ColimitType) : ∃ (j : J) (x : F.obj j), F.ιColimitType j x = t

@[simp]

theorem CategoryTheory.Functor.ιColimitType_map {J : Type u} [Category.{v, u} J] (F : Functor J (Type w₀)) {j j' : J} (f : j ⟶ j') (x : F.obj j) : F.ιColimitType j' ((ConcreteCategory.hom (F.map f)) x) = F.ιColimitType j x

def CategoryTheory.Functor.coconeTypes {J : Type u} [Category.{v, u} J] (F : Functor J (Type w₀)) : F.CoconeTypes

The cocone corresponding to F.ColimitType.

Equations

• F.coconeTypes = { pt := F.ColimitType, ι := fun (j : J) => F.ιColimitType j, ι_naturality := ⋯ }

@[simp]

theorem CategoryTheory.Functor.coconeTypes_pt {J : Type u} [Category.{v, u} J] (F : Functor J (Type w₀)) : F.coconeTypes.pt = F.ColimitType

@[simp]

theorem CategoryTheory.Functor.coconeTypes_ι {J : Type u} [Category.{v, u} J] (F : Functor J (Type w₀)) : F.coconeTypes.ι = fun (j : J) => F.ιColimitType j

def CategoryTheory.Functor.descColimitType {J : Type u} [Category.{v, u} J] (F : Functor J (Type w₀)) (c : F.CoconeTypes) : F.ColimitType → c.pt

A heterogeneous universe version of the universal property of the colimit is satisfied by F.ColimitType together with the maps F.ιColimitType j.

Equations

• F.descColimitType c = Quot.lift (fun (x : (j : J) × F.obj j) => match x with | ⟨j, x⟩ => c.ι j x) ⋯

@[simp]

theorem CategoryTheory.Functor.descColimitType_comp_ι {J : Type u} [Category.{v, u} J] (F : Functor J (Type w₀)) (c : F.CoconeTypes) (j : J) : F.descColimitType c ∘ F.ιColimitType j = c.ι j

@[simp]

theorem CategoryTheory.Functor.descColimitType_ιColimitType_apply {J : Type u} [Category.{v, u} J] (F : Functor J (Type w₀)) (c : F.CoconeTypes) (j : J) (x : F.obj j) : F.descColimitType c (F.ιColimitType j x) = c.ι j x

theorem CategoryTheory.Functor.CoconeTypes.descColimitType_surjective_iff {J : Type u} [Category.{v, u} J] {F : Functor J (Type w₀)} (c : F.CoconeTypes) : Function.Surjective (F.descColimitType c) ↔ ∀ (z : c.pt), ∃ (i : J) (x : F.obj i), c.ι i x = z

structure CategoryTheory.Functor.CoconeTypes.IsColimit {J : Type u} [Category.{v, u} J] {F : Functor J (Type w₀)} (c : F.CoconeTypes) : Prop

Given F : J ⥤ Type w₀ and c : F.CoconeTypes, this is the property that c is a colimit. It is defined by saying the canonical map F.descColimitType c : F.ColimitType → c.pt is a bijection.

• bijective : Function.Bijective (F.descColimitType c)

noncomputable def CategoryTheory.Functor.CoconeTypes.IsColimit.equiv {J : Type u} [Category.{v, u} J] {F : Functor J (Type w₀)} {c : F.CoconeTypes} (hc : c.IsColimit) : F.ColimitType ≃ c.pt

Given F : J ⥤ Type w₀, and c : F.CoconeTypes a cocone that is a colimit, this is the equivalence F.ColimitType ≃ c.pt.

Equations

• hc.equiv = Equiv.ofBijective (F.descColimitType c) ⋯

@[simp]

theorem CategoryTheory.Functor.CoconeTypes.IsColimit.equiv_apply {J : Type u} [Category.{v, u} J] {F : Functor J (Type w₀)} {c : F.CoconeTypes} (hc : c.IsColimit) (a✝ : F.ColimitType) : hc.equiv a✝ = F.descColimitType c a✝

@[simp]

theorem CategoryTheory.Functor.CoconeTypes.IsColimit.equiv_symm_ι_apply {J : Type u} [Category.{v, u} J] {F : Functor J (Type w₀)} {c : F.CoconeTypes} (hc : c.IsColimit) (j : J) (x : F.obj j) : hc.equiv.symm (c.ι j x) = F.ιColimitType j x

theorem CategoryTheory.Functor.CoconeTypes.IsColimit.ι_jointly_surjective {J : Type u} [Category.{v, u} J] {F : Functor J (Type w₀)} {c : F.CoconeTypes} (hc : c.IsColimit) (y : c.pt) : ∃ (j : J) (x : F.obj j), c.ι j x = y

theorem CategoryTheory.Functor.CoconeTypes.IsColimit.funext {J : Type u} [Category.{v, u} J] {F : Functor J (Type w₀)} {c : F.CoconeTypes} (hc : c.IsColimit) {T : Type w₂} {f g : c.pt → T} (h : ∀ (j : J), f ∘ c.ι j = g ∘ c.ι j) : f = g

theorem CategoryTheory.Functor.CoconeTypes.IsColimit.exists_desc {J : Type u} [Category.{v, u} J] {F : Functor J (Type w₀)} {c : F.CoconeTypes} (hc : c.IsColimit) (c' : F.CoconeTypes) : ∃ (f : c.pt → c'.pt), ∀ (j : J), f ∘ c.ι j = c'.ι j

noncomputable def CategoryTheory.Functor.CoconeTypes.IsColimit.desc {J : Type u} [Category.{v, u} J] {F : Functor J (Type w₀)} {c : F.CoconeTypes} (hc : c.IsColimit) (c' : F.CoconeTypes) : c.pt → c'.pt

If F : J ⥤ Type w₀ and c : F.CoconeTypes is colimit, then c satisfies a heterogeneous universe version of the universal property of colimits.

Equations

• hc.desc c' = ⋯.choose

@[simp]

theorem CategoryTheory.Functor.CoconeTypes.IsColimit.fac {J : Type u} [Category.{v, u} J] {F : Functor J (Type w₀)} {c : F.CoconeTypes} (hc : c.IsColimit) (c' : F.CoconeTypes) (j : J) : hc.desc c' ∘ c.ι j = c'.ι j

@[simp]

theorem CategoryTheory.Functor.CoconeTypes.IsColimit.fac_apply {J : Type u} [Category.{v, u} J] {F : Functor J (Type w₀)} {c : F.CoconeTypes} (hc : c.IsColimit) (c' : F.CoconeTypes) (j : J) (x : F.obj j) : hc.desc c' (c.ι j x) = c'.ι j x

theorem CategoryTheory.Functor.CoconeTypes.IsColimit.of_equiv {J : Type u} [Category.{v, u} J] {F : Functor J (Type w₀)} {c : F.CoconeTypes} (hc : c.IsColimit) {c' : F.CoconeTypes} (e : c.pt ≃ c'.pt) (he : ∀ (j : J) (x : F.obj j), c'.ι j x = e (c.ι j x)) : c'.IsColimit

theorem CategoryTheory.Functor.CoconeTypes.IsColimit.iff_bijective {J : Type u} [Category.{v, u} J] {F : Functor J (Type w₀)} {c : F.CoconeTypes} (hc : c.IsColimit) {c' : F.CoconeTypes} (f : c.pt → c'.pt) (hf : ∀ (j : J) (x : F.obj j), c'.ι j x = f (c.ι j x)) : c'.IsColimit ↔ Function.Bijective f

structure CategoryTheory.Functor.CoconeTypes.IsColimitCore {J : Type u} [Category.{v, u} J] {F : Functor J (Type w₀)} (c : F.CoconeTypes) : Type (max (max (max u w₀) w₁) (w₂ + 1))

Structure which expresses that c : F.CoconeTypes satisfies the universal property of the colimit of types: compatible families of maps F.obj j → T (where T is any type in a specified universe) descend in a unique way as maps c.pt → T.

• desc (c' : F.CoconeTypes) : c.pt → c'.pt

  any cocone descends (in a unique way) as a map

• fac (c' : F.CoconeTypes) (j : J) : self.desc c' ∘ c.ι j = c'.ι j
• funext {T : Type w₂} {f g : c.pt → T} (h : ∀ (j : J), f ∘ c.ι j = g ∘ c.ι j) : f = g

@[simp]

theorem CategoryTheory.Functor.CoconeTypes.IsColimitCore.fac_apply {J : Type u} [Category.{v, u} J] {F : Functor J (Type w₀)} {c : F.CoconeTypes} (hc : c.IsColimitCore) (c' : F.CoconeTypes) (j : J) (x : F.obj j) : hc.desc c' (c.ι j x) = c'.ι j x

def CategoryTheory.Functor.CoconeTypes.IsColimitCore.down {J : Type u} [Category.{v, u} J] {F : Functor J (Type w₀)} {c : F.CoconeTypes} (hc : c.IsColimitCore) : c.IsColimitCore

Any structure IsColimitCore.{max w₂ w₃} c can be lowered to IsColimitCore.{w₂} c

Equations

• hc.down = { desc := fun (c' : F.CoconeTypes) => Equiv.ulift.toFun ∘ hc.desc (c'.postcomp ⇑Equiv.ulift.symm), fac := ⋯, funext := ⋯ }

def CategoryTheory.Functor.CoconeTypes.IsColimitCore.precompose {J : Type u} [Category.{v, u} J] {F : Functor J (Type w₀)} {c : F.CoconeTypes} (hc : c.IsColimitCore) {G : Functor J (Type w₀')} (e : (j : J) → G.obj j ≃ F.obj j) (naturality : ∀ {j j' : J} (f : j ⟶ j'), ⇑(e j') ∘ ⇑(ConcreteCategory.hom (G.map f)) = ⇑(ConcreteCategory.hom (F.map f)) ∘ ⇑(e j)) : (c.precompose (fun {j' : J} => ⇑(e j')) ⋯).IsColimitCore

A colimit cocone for F : J ⥤ Type w₀ induces a colimit cocone for G : J ⥤ Type w₉' when we have a natural equivalence G.obj j ≃ F.obj j for all j : J.

Equations

• hc.precompose e naturality = { desc := fun (c' : G.CoconeTypes) => hc.desc (c'.precompose (fun {j' : J} => ⇑(e j').symm) ⋯), fac := ⋯, funext := ⋯ }

noncomputable def CategoryTheory.Functor.CoconeTypes.IsColimit.isColimitCore {J : Type u} [Category.{v, u} J] {F : Functor J (Type w₀)} {c : F.CoconeTypes} (hc : c.IsColimit) : c.IsColimitCore

When c : F.CoconeTypes satisfies the property c.IsColimit, this is a term in IsColimitCore.{w₂} c for any universe w₂.

Equations

• hc.isColimitCore = { desc := hc.desc, fac := ⋯, funext := ⋯ }

@[simp]

theorem CategoryTheory.Functor.CoconeTypes.IsColimit.isColimitCore_desc {J : Type u} [Category.{v, u} J] {F : Functor J (Type w₀)} {c : F.CoconeTypes} (hc : c.IsColimit) (c' : F.CoconeTypes) (a✝ : c.pt) : hc.isColimitCore.desc c' a✝ = hc.desc c' a✝

theorem CategoryTheory.Functor.CoconeTypes.IsColimitCore.isColimit {J : Type u} [Category.{v, u} J] {F : Functor J (Type w₀)} (c : F.CoconeTypes) (hc : c.IsColimitCore) : c.IsColimit

theorem CategoryTheory.Functor.CoconeTypes.IsColimit.precompose {J : Type u} [Category.{v, u} J] {F : Functor J (Type w₀)} {c : F.CoconeTypes} (hc : c.IsColimit) {G : Functor J (Type w₀')} (e : (j : J) → G.obj j ≃ F.obj j) (naturality : ∀ {j j' : J} (f : j ⟶ j'), ⇑(e j') ∘ ⇑(ConcreteCategory.hom (G.map f)) = ⇑(ConcreteCategory.hom (F.map f)) ∘ ⇑(e j)) : (c.precompose (fun {j' : J} => ⇑(e j')) ⋯).IsColimit

theorem CategoryTheory.Functor.CoconeTypes.isColimit_precompose_iff {J : Type u} [Category.{v, u} J] {F : Functor J (Type w₀)} (c : F.CoconeTypes) {G : Functor J (Type w₀')} (e : (j : J) → G.obj j ≃ F.obj j) (naturality : ∀ {j j' : J} (f : j ⟶ j'), ⇑(e j') ∘ ⇑(ConcreteCategory.hom (G.map f)) = ⇑(ConcreteCategory.hom (F.map f)) ∘ ⇑(e j)) : (c.precompose (fun {j' : J} => ⇑(e j')) ⋯).IsColimit ↔ c.IsColimit

theorem CategoryTheory.Functor.isColimit_coconeTypes {J : Type u} [Category.{v, u} J] (F : Functor J (Type w₀)) : F.coconeTypes.IsColimit