Limits in the category of types.

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

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

Finally, we give the natural isomorphism between cones on F with cone point X and the type lim Hom(X, F·), and similarly the natural isomorphism between cocones on F with cocone point X and the type lim Hom(F·, X).

def CategoryTheory.Limits.Types.coneOfSection {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)} {s : (j : J) → F.obj j} (hs : s ∈ F.sections) : CategoryTheory.Limits.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} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)} (c : CategoryTheory.Limits.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} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)} (c : CategoryTheory.Limits.Cone F) : Nonempty (CategoryTheory.Limits.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} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)} (c : CategoryTheory.Limits.Cone F) : Nonempty (CategoryTheory.Limits.IsLimit c) ↔ Function.Bijective (CategoryTheory.Limits.Types.sectionOfCone c)

noncomputable def CategoryTheory.Limits.Types.isLimitEquivSections {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)} {c : CategoryTheory.Limits.Cone F} (t : CategoryTheory.Limits.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} [CategoryTheory.Category.{w, v} J] {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 = c.π.app j x

@[simp]

theorem CategoryTheory.Limits.Types.isLimitEquivSections_symm_apply {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)} {c : CategoryTheory.Limits.Cone F} (t : CategoryTheory.Limits.IsLimit c) (x : ↑F.sections) (j : J) : c.π.app j ((CategoryTheory.Limits.Types.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 ⥤ 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.Small.limitCone_pt {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [Small.{u, max u v} ↑F.sections] : (CategoryTheory.Limits.Types.Small.limitCone F).pt = Shrink.{u, max u v} ↑F.sections

@[simp]

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

noncomputable def CategoryTheory.Limits.Types.Small.limitCone {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [Small.{u, max u v} ↑F.sections] : CategoryTheory.Limits.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.

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

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

@[simp]

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

noncomputable def CategoryTheory.Limits.Types.Small.limitConeIsLimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [Small.{u, max u v} ↑F.sections] : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Types.Small.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.

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

@[simp]

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

@[simp]

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

noncomputable def CategoryTheory.Limits.Types.limitCone {J : Type v} [CategoryTheory.Category.{w, v} 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

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.limitConeIsLimit_lift_coe {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J TypeMax) (s : CategoryTheory.Limits.Cone F) (v : s.pt) (j : J) : ↑((CategoryTheory.Limits.Types.limitConeIsLimit F).lift s v) j = s.π.app j v

noncomputable def CategoryTheory.Limits.Types.limitConeIsLimit {J : Type v} [CategoryTheory.Category.{w, v} 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

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 := ⋯ }

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} [CategoryTheory.Category.{w, v} J] [Small.{u, v} J] (F : CategoryTheory.Functor J (Type u)) : CategoryTheory.Limits.HasLimit F

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[instance 1300]

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

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

Equations

• ⋯ = ⋯

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

The equivalence between the abstract limit of F in TypeMax.{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} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [CategoryTheory.Limits.HasLimit F] (x : CategoryTheory.Limits.limit F) (j : J) : ↑((CategoryTheory.Limits.Types.limitEquivSections F) x) j = CategoryTheory.Limits.limit.π F j x

@[simp]

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.Types.Limit.map_π_apply' {J : Type v} [CategoryTheory.Category.{w, v} 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.π G j (CategoryTheory.Limits.limMap α x) = α.app j (CategoryTheory.Limits.limit.π F j x)

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

def CategoryTheory.Limits.Types.Quot.Rel {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.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} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.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} [CategoryTheory.Category.{w, v} J] [Small.{u, v} J] (F : CategoryTheory.Functor J (Type u)) : Small.{u, max u v} (CategoryTheory.Limits.Types.Quot F)

Equations

• ⋯ = ⋯

def CategoryTheory.Limits.Types.Quot.ι {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) (j : J) : F.obj j → CategoryTheory.Limits.Types.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} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)} (x : CategoryTheory.Limits.Types.Quot F) : ∃ (j : J) (y : F.obj j), x = CategoryTheory.Limits.Types.Quot.ι F j y

