Limits in the category of types.

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

def CategoryTheory.Limits.Types.coneOfSection {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} {s : (j : J) → F.obj j} (hs : s ∈ F.sections) : Cone F

Given a section of a functor F into Type*, construct a cone over F with PUnit as the cone point.

Equations

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

def CategoryTheory.Limits.Types.sectionOfCone {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} (c : Cone F) (x : c.pt) : ↑F.sections

Given a cone over a functor F into Type* and an element in the cone point, construct a section of F.

Equations

• CategoryTheory.Limits.Types.sectionOfCone c x = ⟨fun (j : J) => c.π.app j x, ⋯⟩

theorem CategoryTheory.Limits.Types.isLimit_iff {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} (c : Cone F) : Nonempty (IsLimit c) ↔ ∀ s ∈ F.sections, ∃! x : c.pt, ∀ (j : J), c.π.app j x = s j

theorem CategoryTheory.Limits.Types.isLimit_iff_bijective_sectionOfCone {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} (c : Cone F) : Nonempty (IsLimit c) ↔ Function.Bijective (sectionOfCone c)

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

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

Equations

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

@[simp]

theorem CategoryTheory.Limits.Types.isLimitEquivSections_apply {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} {c : Cone F} (t : IsLimit c) (j : J) (x : c.pt) : ↑((isLimitEquivSections t) x) j = c.π.app j x

@[simp]

theorem CategoryTheory.Limits.Types.isLimitEquivSections_symm_apply {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} {c : Cone F} (t : IsLimit c) (x : ↑F.sections) (j : J) : c.π.app j ((isLimitEquivSections t).symm x) = ↑x j

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

The first, in the CategoryTheory.Limits.Types.Small namespace, assumes Small.{u} J and constructs J-indexed limits in Type u.

The second, in the CategoryTheory.Limits.Types.TypeMax namespace constructs limits for functors F : J ⥤ Type max 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.

