# 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} {F : } {s : (j : J) → F.obj j} (hs : s F.sections) :

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.
Instances For
def CategoryTheory.Limits.Types.sectionOfCone {J : Type v} {F : } (c : ) (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
• = fun (j : J) => c.app j x,
Instances For
theorem CategoryTheory.Limits.Types.isLimit_iff {J : Type v} {F : } (c : ) :
sF.sections, ∃! x : c.pt, ∀ (j : J), c.app j x = s j
noncomputable def CategoryTheory.Limits.Types.isLimitEquivSections {J : Type v} {F : } {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.
Instances For
@[simp]
theorem CategoryTheory.Limits.Types.isLimitEquivSections_apply {J : Type v} {F : } {c : } (j : J) (x : c.pt) :
= c.app j x
@[simp]
theorem CategoryTheory.Limits.Types.isLimitEquivSections_symm_apply {J : Type v} {F : } {c : } (x : F.sections) (j : J) :
c.app j () = 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_π_app {J : Type v} (F : ) [Small.{u, max u v} F.sections] (j : J) (u : (.obj (Shrink.{u, max u v} F.sections)).obj j) :
j u = ((equivShrink F.sections).symm u) j
@[simp]
theorem CategoryTheory.Limits.Types.Small.limitCone_pt {J : Type v} (F : ) [Small.{u, max u v} F.sections] :
= Shrink.{u, max u v} F.sections
noncomputable def CategoryTheory.Limits.Types.Small.limitCone {J : Type v} (F : ) [Small.{u, max u v} F.sections] :

(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.
Instances For
theorem CategoryTheory.Limits.Types.Small.limitCone_pt_ext {J : Type v} (F : ) [Small.{u, max u v} F.sections] {x : } {y : } (w : (equivShrink F.sections).symm x = (equivShrink F.sections).symm y) :
x = y
@[simp]
theorem CategoryTheory.Limits.Types.Small.limitConeIsLimit_lift {J : Type v} (F : ) [Small.{u, max u v} F.sections] (s : ) (v : s.pt) :
= (equivShrink F.sections) fun (j : J) => s.app j v,
noncomputable def CategoryTheory.Limits.Types.Small.limitConeIsLimit {J : Type v} (F : ) [Small.{u, max u v} F.sections] :

(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.
Instances For
@[simp]
theorem CategoryTheory.Limits.Types.limitCone_pt {J : Type v} (F : ) :
= F.sections
@[simp]
theorem CategoryTheory.Limits.Types.limitCone_π_app {J : Type v} (F : ) (j : J) (u : (.obj F.sections).obj j) :
.app j u = u j
noncomputable def CategoryTheory.Limits.Types.limitCone {J : Type v} (F : ) :

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

Equations
• = { pt := F.sections, π := { app := fun (j : J) (u : (.obj F.sections).obj j) => u j, naturality := } }
Instances For
@[simp]
theorem CategoryTheory.Limits.Types.limitConeIsLimit_lift_coe {J : Type v} (F : ) (s : ) (v : s.pt) (j : J) :
( s v) j = s.app j v
noncomputable def CategoryTheory.Limits.Types.limitConeIsLimit {J : Type v} (F : ) :

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

Equations
• = { lift := fun (s : ) (v : s.pt) => fun (j : J) => s.app j v, , fac := , uniq := }
Instances For

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} [] (F : ) :
Equations
• =
Equations
• =
@[instance 1300]

The category of types has all limits.

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

See .

Equations
• =
noncomputable def CategoryTheory.Limits.Types.limitEquivSections {J : Type v} (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
Instances For
@[simp]
theorem CategoryTheory.Limits.Types.limitEquivSections_apply {J : Type v} (F : ) (x : ) (j : J) :
@[simp]
theorem CategoryTheory.Limits.Types.limitEquivSections_symm_apply {J : Type v} (F : ) (x : F.sections) (j : J) :
= x j
noncomputable def CategoryTheory.Limits.Types.Limit.mk {J : Type v} (F : ) (x : (j : J) → F.obj j) (h : ∀ (j j' : J) (f : j j'), F.map f (x j) = x j') :

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
• = x,
Instances For
@[simp]
theorem CategoryTheory.Limits.Types.Limit.π_mk {J : Type v} (F : ) (x : (j : J) → F.obj j) (h : ∀ (j j' : J) (f : j j'), F.map f (x j) = x j') (j : J) :
theorem CategoryTheory.Limits.Types.limit_ext {J : Type v} (F : ) (x : ) (y : ) (w : ∀ (j : J), ) :
x = y
theorem CategoryTheory.Limits.Types.limit_ext' {J : Type v} (F : ) (x : ) (y : ) (w : ∀ (j : J), ) :
x = y
theorem CategoryTheory.Limits.Types.limit_ext_iff {J : Type v} (F : ) (x : ) (y : ) :
x = y ∀ (j : J),
theorem CategoryTheory.Limits.Types.limit_ext_iff' {J : Type v} (F : ) (x : ) (y : ) :
x = y ∀ (j : J),
theorem CategoryTheory.Limits.Types.Limit.w_apply {J : Type v} {F : } {j : J} {j' : J} {x : } (f : j j') :
F.map f () =
theorem CategoryTheory.Limits.Types.Limit.lift_π_apply {J : Type v} (F : ) (s : ) (j : J) (x : s.pt) :
= s.app j x
theorem CategoryTheory.Limits.Types.Limit.map_π_apply {J : Type v} {F : } {G : } (α : F G) (j : J) (x : ) :
= α.app j ()
@[simp]
theorem CategoryTheory.Limits.Types.Limit.w_apply' {J : Type v} {F : } {j : J} {j' : J} {x : } (f : j j') :
F.map f () =
@[simp]
theorem CategoryTheory.Limits.Types.Limit.lift_π_apply' {J : Type v} (F : ) (s : ) (j : J) (x : s.pt) :
= s.app j x
@[simp]
theorem CategoryTheory.Limits.Types.Limit.map_π_apply' {J : Type v} {F : } {G : } (α : F G) (j : J) (x : ) :
= α.app j ()

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

def CategoryTheory.Limits.Types.Quot.Rel {J : Type v} (F : ) :
(j : J) × F.obj j(j : J) × F.obj jProp

The relation defining the quotient type which implements the colimit of a functor F : J ⥤ Type u. See CategoryTheory.Limits.Types.Quot.

Equations
• = ∃ (f : p.fst p'.fst), p'.snd = F.map f p.snd
Instances For
def CategoryTheory.Limits.Types.Quot {J : Type v} (F : ) :
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
Instances For
instance CategoryTheory.Limits.Types.instSmallQuot {J : Type v} [] (F : ) :
Equations
• =
def CategoryTheory.Limits.Types.Quot.ι {J : Type v} (F : ) (j : J) :
F.obj j

Inclusion into the quotient type implementing the colimit.

Equations
Instances For
theorem CategoryTheory.Limits.Types.Quot.jointly_surjective {J : Type v} {F : } :
∃ (j : J) (y : F.obj j),
def CategoryTheory.Limits.Types.Quot.desc {J : Type v} {F : } (c : ) :

(implementation detail) Part of the universal property of the colimit cocone, but without assuming that Quot F lives in the correct universe.

Equations
• = Quot.lift (fun (x : (j : J) × F.obj j) => c.app x.fst x.snd)
Instances For
@[simp]
theorem CategoryTheory.Limits.Types.Quot.ι_desc {J : Type v} {F : } (c : ) (j : J) (x : F.obj j) :
= c.app j x
@[simp]
theorem CategoryTheory.Limits.Types.Quot.map_ι {J : Type v} {F : } {j : J} {j' : J} {f : j j'} (x : F.obj j) :
@[simp]
theorem CategoryTheory.Limits.Types.toCocone_pt {J : Type v} {F : } {α : Type u} (f : ) :
@[simp]
theorem CategoryTheory.Limits.Types.toCocone_ι_app {J : Type v} {F : } {α : Type u} (f : ) (j : J) :
∀ (a : F.obj j), .app j a = () a
def CategoryTheory.Limits.Types.toCocone {J : Type v} {F : } {α : Type u} (f : ) :

(implementation detail) A function Quot F → α induces a cocone on F as long as the universes work out.

Equations
• = { pt := α, ι := { app := fun (j : J) => , naturality := } }
Instances For
theorem CategoryTheory.Limits.Types.Quot.desc_toCocone_desc {J : Type v} {F : } (c : ) {α : Type u} (f : ) (hc : ) :
= f x
@[simp]
theorem CategoryTheory.Limits.Types.colimitCocone_ι_app {J : Type v} (F : ) [] (j : J) (x : F.obj j) :
j x =
@[simp]
noncomputable def CategoryTheory.Limits.Types.colimitCocone {J : Type v} (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.
Instances For
@[simp]
noncomputable def CategoryTheory.Limits.Types.colimitCoconeIsColimit {J : Type v} (F : ) [] :

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

Equations
Instances For
instance CategoryTheory.Limits.Types.hasColimit {J : Type v} [] (F : ) :
Equations
• =
Equations
• =
@[instance 1300]

The category of types has all colimits.

See .

Equations
• =
@[simp]
@[simp]
theorem CategoryTheory.Limits.Types.TypeMax.colimitCocone_ι_app {J : Type v} (F : ) (j : J) (x : F.obj j) :
=

(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.
Instances For

(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.
Instances For
noncomputable def CategoryTheory.Limits.Types.colimitEquivQuot {J : Type v} (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.
Instances For
@[simp]
theorem CategoryTheory.Limits.Types.colimitEquivQuot_symm_apply {J : Type v} (F : ) (j : J) (x : F.obj j) :
() =
@[simp]
theorem CategoryTheory.Limits.Types.colimitEquivQuot_apply {J : Type v} (F : ) (j : J) (x : F.obj j) :
theorem CategoryTheory.Limits.Types.Colimit.w_apply {J : Type v} {F : } {j : J} {j' : J} {x : F.obj j} (f : j j') :
theorem CategoryTheory.Limits.Types.Colimit.ι_desc_apply {J : Type v} (F : ) (s : ) (j : J) (x : F.obj j) :
= s.app j x
theorem CategoryTheory.Limits.Types.Colimit.ι_map_apply {J : Type v} {F : } {G : } (α : F G) (j : J) (x : F.obj j) :
CategoryTheory.Limits.colim.map α () = CategoryTheory.Limits.colimit.ι G j (α.app j x)
@[simp]
theorem CategoryTheory.Limits.Types.Colimit.w_apply' {J : Type v} {F : } {j : J} {j' : J} {x : F.obj j} (f : j j') :
@[simp]
theorem CategoryTheory.Limits.Types.Colimit.ι_desc_apply' {J : Type v} (F : ) (s : ) (j : J) (x : F.obj j) :
= s.app j x
@[simp]
theorem CategoryTheory.Limits.Types.Colimit.ι_map_apply' {J : Type v} {F : } {G : } (α : F G) (j : J) (x : F.obj j) :
CategoryTheory.Limits.colim.map α () = CategoryTheory.Limits.colimit.ι G j (α.app j x)
theorem CategoryTheory.Limits.Types.colimit_sound {J : Type v} {F : } {j : J} {j' : J} {x : F.obj j} {x' : F.obj j'} (f : j j') (w : F.map f x = x') :
theorem CategoryTheory.Limits.Types.colimit_sound' {J : Type v} {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') :
theorem CategoryTheory.Limits.Types.colimit_eq {J : Type v} {F : } {j : J} {j' : J} {x : F.obj j} {x' : F.obj j'} (w : ) :
EqvGen j, x j', x'
theorem CategoryTheory.Limits.Types.jointly_surjective_of_isColimit {J : Type v} {F : } {t : } (x : t.pt) :
∃ (j : J) (y : F.obj j), t.app j y = x
theorem CategoryTheory.Limits.Types.jointly_surjective {J : Type v} (F : ) {t : } (x : t.pt) :
∃ (j : J) (y : F.obj j), t.app j y = x
theorem CategoryTheory.Limits.Types.jointly_surjective' {J : Type v} {F : } :
∃ (j : J) (y : F.obj j),

A variant of jointly_surjective for x : colimit F.

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

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

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

Equations
Instances For
instance CategoryTheory.Limits.Types.instInhabitedImage {α : Type u} {β : Type u} (f : α β) [] :
Equations
• = { default := f default, }
def CategoryTheory.Limits.Types.Image.ι {α : Type u} {β : Type u} (f : α β) :

the inclusion of Image f into the target

Equations
• = Subtype.val
Instances For
instance CategoryTheory.Limits.Types.instMonoImageι {α : Type u} {β : Type u} (f : α β) :
Equations
• =
noncomputable def CategoryTheory.Limits.Types.Image.lift {α : Type u} {β : Type u} {f : α β} :

the universal property for the image factorisation

Equations
Instances For
theorem CategoryTheory.Limits.Types.Image.lift_fac {α : Type u} {β : Type u} {f : α β} :
def CategoryTheory.Limits.Types.monoFactorisation {α : Type u} {β : Type u} (f : α β) :

the factorisation of any morphism in Type through a mono.

Equations
• One or more equations did not get rendered due to their size.
Instances For
noncomputable def CategoryTheory.Limits.Types.isImage {α : Type u} {β : Type u} (f : α β) :

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

Equations
• = { lift := CategoryTheory.Limits.Types.Image.lift, lift_fac := }
Instances For
instance CategoryTheory.Limits.Types.instHasImage {α : Type u} {β : Type u} (f : α β) :
Equations
• =
@[simp]
theorem CategoryTheory.Limits.compCoyonedaSectionsEquiv_symm_apply_coe {J : Type u_1} {C : Type u_2} [] [] (F : ) (X : C) (τ : .obj X✝ F) (X : J) :
(.symm τ) X = τ.app X
@[simp]
theorem CategoryTheory.Limits.compCoyonedaSectionsEquiv_apply_app {J : Type u_1} {C : Type u_2} [] [] (F : ) (X : C) (s : (F.comp (CategoryTheory.coyoneda.obj { unop := X })).sections) (j : J) :
.app j = s j
def CategoryTheory.Limits.compCoyonedaSectionsEquiv {J : Type u_1} {C : Type u_2} [] [] (F : ) (X : C) :
(F.comp (CategoryTheory.coyoneda.obj { unop := X })).sections (.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.
Instances For
@[simp]
theorem CategoryTheory.Limits.opCompYonedaSectionsEquiv_apply_app {J : Type u_1} {C : Type u_2} [] [] (F : ) (X : C) (s : (F.op.comp (CategoryTheory.yoneda.obj X)).sections) (j : J) :
.app j = s { unop := j }
@[simp]
theorem CategoryTheory.Limits.opCompYonedaSectionsEquiv_symm_apply_coe {J : Type u_1} {C : Type u_2} [] [] (F : ) (X : C) (τ : F .obj X) (j : Jᵒᵖ) :
( τ) j = τ.app j.unop
def CategoryTheory.Limits.opCompYonedaSectionsEquiv {J : Type u_1} {C : Type u_2} [] [] (F : ) (X : C) :
(F.op.comp (CategoryTheory.yoneda.obj X)).sections (F .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.
Instances For
@[simp]
theorem CategoryTheory.Limits.compYonedaSectionsEquiv_apply_app {J : Type u_1} {C : Type u_2} [] [] (F : ) (X : C) (s : (F.comp (CategoryTheory.yoneda.obj X)).sections) (j : J) :
.app j = Quiver.Hom.op (s j)
@[simp]
theorem CategoryTheory.Limits.compYonedaSectionsEquiv_symm_apply_coe {J : Type u_1} {C : Type u_2} [] [] (F : ) (X : C) (τ : .obj { unop := X } F) (j : J) :
( τ) j = (τ.app j).unop
def CategoryTheory.Limits.compYonedaSectionsEquiv {J : Type u_1} {C : Type u_2} [] [] (F : ) (X : C) :
(F.comp (CategoryTheory.yoneda.obj X)).sections (.obj { unop := 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.
Instances For
@[simp]
theorem CategoryTheory.Limits.limitCompCoyonedaIsoCone_hom_app {J : Type v} {C : Type u} (F : ) (X : C) :
∀ (a : CategoryTheory.Limits.limit (F.comp (CategoryTheory.coyoneda.obj { unop := X }))) (j : J), ().app j = CategoryTheory.Limits.limit.π (F.comp (CategoryTheory.coyoneda.obj { unop := X })) j a
@[simp]
theorem CategoryTheory.Limits.limitCompCoyonedaIsoCone_inv {J : Type v} {C : Type u} (F : ) (X : C) :
∀ (a : .obj X F), = (CategoryTheory.Limits.Types.limitEquivSections (F.comp (CategoryTheory.coyoneda.obj { unop := X }))).symm ( a)
noncomputable def CategoryTheory.Limits.limitCompCoyonedaIsoCone {J : Type v} {C : Type u} (F : ) (X : C) :
CategoryTheory.Limits.limit (F.comp (CategoryTheory.coyoneda.obj { unop := X })) .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.
Instances For
@[simp]
theorem CategoryTheory.Limits.coyonedaCompLimIsoCones_inv_app {J : Type v} {C : Type u} (F : ) (X : Cᵒᵖ) :
∀ (a : F.cones.obj X), .app X a = (CategoryTheory.Limits.Types.limitEquivSections (F.comp (CategoryTheory.coyoneda.obj X))).symm (.symm a)
@[simp]
theorem CategoryTheory.Limits.coyonedaCompLimIsoCones_hom_app_app {J : Type v} {C : Type u} (F : ) (X : Cᵒᵖ) :
∀ (a : (CategoryTheory.coyoneda.comp ((().obj F).comp CategoryTheory.Limits.lim)).obj X) (j : J), (.app X a).app j = CategoryTheory.Limits.limit.π (F.comp (CategoryTheory.coyoneda.obj X)) j a
noncomputable def CategoryTheory.Limits.coyonedaCompLimIsoCones {J : Type v} {C : Type u} (F : ) :
CategoryTheory.coyoneda.comp ((().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
Instances For
@[simp]
theorem CategoryTheory.Limits.whiskeringLimYonedaIsoCones_inv_app_app (J : Type v) (C : Type u) (X : ) (X : Cᵒᵖ) :
∀ (a : X✝.cones.obj X), (.app X✝).app X a = (CategoryTheory.Limits.Types.limitEquivSections (X✝.comp (CategoryTheory.coyoneda.obj X))).symm (().symm a)
@[simp]
theorem CategoryTheory.Limits.whiskeringLimYonedaIsoCones_hom_app_app_app (J : Type v) (C : Type u) (X : ) (X : Cᵒᵖ) :
∀ (a : (CategoryTheory.coyoneda.comp ((().obj X✝).comp CategoryTheory.Limits.lim)).obj X) (j : J), ((.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) (C : Type u) :
().comp ((().obj CategoryTheory.Limits.lim).comp (().obj CategoryTheory.coyoneda))

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
Instances For
@[simp]
theorem CategoryTheory.Limits.limitCompYonedaIsoCocone_inv {J : Type v} {C : Type u} (F : ) (X : C) :
∀ (a : F .obj X), = (CategoryTheory.Limits.Types.limitEquivSections (F.op.comp (CategoryTheory.yoneda.obj X))).symm ( a)
@[simp]
theorem CategoryTheory.Limits.limitCompYonedaIsoCocone_hom_app {J : Type v} {C : Type u} (F : ) (X : C) :
∀ (a : CategoryTheory.Limits.limit (F.op.comp (CategoryTheory.yoneda.obj X))) (j : J), ().app j = CategoryTheory.Limits.limit.π (F.op.comp (CategoryTheory.yoneda.obj X)) { unop := j } a
noncomputable def CategoryTheory.Limits.limitCompYonedaIsoCocone {J : Type v} {C : Type u} (F : ) (X : C) :
CategoryTheory.Limits.limit (F.op.comp (CategoryTheory.yoneda.obj X)) F .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.
Instances For
@[simp]
theorem CategoryTheory.Limits.yonedaCompLimIsoCocones_inv_app {J : Type v} {C : Type u} (F : ) (X : C) :
∀ (a : F.cocones.obj X), .app X a = (CategoryTheory.Limits.Types.limitEquivSections (F.op.comp (CategoryTheory.yoneda.obj X))).symm ( a)
@[simp]
theorem CategoryTheory.Limits.yonedaCompLimIsoCocones_hom_app_app {J : Type v} {C : Type u} (F : ) (X : C) :
∀ (a : (CategoryTheory.yoneda.comp ((().obj F.op).comp CategoryTheory.Limits.lim)).obj X) (j : J), (.app X a).app j = CategoryTheory.Limits.limit.π (F.op.comp (CategoryTheory.yoneda.obj X)) { unop := j } a
noncomputable def CategoryTheory.Limits.yonedaCompLimIsoCocones {J : Type v} {C : Type u} (F : ) :
CategoryTheory.yoneda.comp ((().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
Instances For
@[simp]
theorem CategoryTheory.Limits.opHomCompWhiskeringLimYonedaIsoCocones_inv_app_app (J : Type v) (C : Type u) (X : ()ᵒᵖ) (X : C) :
∀ (a : X✝.unop.cocones.obj X), ( X✝).app X a = (CategoryTheory.Limits.Types.limitEquivSections (X✝.unop.op.comp (CategoryTheory.yoneda.obj X))).symm (().symm a)
@[simp]
theorem CategoryTheory.Limits.opHomCompWhiskeringLimYonedaIsoCocones_hom_app_app_app (J : Type v) (C : Type u) (X : ()ᵒᵖ) (X : C) :
∀ (a : (CategoryTheory.yoneda.comp ((().obj X✝.unop.op).comp CategoryTheory.Limits.lim)).obj X) (j : J), (( X✝).app X a).app j = CategoryTheory.Limits.limit.π (X✝.unop.op.comp (CategoryTheory.yoneda.obj X)) { unop := j } a
noncomputable def CategoryTheory.Limits.opHomCompWhiskeringLimYonedaIsoCocones (J : Type v) (C : Type u) :
.comp (().comp ((().obj CategoryTheory.Limits.lim).comp (().obj CategoryTheory.yoneda)))

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.
Instances For