def CategoryTheory.Limits.Types.Quot.desc {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)} (c : CategoryTheory.Limits.Cocone F) : CategoryTheory.Limits.Types.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} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)} (c : CategoryTheory.Limits.Cocone F) (j : J) (x : F.obj j) : CategoryTheory.Limits.Types.Quot.desc c (CategoryTheory.Limits.Types.Quot.ι F j x) = c.ι.app j x

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Limits.Types.toCocone {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)} {α : Type u} (f : CategoryTheory.Limits.Types.Quot F → α) : CategoryTheory.Limits.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 := ⋯ } }

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

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

@[simp]

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

@[simp]

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

noncomputable def CategoryTheory.Limits.Types.colimitCocone {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [Small.{u, max u v} (CategoryTheory.Limits.Types.Quot F)] : CategoryTheory.Limits.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.Quot.desc_colimitCocone {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [Small.{u, max u v} (CategoryTheory.Limits.Types.Quot F)] : CategoryTheory.Limits.Types.Quot.desc (CategoryTheory.Limits.Types.colimitCocone F) = ⇑(equivShrink (CategoryTheory.Limits.Types.Quot F))

noncomputable def CategoryTheory.Limits.Types.colimitCoconeIsColimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [Small.{u, max u v} (CategoryTheory.Limits.Types.Quot F)] : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Types.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} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) : CategoryTheory.Limits.HasColimit F ↔ Small.{u, max u v} (CategoryTheory.Limits.Types.Quot F)

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

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

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

@[instance 1300]

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

The category of types has all colimits.

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

Equations

• ⋯ = ⋯

@[simp]

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

@[simp]

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

def CategoryTheory.Limits.Types.TypeMax.colimitCocone {J : Type v} [CategoryTheory.Category.{w, v} 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

Equations

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

def CategoryTheory.Limits.Types.TypeMax.colimitCoconeIsColimit {J : Type v} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J TypeMax) : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Types.TypeMax.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} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) [CategoryTheory.Limits.HasColimit F] : 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.

Equations

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

@[simp]

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

@[simp]

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.Types.Colimit.ι_map_apply' {J : Type v} [CategoryTheory.Category.{w, v} 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.ι F j x) = CategoryTheory.Limits.colimit.ι G j (α.app j x)

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

theorem CategoryTheory.Limits.Types.colimit_sound' {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)} [CategoryTheory.Limits.HasColimit F] {j : 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') : CategoryTheory.Limits.colimit.ι F j x = CategoryTheory.Limits.colimit.ι F j' x'

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

theorem CategoryTheory.Limits.Types.jointly_surjective_of_isColimit {J : Type v} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)} {t : CategoryTheory.Limits.Cocone F} (h : CategoryTheory.Limits.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} [CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u)) {t : CategoryTheory.Limits.Cocone F} (h : CategoryTheory.Limits.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} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)} [CategoryTheory.Limits.HasColimit F] (x : CategoryTheory.Limits.colimit F) : ∃ (j : J) (y : F.obj j), CategoryTheory.Limits.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} [CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)} [CategoryTheory.Limits.HasColimit F] : Nonempty (CategoryTheory.Limits.colimit F) → Nonempty J

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

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

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

Equations

• CategoryTheory.Limits.Types.Image f = ↑(Set.range f)

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

Equations

• CategoryTheory.Limits.Types.instInhabitedImage f = { default := ⟨f default, ⋯⟩ }

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

the inclusion of Image f into the target

Equations

• CategoryTheory.Limits.Types.Image.ι f = Subtype.val

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

Equations

• ⋯ = ⋯

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

Equations

• CategoryTheory.Limits.Types.Image.lift F' x = F'.e ↑(Classical.indefiniteDescription (fun (x_1 : α) => f x_1 = ↑x) ⋯)

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.

Equations

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

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.

Equations

• CategoryTheory.Limits.Types.isImage f = { lift := CategoryTheory.Limits.Types.Image.lift, lift_fac := ⋯ }

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

Equations

• ⋯ = ⋯

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

Equations

• CategoryTheory.Limits.Types.instHasImagesType = ⋯

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

Equations

• CategoryTheory.Limits.Types.instHasImageMapsType = ⋯