noncomputable def CategoryTheory.Limits.Types.Small.limitCone {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [Small.{u, max u v} ↑F.sections] : Cone F

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

Equations

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

@[simp]

theorem CategoryTheory.Limits.Types.Small.limitCone_π_app {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [Small.{u, max u v} ↑F.sections] (j : J) (u : ((Functor.const J).obj (Shrink.{u, max u v} ↑F.sections)).obj j) : (limitCone F).π.app j u = ↑((equivShrink ↑F.sections).symm u) j

@[simp]

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

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

theorem CategoryTheory.Limits.Types.Small.limitCone_pt_ext_iff {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} [Small.{u, max u v} ↑F.sections] {x y : (limitCone F).pt} : x = y ↔ (equivShrink ↑F.sections).symm x = (equivShrink ↑F.sections).symm y

noncomputable def CategoryTheory.Limits.Types.Small.limitConeIsLimit {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [Small.{u, max u v} ↑F.sections] : IsLimit (limitCone F)

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

Equations

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

@[simp]

theorem CategoryTheory.Limits.Types.Small.limitConeIsLimit_lift {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [Small.{u, max u v} ↑F.sections] (s : Cone F) (v : s.pt) : (limitConeIsLimit F).lift s v = (equivShrink ↑F.sections) ⟨fun (j : J) => s.π.app j v, ⋯⟩

theorem CategoryTheory.Limits.Types.hasLimit_iff_small_sections {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) : HasLimit F ↔ Small.{u, max u v} ↑F.sections

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

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

Equations

• CategoryTheory.Limits.Types.limitCone F = { pt := ↑F.sections, π := { app := fun (j : J) (u : ((CategoryTheory.Functor.const J).obj ↑F.sections).obj j) => ↑u j, naturality := ⋯ } }

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.Types.limitCone_π_app {J : Type v} [Category.{w, v} J] (F : Functor J (Type (max v u))) (j : J) (u : ((Functor.const J).obj ↑F.sections).obj j) : (limitCone F).π.app j u = ↑u j

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

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

Equations

• CategoryTheory.Limits.Types.limitConeIsLimit F = { lift := fun (s : CategoryTheory.Limits.Cone F) (v : s.pt) => ⟨fun (j : J) => s.π.app j v, ⋯⟩, fac := ⋯, uniq := ⋯ }

@[simp]

theorem CategoryTheory.Limits.Types.limitConeIsLimit_lift_coe {J : Type v} [Category.{w, v} J] (F : Functor J (Type (max v u))) (s : Cone F) (v : s.pt) (j : J) : ↑((limitConeIsLimit F).lift s v) j = s.π.app j v

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.

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

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

@[instance 1300]

instance CategoryTheory.Limits.Types.hasLimitsOfSize [UnivLE.{v, u}] : HasLimitsOfSize.{w, 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.

Stacks Tag 002U

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

The equivalence between the abstract limit of F in Type max v u and the "concrete" definition as the sections of F.

Equations

• CategoryTheory.Limits.Types.limitEquivSections F = CategoryTheory.Limits.Types.isLimitEquivSections (CategoryTheory.Limits.limit.isLimit F)

@[simp]

theorem CategoryTheory.Limits.Types.limitEquivSections_apply {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [HasLimit F] (x : limit F) (j : J) : ↑((limitEquivSections F) x) j = limit.π F j x

@[simp]

theorem CategoryTheory.Limits.Types.limitEquivSections_symm_apply {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [HasLimit F] (x : ↑F.sections) (j : J) : limit.π F j ((limitEquivSections F).symm x) = ↑x j

noncomputable def CategoryTheory.Limits.Types.limNatIsoSectionsFunctor {J : Type v} [Category.{w, v} J] : lim ≅ Functor.sectionsFunctor J

The limit of a functor F : J ⥤ Type _ is naturally isomorphic to F.sections.

Equations

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

noncomputable def CategoryTheory.Limits.Types.Limit.mk {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [HasLimit F] (x : (j : J) → F.obj j) (h : ∀ (j j' : J) (f : j ⟶ j'), F.map f (x j) = x j') : 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'.

Equations

• CategoryTheory.Limits.Types.Limit.mk F x h = (CategoryTheory.Limits.Types.limitEquivSections F).symm ⟨x, ⋯⟩

@[simp]

theorem CategoryTheory.Limits.Types.Limit.π_mk {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [HasLimit F] (x : (j : J) → F.obj j) (h : ∀ (j j' : J) (f : j ⟶ j'), F.map f (x j) = x j') (j : J) : limit.π F j (mk F x h) = x j

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

theorem CategoryTheory.Limits.Types.limit_ext_iff {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} [HasLimit F] {x y : limit F} : x = y ↔ ∀ (j : J), limit.π F j x = limit.π F j y

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

theorem CategoryTheory.Limits.Types.limit_ext'_iff {J : Type v} [Category.{w, v} J] {F : Functor J (Type v)} {x y : limit F} : x = y ↔ ∀ (j : J), limit.π F j x = limit.π F j y

theorem CategoryTheory.Limits.Types.limit_ext_iff' {J : Type v} [Category.{w, v} J] (F : Functor J (Type v)) (x y : limit F) : x = y ↔ ∀ (j : J), limit.π F j x = limit.π F j y

theorem CategoryTheory.Limits.Types.Limit.w_apply {J : Type v} [Category.{w, v} J] {F : Functor J (Type u)} [HasLimit F] {j j' : J} {x : limit F} (f : j ⟶ j') : F.map f (limit.π F j x) = limit.π F j' x

theorem CategoryTheory.Limits.Types.Limit.lift_π_apply {J : Type v} [Category.{w, v} J] (F : Functor J (Type u)) [HasLimit F] (s : Cone F) (j : J) (x : s.pt) : limit.π F j (limit.lift F s x) = s.π.app j x

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

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.Types.Limit.lift_π_apply' {J : Type v} [Category.{w, v} J] (F : Functor J (Type v)) (s : Cone F) (j : J) (x : s.pt) : limit.π F j (limit.lift F s x) = s.π.app j x

@[simp]

theorem CategoryTheory.Limits.Types.Limit.map_π_apply' {J : Type v} [Category.{w, v} J] {F G : Functor J (Type v)} (α : F ⟶ G) (j : J) (x : limit F) : limit.π G j (limMap α x) = α.app j (limit.π F j x)

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