ULift creates small (co)limits

This file shows that uliftFunctor.{v, u} creates (and hence preserves) limits and colimits indexed by J with [Category.{w, u} J].

It also shows that uliftFunctor.{v, u} preserves "all" limits, potentially too big to exist in Type u).

def CategoryTheory.Limits.Types.sectionsEquiv {J : Type u_1} [CategoryTheory.Category.{u_2, u_1} J] (K : CategoryTheory.Functor J (Type u)) : ↑K.sections ≃ ↑(K.comp CategoryTheory.uliftFunctor.{v, u} ).sections

The equivalence between K.sections and (K ⋙ uliftFunctor.{v, u}).sections. This is used to show that uliftFunctor preserves limits that are potentially too large to exist in the source category.

Equations

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

noncomputable instance CategoryTheory.Limits.Types.instPreservesLimitsOfSizeUliftFunctor : CategoryTheory.Limits.PreservesLimitsOfSize.{w', w, u, max u v, u + 1, max (u + 1) (v + 1)} CategoryTheory.uliftFunctor.{v, u}

The functor uliftFunctor : Type u ⥤ Type (max u v) preserves limits of arbitrary size.

Equations

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

noncomputable instance CategoryTheory.Limits.Types.instCreatesLimitsOfSizeUliftFunctor : CategoryTheory.CreatesLimitsOfSize.{w, u, u, max u v, u + 1, max (u + 1) (v + 1)} CategoryTheory.uliftFunctor.{v, u}

The functor uliftFunctor : Type u ⥤ Type (max u v) creates u-small limits.

Equations

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

def CategoryTheory.Limits.Types.coconeOfSet {J : Type u_1} [CategoryTheory.Category.{u_2, u_1} J] {K : CategoryTheory.Functor J (Type u)} {lc : CategoryTheory.Limits.Cocone (K.comp CategoryTheory.uliftFunctor.{v, u} )} (ls : Set lc.pt) : CategoryTheory.Limits.Cocone K

Given a subset of the cocone point of a cocone over the lifted functor, produce a cocone over the original functor.

Equations

• CategoryTheory.Limits.Types.coconeOfSet ls = { pt := ULift.{u, 0} Prop, ι := { app := fun (j : J) (x : K.obj j) => { down := lc.ι.app j { down := x } ∈ ls }, naturality := ⋯ } }

def CategoryTheory.Limits.Types.descSet {J : Type u_1} [CategoryTheory.Category.{u_2, u_1} J] {K : CategoryTheory.Functor J (Type u)} {c : CategoryTheory.Limits.Cocone K} (hc : CategoryTheory.Limits.IsColimit c) {lc : CategoryTheory.Limits.Cocone (K.comp CategoryTheory.uliftFunctor.{v, u} )} (ls : Set lc.pt) : Set c.pt

Given a subset of the cocone point of a cocone over the lifted functor, produce a subset of the cocone point of a colimit cocone over the original functor.

Equations

• CategoryTheory.Limits.Types.descSet hc ls = {x : c.pt | (hc.desc (CategoryTheory.Limits.Types.coconeOfSet ls) x).down}

theorem CategoryTheory.Limits.Types.descSet_spec {J : Type u_1} [CategoryTheory.Category.{u_2, u_1} J] {K : CategoryTheory.Functor J (Type u)} {c : CategoryTheory.Limits.Cocone K} (hc : CategoryTheory.Limits.IsColimit c) {lc : CategoryTheory.Limits.Cocone (K.comp CategoryTheory.uliftFunctor.{v, u} )} (s : Set c.pt) (ls : Set lc.pt) : CategoryTheory.Limits.Types.descSet hc ls = s ↔ ∀ (j : J) (x : K.obj j), lc.ι.app j { down := x } ∈ ls ↔ c.ι.app j x ∈ s

Characterization the map descSet hc: the image of an element in a vertex of the original diagram in the cocone point lies in descSet hc ls if and only if the image of the corresponding element in the lifted diagram lie in ls.

theorem CategoryTheory.Limits.Types.mem_descSet_singleton {J : Type u_1} [CategoryTheory.Category.{u_2, u_1} J] {K : CategoryTheory.Functor J (Type u)} {c : CategoryTheory.Limits.Cocone K} (hc : CategoryTheory.Limits.IsColimit c) {lc : CategoryTheory.Limits.Cocone (K.comp CategoryTheory.uliftFunctor.{v, u} )} {x : lc.pt} {j : J} {y : K.obj j} : c.ι.app j y ∈ CategoryTheory.Limits.Types.descSet hc {x} ↔ lc.ι.app j { down := y } = x

theorem CategoryTheory.Limits.Types.descSet_univ {J : Type u_1} [CategoryTheory.Category.{u_2, u_1} J] {K : CategoryTheory.Functor J (Type u)} {c : CategoryTheory.Limits.Cocone K} (hc : CategoryTheory.Limits.IsColimit c) (lc : CategoryTheory.Limits.Cocone (K.comp CategoryTheory.uliftFunctor.{v, u} )) : CategoryTheory.Limits.Types.descSet hc Set.univ = Set.univ

theorem CategoryTheory.Limits.Types.iUnion_descSet_singleton {J : Type u_1} [CategoryTheory.Category.{u_2, u_1} J] {K : CategoryTheory.Functor J (Type u)} {c : CategoryTheory.Limits.Cocone K} (hc : CategoryTheory.Limits.IsColimit c) (lc : CategoryTheory.Limits.Cocone (K.comp CategoryTheory.uliftFunctor.{v, u} )) : ⋃ (x : lc.pt), CategoryTheory.Limits.Types.descSet hc {x} = Set.univ

theorem CategoryTheory.Limits.Types.descSet_empty {J : Type u_1} [CategoryTheory.Category.{u_2, u_1} J] {K : CategoryTheory.Functor J (Type u)} {c : CategoryTheory.Limits.Cocone K} (hc : CategoryTheory.Limits.IsColimit c) (lc : CategoryTheory.Limits.Cocone (K.comp CategoryTheory.uliftFunctor.{v, u} )) : CategoryTheory.Limits.Types.descSet hc ∅ = ∅

theorem CategoryTheory.Limits.Types.descSet_inter_of_ne {J : Type u_1} [CategoryTheory.Category.{u_2, u_1} J] {K : CategoryTheory.Functor J (Type u)} {c : CategoryTheory.Limits.Cocone K} (hc : CategoryTheory.Limits.IsColimit c) (lc : CategoryTheory.Limits.Cocone (K.comp CategoryTheory.uliftFunctor.{v, u} )) (x : lc.pt) (y : lc.pt) (hn : x ≠ y) : CategoryTheory.Limits.Types.descSet hc {x} ∩ CategoryTheory.Limits.Types.descSet hc {y} = ∅

theorem CategoryTheory.Limits.Types.exists_unique_mem_descSet {J : Type u_1} [CategoryTheory.Category.{u_2, u_1} J] {K : CategoryTheory.Functor J (Type u)} {c : CategoryTheory.Limits.Cocone K} (hc : CategoryTheory.Limits.IsColimit c) (lc : CategoryTheory.Limits.Cocone (K.comp CategoryTheory.uliftFunctor.{v, u} )) (x : c.pt) : ∃! y : lc.pt, x ∈ CategoryTheory.Limits.Types.descSet hc {y}

noncomputable def CategoryTheory.Limits.Types.descFun {J : Type u_1} [CategoryTheory.Category.{u_2, u_1} J] {K : CategoryTheory.Functor J (Type u)} {c : CategoryTheory.Limits.Cocone K} (hc : CategoryTheory.Limits.IsColimit c) (lc : CategoryTheory.Limits.Cocone (K.comp CategoryTheory.uliftFunctor.{v, u} )) (x : c.pt) : lc.pt

Given a colimit cocone in Type u and an arbitrary cocone over the diagram lifted to Type (max u v), produce a function from the cocone point of the colimit cocone to the cocone point of the other cocone, that witnesses the colimit cocone also being a colimit in the higher universe.

Equations

• CategoryTheory.Limits.Types.descFun hc lc x = ⋯.choose

theorem CategoryTheory.Limits.Types.descFun_apply_spec {J : Type u_1} [CategoryTheory.Category.{u_2, u_1} J] {K : CategoryTheory.Functor J (Type u)} {c : CategoryTheory.Limits.Cocone K} (hc : CategoryTheory.Limits.IsColimit c) (lc : CategoryTheory.Limits.Cocone (K.comp CategoryTheory.uliftFunctor.{v, u} )) {x : c.pt} {y : lc.pt} : CategoryTheory.Limits.Types.descFun hc lc x = y ↔ x ∈ CategoryTheory.Limits.Types.descSet hc {y}

theorem CategoryTheory.Limits.Types.descFun_spec {J : Type u_1} [CategoryTheory.Category.{u_2, u_1} J] {K : CategoryTheory.Functor J (Type u)} {c : CategoryTheory.Limits.Cocone K} (hc : CategoryTheory.Limits.IsColimit c) (lc : CategoryTheory.Limits.Cocone (K.comp CategoryTheory.uliftFunctor.{v, u} )) (f : c.pt → lc.pt) : f = CategoryTheory.Limits.Types.descFun hc lc ↔ ∀ (j : J), f ∘ c.ι.app j = lc.ι.app j ∘ ULift.up

noncomputable instance CategoryTheory.Limits.Types.instPreservesColimitsOfSizeUliftFunctor : CategoryTheory.Limits.PreservesColimitsOfSize.{w', w, u, max u v, u + 1, max (u + 1) (v + 1)} CategoryTheory.uliftFunctor.{v, u}

The functor uliftFunctor : Type u ⥤ Type (max u v) preserves colimits of arbitrary size.

Equations

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

noncomputable instance CategoryTheory.Limits.Types.instCreatesColimitsOfSizeUliftFunctor : CategoryTheory.CreatesColimitsOfSize.{w, u, u, max u v, u + 1, max (u + 1) (v + 1)} CategoryTheory.uliftFunctor.{v, u}

The functor uliftFunctor : Type u ⥤ Type (max u v) creates u-small colimits.

Equations

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