theorem CategoryTheory.Limits.Types.surjective_π_app_zero_of_surjective_map_aux {F : CategoryTheory.Functor ℕᵒᵖ (Type u)} (hF : ∀ (n : ℕ), Function.Surjective (F.map (CategoryTheory.homOfLE ⋯).op)) : Function.Surjective ((CategoryTheory.Limits.Types.limitCone F).π.app (Opposite.op 0))

Auxiliary lemma. Use limit_of_surjections_surjective instead.

theorem CategoryTheory.Limits.Types.surjective_π_app_zero_of_surjective_map {F : CategoryTheory.Functor ℕᵒᵖ (Type u)} {c : CategoryTheory.Limits.Cone F} (hc : CategoryTheory.Limits.IsLimit c) (hF : ∀ (n : ℕ), Function.Surjective (F.map (CategoryTheory.homOfLE ⋯).op)) : Function.Surjective (c.π.app (Opposite.op 0))

Given surjections ⋯ ⟶ Xₙ₊₁ ⟶ Xₙ ⟶ ⋯ ⟶ X₀, the projection map lim Xₙ ⟶ X₀ is surjective.

@[simp]

theorem CategoryTheory.Limits.compCoyonedaSectionsEquiv_symm_apply_coe {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] (F : CategoryTheory.Functor J C) (X : C) (τ : (CategoryTheory.Functor.const J).obj X✝ ⟶ F) (X : J) : ↑((CategoryTheory.Limits.compCoyonedaSectionsEquiv F X✝).symm τ) X = τ.app X

@[simp]

theorem CategoryTheory.Limits.compCoyonedaSectionsEquiv_apply_app {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] (F : CategoryTheory.Functor J C) (X : C) (s : ↑(F.comp (CategoryTheory.coyoneda.obj (Opposite.op X))).sections) (j : J) : ((CategoryTheory.Limits.compCoyonedaSectionsEquiv F X) s).app j = ↑s j

def CategoryTheory.Limits.compCoyonedaSectionsEquiv {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] (F : CategoryTheory.Functor J C) (X : C) : ↑(F.comp (CategoryTheory.coyoneda.obj (Opposite.op X))).sections ≃ ((CategoryTheory.Functor.const J).obj X ⟶ F)

Sections of F ⋙ coyoneda.obj (op X) identify to natural transformations (const J).obj X ⟶ F.

Equations

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

@[simp]

theorem CategoryTheory.Limits.opCompYonedaSectionsEquiv_symm_apply_coe {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] (F : CategoryTheory.Functor J C) (X : C) (τ : F ⟶ (CategoryTheory.Functor.const J).obj X) (j : Jᵒᵖ) : ↑((CategoryTheory.Limits.opCompYonedaSectionsEquiv F X).symm τ) j = τ.app (Opposite.unop j)

@[simp]

theorem CategoryTheory.Limits.opCompYonedaSectionsEquiv_apply_app {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] (F : CategoryTheory.Functor J C) (X : C) (s : ↑(F.op.comp (CategoryTheory.yoneda.obj X)).sections) (j : J) : ((CategoryTheory.Limits.opCompYonedaSectionsEquiv F X) s).app j = ↑s (Opposite.op j)

def CategoryTheory.Limits.opCompYonedaSectionsEquiv {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] (F : CategoryTheory.Functor J C) (X : C) : ↑(F.op.comp (CategoryTheory.yoneda.obj X)).sections ≃ (F ⟶ (CategoryTheory.Functor.const J).obj X)

Sections of F.op ⋙ yoneda.obj X identify to natural transformations F ⟶ (const J).obj X.

Equations

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

@[simp]

theorem CategoryTheory.Limits.compYonedaSectionsEquiv_symm_apply_coe {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] (F : CategoryTheory.Functor J Cᵒᵖ) (X : C) (τ : (CategoryTheory.Functor.const J).obj (Opposite.op X) ⟶ F) (j : J) : ↑((CategoryTheory.Limits.compYonedaSectionsEquiv F X).symm τ) j = (τ.app j).unop

@[simp]

theorem CategoryTheory.Limits.compYonedaSectionsEquiv_apply_app {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] (F : CategoryTheory.Functor J Cᵒᵖ) (X : C) (s : ↑(F.comp (CategoryTheory.yoneda.obj X)).sections) (j : J) : ((CategoryTheory.Limits.compYonedaSectionsEquiv F X) s).app j = Quiver.Hom.op (↑s j)

def CategoryTheory.Limits.compYonedaSectionsEquiv {J : Type u_1} {C : Type u_2} [CategoryTheory.Category.{u_3, u_1} J] [CategoryTheory.Category.{u_4, u_2} C] (F : CategoryTheory.Functor J Cᵒᵖ) (X : C) : ↑(F.comp (CategoryTheory.yoneda.obj X)).sections ≃ ((CategoryTheory.Functor.const J).obj (Opposite.op X) ⟶ F)

Sections of F ⋙ yoneda.obj X identify to natural transformations (const J).obj X ⟶ F.

Equations

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

@[simp]

theorem CategoryTheory.Limits.limitCompCoyonedaIsoCone_hom_app {J : Type v} [CategoryTheory.SmallCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J C) (X : C) : ∀ (a : CategoryTheory.Limits.limit (F.comp (CategoryTheory.coyoneda.obj (Opposite.op X)))) (j : J), ((CategoryTheory.Limits.limitCompCoyonedaIsoCone F X).hom a).app j = CategoryTheory.Limits.limit.π (F.comp (CategoryTheory.coyoneda.obj (Opposite.op X))) j a

@[simp]

theorem CategoryTheory.Limits.limitCompCoyonedaIsoCone_inv {J : Type v} [CategoryTheory.SmallCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J C) (X : C) : ∀ (a : (CategoryTheory.Functor.const J).obj X ⟶ F), (CategoryTheory.Limits.limitCompCoyonedaIsoCone F X).inv a = (CategoryTheory.Limits.Types.limitEquivSections (F.comp (CategoryTheory.coyoneda.obj (Opposite.op X)))).symm ((CategoryTheory.Limits.compCoyonedaSectionsEquiv F X).symm a)

noncomputable def CategoryTheory.Limits.limitCompCoyonedaIsoCone {J : Type v} [CategoryTheory.SmallCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J C) (X : C) : CategoryTheory.Limits.limit (F.comp (CategoryTheory.coyoneda.obj (Opposite.op X))) ≅ (CategoryTheory.Functor.const J).obj X ⟶ F

A cone on F with cone point X is the same as an element of lim Hom(X, F·).

Equations

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

@[simp]

theorem CategoryTheory.Limits.coyonedaCompLimIsoCones_inv_app {J : Type v} [CategoryTheory.SmallCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J C) (X : Cᵒᵖ) : ∀ (a : F.cones.obj X), (CategoryTheory.Limits.coyonedaCompLimIsoCones F).inv.app X a = (CategoryTheory.Limits.Types.limitEquivSections (F.comp (CategoryTheory.coyoneda.obj X))).symm ((CategoryTheory.Limits.compCoyonedaSectionsEquiv F (Opposite.unop X)).symm a)

@[simp]

theorem CategoryTheory.Limits.coyonedaCompLimIsoCones_hom_app_app {J : Type v} [CategoryTheory.SmallCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J C) (X : Cᵒᵖ) : ∀ (a : (CategoryTheory.coyoneda.comp (((CategoryTheory.whiskeringLeft J C (Type v)).obj F).comp CategoryTheory.Limits.lim)).obj X) (j : J), ((CategoryTheory.Limits.coyonedaCompLimIsoCones F).hom.app X a).app j = CategoryTheory.Limits.limit.π (F.comp (CategoryTheory.coyoneda.obj X)) j a

noncomputable def CategoryTheory.Limits.coyonedaCompLimIsoCones {J : Type v} [CategoryTheory.SmallCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J C) : CategoryTheory.coyoneda.comp (((CategoryTheory.whiskeringLeft J C (Type v)).obj F).comp CategoryTheory.Limits.lim) ≅ F.cones

A cone on F with cone point X is the same as an element of lim Hom(X, F·), naturally in X.

Equations

• CategoryTheory.Limits.coyonedaCompLimIsoCones F = CategoryTheory.NatIso.ofComponents (fun (X : Cᵒᵖ) => CategoryTheory.Limits.limitCompCoyonedaIsoCone F (Opposite.unop X)) ⋯

@[simp]

theorem CategoryTheory.Limits.whiskeringLimYonedaIsoCones_inv_app_app (J : Type v) [CategoryTheory.SmallCategory J] (C : Type u) [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor J C) (X : Cᵒᵖ) : ∀ (a : X✝.cones.obj X), ((CategoryTheory.Limits.whiskeringLimYonedaIsoCones J C).inv.app X✝).app X a = (CategoryTheory.Limits.Types.limitEquivSections (X✝.comp (CategoryTheory.coyoneda.obj X))).symm ((CategoryTheory.Limits.compCoyonedaSectionsEquiv X✝ (Opposite.unop X)).symm a)

@[simp]

theorem CategoryTheory.Limits.whiskeringLimYonedaIsoCones_hom_app_app_app (J : Type v) [CategoryTheory.SmallCategory J] (C : Type u) [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor J C) (X : Cᵒᵖ) : ∀ (a : (CategoryTheory.coyoneda.comp (((CategoryTheory.whiskeringLeft J C (Type v)).obj X✝).comp CategoryTheory.Limits.lim)).obj X) (j : J), (((CategoryTheory.Limits.whiskeringLimYonedaIsoCones J C).hom.app X✝).app X a).app j = CategoryTheory.Limits.limit.π (X✝.comp (CategoryTheory.coyoneda.obj X)) j a

noncomputable def CategoryTheory.Limits.whiskeringLimYonedaIsoCones (J : Type v) [CategoryTheory.SmallCategory J] (C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.whiskeringLeft J C (Type v)).comp (((CategoryTheory.whiskeringRight (CategoryTheory.Functor C (Type v)) (CategoryTheory.Functor J (Type v)) (Type v)).obj CategoryTheory.Limits.lim).comp ((CategoryTheory.whiskeringLeft Cᵒᵖ (CategoryTheory.Functor C (Type v)) (Type v)).obj CategoryTheory.coyoneda)) ≅ CategoryTheory.cones J C

A cone on F with cone point X is the same as an element of lim Hom(X, F·), naturally in F and X.

Equations

• CategoryTheory.Limits.whiskeringLimYonedaIsoCones J C = CategoryTheory.NatIso.ofComponents CategoryTheory.Limits.coyonedaCompLimIsoCones ⋯

@[simp]

theorem CategoryTheory.Limits.limitCompYonedaIsoCocone_inv {J : Type v} [CategoryTheory.SmallCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J C) (X : C) : ∀ (a : F ⟶ (CategoryTheory.Functor.const J).obj X), (CategoryTheory.Limits.limitCompYonedaIsoCocone F X).inv a = (CategoryTheory.Limits.Types.limitEquivSections (F.op.comp (CategoryTheory.yoneda.obj X))).symm ((CategoryTheory.Limits.opCompYonedaSectionsEquiv F X).symm a)

@[simp]

theorem CategoryTheory.Limits.limitCompYonedaIsoCocone_hom_app {J : Type v} [CategoryTheory.SmallCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J C) (X : C) : ∀ (a : CategoryTheory.Limits.limit (F.op.comp (CategoryTheory.yoneda.obj X))) (j : J), ((CategoryTheory.Limits.limitCompYonedaIsoCocone F X).hom a).app j = CategoryTheory.Limits.limit.π (F.op.comp (CategoryTheory.yoneda.obj X)) (Opposite.op j) a

noncomputable def CategoryTheory.Limits.limitCompYonedaIsoCocone {J : Type v} [CategoryTheory.SmallCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J C) (X : C) : CategoryTheory.Limits.limit (F.op.comp (CategoryTheory.yoneda.obj X)) ≅ F ⟶ (CategoryTheory.Functor.const J).obj X

A cocone on F with cocone point X is the same as an element of lim Hom(F·, X).

Equations

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

@[simp]

theorem CategoryTheory.Limits.yonedaCompLimIsoCocones_inv_app {J : Type v} [CategoryTheory.SmallCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J C) (X : C) : ∀ (a : F.cocones.obj X), (CategoryTheory.Limits.yonedaCompLimIsoCocones F).inv.app X a = (CategoryTheory.Limits.Types.limitEquivSections (F.op.comp (CategoryTheory.yoneda.obj X))).symm ((CategoryTheory.Limits.opCompYonedaSectionsEquiv F X).symm a)

@[simp]

theorem CategoryTheory.Limits.yonedaCompLimIsoCocones_hom_app_app {J : Type v} [CategoryTheory.SmallCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J C) (X : C) : ∀ (a : (CategoryTheory.yoneda.comp (((CategoryTheory.whiskeringLeft Jᵒᵖ Cᵒᵖ (Type v)).obj F.op).comp CategoryTheory.Limits.lim)).obj X) (j : J), ((CategoryTheory.Limits.yonedaCompLimIsoCocones F).hom.app X a).app j = CategoryTheory.Limits.limit.π (F.op.comp (CategoryTheory.yoneda.obj X)) (Opposite.op j) a

noncomputable def CategoryTheory.Limits.yonedaCompLimIsoCocones {J : Type v} [CategoryTheory.SmallCategory J] {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor J C) : CategoryTheory.yoneda.comp (((CategoryTheory.whiskeringLeft Jᵒᵖ Cᵒᵖ (Type v)).obj F.op).comp CategoryTheory.Limits.lim) ≅ F.cocones

A cocone on F with cocone point X is the same as an element of lim Hom(F·, X), naturally in X.

Equations

• CategoryTheory.Limits.yonedaCompLimIsoCocones F = CategoryTheory.NatIso.ofComponents (CategoryTheory.Limits.limitCompYonedaIsoCocone F) ⋯

@[simp]

theorem CategoryTheory.Limits.opHomCompWhiskeringLimYonedaIsoCocones_hom_app_app_app (J : Type v) [CategoryTheory.SmallCategory J] (C : Type u) [CategoryTheory.Category.{v, u} C] (X : (CategoryTheory.Functor J C)ᵒᵖ) (X : C) : ∀ (a : (CategoryTheory.yoneda.comp (((CategoryTheory.whiskeringLeft Jᵒᵖ Cᵒᵖ (Type v)).obj (Opposite.unop X✝).op).comp CategoryTheory.Limits.lim)).obj X) (j : J), (((CategoryTheory.Limits.opHomCompWhiskeringLimYonedaIsoCocones J C).hom.app X✝).app X a).app j = CategoryTheory.Limits.limit.π ((Opposite.unop X✝).op.comp (CategoryTheory.yoneda.obj X)) (Opposite.op j) a

@[simp]

theorem CategoryTheory.Limits.opHomCompWhiskeringLimYonedaIsoCocones_inv_app_app (J : Type v) [CategoryTheory.SmallCategory J] (C : Type u) [CategoryTheory.Category.{v, u} C] (X : (CategoryTheory.Functor J C)ᵒᵖ) (X : C) : ∀ (a : (Opposite.unop X✝).cocones.obj X), ((CategoryTheory.Limits.opHomCompWhiskeringLimYonedaIsoCocones J C).inv.app X✝).app X a = (CategoryTheory.Limits.Types.limitEquivSections ((Opposite.unop X✝).op.comp (CategoryTheory.yoneda.obj X))).symm ((CategoryTheory.Limits.opCompYonedaSectionsEquiv (Opposite.unop X✝) X).symm a)

noncomputable def CategoryTheory.Limits.opHomCompWhiskeringLimYonedaIsoCocones (J : Type v) [CategoryTheory.SmallCategory J] (C : Type u) [CategoryTheory.Category.{v, u} C] : (CategoryTheory.Functor.opHom J C).comp ((CategoryTheory.whiskeringLeft Jᵒᵖ Cᵒᵖ (Type v)).comp (((CategoryTheory.whiskeringRight (CategoryTheory.Functor Cᵒᵖ (Type v)) (CategoryTheory.Functor Jᵒᵖ (Type v)) (Type v)).obj CategoryTheory.Limits.lim).comp ((CategoryTheory.whiskeringLeft C (CategoryTheory.Functor Cᵒᵖ (Type v)) (Type v)).obj CategoryTheory.yoneda))) ≅ CategoryTheory.cocones J C

A cocone on F with cocone point X is the same as an element of lim Hom(F·, X), naturally in F and X.

Equations

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