Ind- and pro- (co)yoneda lemmas

We define limit versions of the yoneda and coyoneda lemmas.

Main results

Notation: categories C, I and functors D : Iᵒᵖ ⥤ C, F : C ⥤ Type.

• colimitCoyonedaHomIsoLimit: pro-coyoneda lemma: homorphisms from colimit of coyoneda of diagram D to F is limit of F evaluated at D.
• colimitCoyonedaHomIsoLimit': a variant of colimitCoyonedaHomIsoLimit for a covariant diagram.

TODO

• define the ind-yoneda versions (for contravariant F)

noncomputable def CategoryTheory.Limits.limitOpIsoOpColimit {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [CategoryTheory.Category.{v₂, v₁} I] (F : CategoryTheory.Functor I C) [CategoryTheory.Limits.HasColimit F] : CategoryTheory.Limits.limit F.op ≅ Opposite.op (CategoryTheory.Limits.colimit F)

The limit of F.op is the opposite of colimit F.

Equations

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

@[simp]

theorem CategoryTheory.Limits.limitOpIsoOpColimit_inv_comp_π {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [CategoryTheory.Category.{v₂, v₁} I] (F : CategoryTheory.Functor I C) [CategoryTheory.Limits.HasColimit F] (i : I) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitOpIsoOpColimit F).inv (CategoryTheory.Limits.limit.π F.op (Opposite.op i)) = (CategoryTheory.Limits.colimit.ι F i).op

@[simp]

theorem CategoryTheory.Limits.limitOpIsoOpColimit_inv_comp_π_assoc {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [CategoryTheory.Category.{v₂, v₁} I] (F : CategoryTheory.Functor I C) [CategoryTheory.Limits.HasColimit F] (i : I) {Z : Cᵒᵖ} (h : F.op.obj (Opposite.op i) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitOpIsoOpColimit F).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F.op (Opposite.op i)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F i).op h

@[simp]

theorem CategoryTheory.Limits.limitOpIsoOpColimit_hom_comp_ι {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [CategoryTheory.Category.{v₂, v₁} I] (F : CategoryTheory.Functor I C) [CategoryTheory.Limits.HasColimit F] (i : I) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitOpIsoOpColimit F).hom (CategoryTheory.Limits.colimit.ι F i).op = CategoryTheory.Limits.limit.π F.op (Opposite.op i)

@[simp]

theorem CategoryTheory.Limits.limitOpIsoOpColimit_hom_comp_ι_assoc {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [CategoryTheory.Category.{v₂, v₁} I] (F : CategoryTheory.Functor I C) [CategoryTheory.Limits.HasColimit F] (i : I) {Z : Cᵒᵖ} (h : Opposite.op (F.obj i) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitOpIsoOpColimit F).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F i).op h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F.op (Opposite.op i)) h

instance CategoryTheory.Limits.instHasLimitOppositeRightOpOfHasColimit {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [CategoryTheory.Category.{v₂, v₁} I] (F : CategoryTheory.Functor Iᵒᵖ C) [CategoryTheory.Limits.HasColimit F] : CategoryTheory.Limits.HasLimit F.rightOp

Equations

• ⋯ = ⋯

noncomputable def CategoryTheory.Limits.limitRightOpIsoOpColimit {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [CategoryTheory.Category.{v₂, v₁} I] (F : CategoryTheory.Functor Iᵒᵖ C) [CategoryTheory.Limits.HasColimit F] : CategoryTheory.Limits.limit F.rightOp ≅ Opposite.op (CategoryTheory.Limits.colimit F)

limitOpIsoOpColimit for contravariant functor.

Equations

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

@[simp]

theorem CategoryTheory.Limits.limitRightOpIsoOpColimit_inv_comp_π {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [CategoryTheory.Category.{v₂, v₁} I] (F : CategoryTheory.Functor Iᵒᵖ C) [CategoryTheory.Limits.HasColimit F] (i : I) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitRightOpIsoOpColimit F).inv (CategoryTheory.Limits.limit.π F.rightOp i) = (CategoryTheory.Limits.colimit.ι F (Opposite.op i)).op

@[simp]

theorem CategoryTheory.Limits.limitRightOpIsoOpColimit_inv_comp_π_assoc {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [CategoryTheory.Category.{v₂, v₁} I] (F : CategoryTheory.Functor Iᵒᵖ C) [CategoryTheory.Limits.HasColimit F] (i : I) {Z : Cᵒᵖ} (h : F.rightOp.obj i ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitRightOpIsoOpColimit F).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F.rightOp i) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F (Opposite.op i)).op h

@[simp]

theorem CategoryTheory.Limits.limitRightOpIsoOpColimit_hom_comp_ι {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [CategoryTheory.Category.{v₂, v₁} I] (F : CategoryTheory.Functor Iᵒᵖ C) [CategoryTheory.Limits.HasColimit F] (i : I) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitRightOpIsoOpColimit F).hom (CategoryTheory.Limits.colimit.ι F (Opposite.op i)).op = CategoryTheory.Limits.limit.π F.rightOp i

@[simp]

theorem CategoryTheory.Limits.limitRightOpIsoOpColimit_hom_comp_ι_assoc {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [CategoryTheory.Category.{v₂, v₁} I] (F : CategoryTheory.Functor Iᵒᵖ C) [CategoryTheory.Limits.HasColimit F] (i : I) {Z : Cᵒᵖ} (h : Opposite.op (F.obj (Opposite.op i)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitRightOpIsoOpColimit F).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F (Opposite.op i)).op h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F.rightOp i) h

noncomputable def CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [CategoryTheory.Category.{v₂, v₁} I] (F : CategoryTheory.Functor I C) [CategoryTheory.Limits.HasColimit F] : CategoryTheory.coyoneda.obj (Opposite.op (CategoryTheory.Limits.colimit F)) ≅ CategoryTheory.Limits.limit (F.op.comp CategoryTheory.coyoneda)

Hom is functorially cocontinuous: coyoneda of a colimit is the limit over coyoneda of the diagram.

Equations

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

@[simp]

theorem CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda_hom_comp_π {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [CategoryTheory.Category.{v₂, v₁} I] (F : CategoryTheory.Functor I C) [CategoryTheory.Limits.HasColimit F] (i : I) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda F).hom (CategoryTheory.Limits.limit.π (F.op.comp CategoryTheory.coyoneda) (Opposite.op i)) = CategoryTheory.coyoneda.map (CategoryTheory.Limits.colimit.ι F i).op

@[simp]

theorem CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda_hom_comp_π_assoc {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [CategoryTheory.Category.{v₂, v₁} I] (F : CategoryTheory.Functor I C) [CategoryTheory.Limits.HasColimit F] (i : I) {Z : CategoryTheory.Functor C (Type u₂)} (h : CategoryTheory.coyoneda.obj (F.op.obj (Opposite.op i)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda F).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.op.comp CategoryTheory.coyoneda) (Opposite.op i)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.coyoneda.map (CategoryTheory.Limits.colimit.ι F i).op) h

@[simp]

theorem CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda_inv_comp_π {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [CategoryTheory.Category.{v₂, v₁} I] (F : CategoryTheory.Functor I C) [CategoryTheory.Limits.HasColimit F] (i : I) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda F).inv (CategoryTheory.coyoneda.map (CategoryTheory.Limits.colimit.ι F i).op) = CategoryTheory.Limits.limit.π (F.op.comp CategoryTheory.coyoneda) (Opposite.op i)

@[simp]

theorem CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda_inv_comp_π_assoc {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [CategoryTheory.Category.{v₂, v₁} I] (F : CategoryTheory.Functor I C) [CategoryTheory.Limits.HasColimit F] (i : I) {Z : CategoryTheory.Functor C (Type u₂)} (h : CategoryTheory.coyoneda.obj (Opposite.op (F.obj i)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda F).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.coyoneda.map (CategoryTheory.Limits.colimit.ι F i).op) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.op.comp CategoryTheory.coyoneda) (Opposite.op i)) h

noncomputable def CategoryTheory.Limits.colimitHomIsoLimitYoneda {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [CategoryTheory.Category.{v₂, v₁} I] (F : CategoryTheory.Functor I C) [CategoryTheory.Limits.HasColimit F] [CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type u₂)] (A : C) : (CategoryTheory.Limits.colimit F ⟶ A) ≅ CategoryTheory.Limits.limit (F.op.comp (CategoryTheory.yoneda.obj A))

Hom is cocontinuous: homomorphisms from a colimit is the limit over yoneda of the diagram.

Equations

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

@[simp]

theorem CategoryTheory.Limits.colimitHomIsoLimitYoneda_hom_comp_π {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [CategoryTheory.Category.{v₂, v₁} I] (F : CategoryTheory.Functor I C) [CategoryTheory.Limits.HasColimit F] [CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type u₂)] (A : C) (i : I) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitHomIsoLimitYoneda F A).hom (CategoryTheory.Limits.limit.π (F.op.comp (CategoryTheory.yoneda.obj A)) (Opposite.op i)) = (CategoryTheory.coyoneda.map (CategoryTheory.Limits.colimit.ι F i).op).app A

@[simp]

theorem CategoryTheory.Limits.colimitHomIsoLimitYoneda_hom_comp_π_assoc {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [CategoryTheory.Category.{v₂, v₁} I] (F : CategoryTheory.Functor I C) [CategoryTheory.Limits.HasColimit F] [CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type u₂)] (A : C) (i : I) {Z : Type u₂} (h : (CategoryTheory.yoneda.obj A).obj (F.op.obj (Opposite.op i)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitHomIsoLimitYoneda F A).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.op.comp (CategoryTheory.yoneda.obj A)) (Opposite.op i)) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.coyoneda.map (CategoryTheory.Limits.colimit.ι F i).op).app A) h

@[simp]

theorem CategoryTheory.Limits.colimitHomIsoLimitYoneda_inv_comp_π {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [CategoryTheory.Category.{v₂, v₁} I] (F : CategoryTheory.Functor I C) [CategoryTheory.Limits.HasColimit F] [CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type u₂)] (A : C) (i : I) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitHomIsoLimitYoneda F A).inv ((CategoryTheory.coyoneda.map (CategoryTheory.Limits.colimit.ι F i).op).app A) = CategoryTheory.Limits.limit.π (F.op.comp (CategoryTheory.yoneda.obj A)) (Opposite.op i)

@[simp]

theorem CategoryTheory.Limits.colimitHomIsoLimitYoneda_inv_comp_π_assoc {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [CategoryTheory.Category.{v₂, v₁} I] (F : CategoryTheory.Functor I C) [CategoryTheory.Limits.HasColimit F] [CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type u₂)] (A : C) (i : I) {Z : Type u₂} (h : (CategoryTheory.coyoneda.obj (Opposite.op (F.obj i))).obj A ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitHomIsoLimitYoneda F A).inv (CategoryTheory.CategoryStruct.comp ((CategoryTheory.coyoneda.map (CategoryTheory.Limits.colimit.ι F i).op).app A) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.op.comp (CategoryTheory.yoneda.obj A)) (Opposite.op i)) h

noncomputable def CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda' {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [CategoryTheory.Category.{v₂, v₁} I] (F : CategoryTheory.Functor Iᵒᵖ C) [CategoryTheory.Limits.HasColimit F] : CategoryTheory.coyoneda.obj (Opposite.op (CategoryTheory.Limits.colimit F)) ≅ CategoryTheory.Limits.limit (F.rightOp.comp CategoryTheory.coyoneda)

Variant of coyonedaOoColimitIsoLimitCoyoneda for contravariant F.

Equations

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

@[simp]

theorem CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda'_hom_comp_π {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [CategoryTheory.Category.{v₂, v₁} I] (F : CategoryTheory.Functor Iᵒᵖ C) [CategoryTheory.Limits.HasColimit F] (i : I) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda' F).hom (CategoryTheory.Limits.limit.π (F.rightOp.comp CategoryTheory.coyoneda) i) = CategoryTheory.coyoneda.map (CategoryTheory.Limits.colimit.ι F (Opposite.op i)).op

@[simp]

theorem CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda'_hom_comp_π_assoc {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [CategoryTheory.Category.{v₂, v₁} I] (F : CategoryTheory.Functor Iᵒᵖ C) [CategoryTheory.Limits.HasColimit F] (i : I) {Z : CategoryTheory.Functor C (Type u₂)} (h : CategoryTheory.coyoneda.obj (F.rightOp.obj i) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda' F).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.rightOp.comp CategoryTheory.coyoneda) i) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.coyoneda.map (CategoryTheory.Limits.colimit.ι F (Opposite.op i)).op) h

@[simp]

theorem CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda'_inv_comp_π {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [CategoryTheory.Category.{v₂, v₁} I] (F : CategoryTheory.Functor Iᵒᵖ C) [CategoryTheory.Limits.HasColimit F] (i : I) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda' F).inv (CategoryTheory.coyoneda.map (CategoryTheory.Limits.colimit.ι F (Opposite.op i)).op) = CategoryTheory.Limits.limit.π (F.rightOp.comp CategoryTheory.coyoneda) i

@[simp]

theorem CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda'_inv_comp_π_assoc {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [CategoryTheory.Category.{v₂, v₁} I] (F : CategoryTheory.Functor Iᵒᵖ C) [CategoryTheory.Limits.HasColimit F] (i : I) {Z : CategoryTheory.Functor C (Type u₂)} (h : CategoryTheory.coyoneda.obj (Opposite.op (F.obj (Opposite.op i))) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda' F).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.coyoneda.map (CategoryTheory.Limits.colimit.ι F (Opposite.op i)).op) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.rightOp.comp CategoryTheory.coyoneda) i) h

noncomputable def CategoryTheory.Limits.colimitHomIsoLimitYoneda' {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [CategoryTheory.Category.{v₂, v₁} I] (F : CategoryTheory.Functor Iᵒᵖ C) [CategoryTheory.Limits.HasColimit F] [CategoryTheory.Limits.HasLimitsOfShape I (Type u₂)] (A : C) : (CategoryTheory.Limits.colimit F ⟶ A) ≅ CategoryTheory.Limits.limit (F.rightOp.comp (CategoryTheory.yoneda.obj A))

Variant of colimitHomIsoLimitYoneda for contravariant F.

Equations

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

@[simp]

theorem CategoryTheory.Limits.colimitHomIsoLimitYoneda'_hom_comp_π {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [CategoryTheory.Category.{v₂, v₁} I] (F : CategoryTheory.Functor Iᵒᵖ C) [CategoryTheory.Limits.HasColimit F] [CategoryTheory.Limits.HasLimitsOfShape I (Type u₂)] (A : C) (i : I) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitHomIsoLimitYoneda' F A).hom (CategoryTheory.Limits.limit.π (F.rightOp.comp (CategoryTheory.yoneda.obj A)) i) = (CategoryTheory.coyoneda.map (CategoryTheory.Limits.colimit.ι F (Opposite.op i)).op).app A

@[simp]

theorem CategoryTheory.Limits.colimitHomIsoLimitYoneda'_hom_comp_π_assoc {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [CategoryTheory.Category.{v₂, v₁} I] (F : CategoryTheory.Functor Iᵒᵖ C) [CategoryTheory.Limits.HasColimit F] [CategoryTheory.Limits.HasLimitsOfShape I (Type u₂)] (A : C) (i : I) {Z : Type u₂} (h : (CategoryTheory.yoneda.obj A).obj (F.rightOp.obj i) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitHomIsoLimitYoneda' F A).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.rightOp.comp (CategoryTheory.yoneda.obj A)) i) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.coyoneda.map (CategoryTheory.Limits.colimit.ι F (Opposite.op i)).op).app A) h

@[simp]

theorem CategoryTheory.Limits.colimitHomIsoLimitYoneda'_inv_comp_π {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [CategoryTheory.Category.{v₂, v₁} I] (F : CategoryTheory.Functor Iᵒᵖ C) [CategoryTheory.Limits.HasColimit F] [CategoryTheory.Limits.HasLimitsOfShape I (Type u₂)] (A : C) (i : I) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitHomIsoLimitYoneda' F A).inv ((CategoryTheory.coyoneda.map (CategoryTheory.Limits.colimit.ι F (Opposite.op i)).op).app A) = CategoryTheory.Limits.limit.π (F.rightOp.comp (CategoryTheory.yoneda.obj A)) i

@[simp]

theorem CategoryTheory.Limits.colimitHomIsoLimitYoneda'_inv_comp_π_assoc {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [CategoryTheory.Category.{v₂, v₁} I] (F : CategoryTheory.Functor Iᵒᵖ C) [CategoryTheory.Limits.HasColimit F] [CategoryTheory.Limits.HasLimitsOfShape I (Type u₂)] (A : C) (i : I) {Z : Type u₂} (h : (CategoryTheory.coyoneda.obj (Opposite.op (F.obj (Opposite.op i)))).obj A ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitHomIsoLimitYoneda' F A).inv (CategoryTheory.CategoryStruct.comp ((CategoryTheory.coyoneda.map (CategoryTheory.Limits.colimit.ι F (Opposite.op i)).op).app A) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.rightOp.comp (CategoryTheory.yoneda.obj A)) i) h

noncomputable def CategoryTheory.Limits.colimitCoyonedaHomIsoLimit {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [CategoryTheory.Category.{v₂, v₁} I] (D : CategoryTheory.Functor Iᵒᵖ C) (F : CategoryTheory.Functor C (Type u₂)) [CategoryTheory.Limits.HasColimit (D.rightOp.comp CategoryTheory.coyoneda)] [CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))] : (CategoryTheory.Limits.colimit (D.rightOp.comp CategoryTheory.coyoneda) ⟶ F) ≅ CategoryTheory.Limits.limit (D.comp (F.comp CategoryTheory.uliftFunctor.{u₁, u₂} ))

Pro-Coyoneda lemma: homorphisms from colimit of coyoneda of diagram D to F is limit of F evaluated at D.

Equations

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

@[simp]

theorem CategoryTheory.Limits.colimitCoyonedaHomIsoLimit_π_apply {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [CategoryTheory.Category.{v₂, v₁} I] (D : CategoryTheory.Functor Iᵒᵖ C) (F : CategoryTheory.Functor C (Type u₂)) [CategoryTheory.Limits.HasColimit (D.rightOp.comp CategoryTheory.coyoneda)] [CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))] (f : CategoryTheory.Limits.colimit (D.rightOp.comp CategoryTheory.coyoneda) ⟶ F) (i : I) : CategoryTheory.Limits.limit.π (D.comp (F.comp CategoryTheory.uliftFunctor.{u₁, u₂} )) (Opposite.op i) ((CategoryTheory.Limits.colimitCoyonedaHomIsoLimit D F).hom f) = { down := f.app (D.obj (Opposite.op i)) ((CategoryTheory.Limits.colimit.ι (D.rightOp.comp CategoryTheory.coyoneda) i).app (D.obj (Opposite.op i)) (CategoryTheory.CategoryStruct.id (D.obj (Opposite.op i)))) }

noncomputable def CategoryTheory.Limits.colimitCoyonedaHomIsoLimit' {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [CategoryTheory.Category.{v₂, v₁} I] (D : CategoryTheory.Functor I C) (F : CategoryTheory.Functor C (Type u₂)) [CategoryTheory.Limits.HasColimit (D.op.comp CategoryTheory.coyoneda)] [CategoryTheory.Limits.HasLimitsOfShape I (Type (max u₁ u₂))] : (CategoryTheory.Limits.colimit (D.op.comp CategoryTheory.coyoneda) ⟶ F) ≅ CategoryTheory.Limits.limit (D.comp (F.comp CategoryTheory.uliftFunctor.{u₁, u₂} ))

A variant of colimitCoyonedaHomIsoLimit for a contravariant diagram.

Equations

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

@[simp]

theorem CategoryTheory.Limits.colimitCoyonedaHomIsoLimit'_π_apply {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [CategoryTheory.Category.{v₂, v₁} I] (D : CategoryTheory.Functor I C) (F : CategoryTheory.Functor C (Type u₂)) [CategoryTheory.Limits.HasColimit (D.op.comp CategoryTheory.coyoneda)] [CategoryTheory.Limits.HasLimitsOfShape I (Type (max u₁ u₂))] (f : CategoryTheory.Limits.colimit (D.op.comp CategoryTheory.coyoneda) ⟶ F) (i : I) : CategoryTheory.Limits.limit.π (D.comp (F.comp CategoryTheory.uliftFunctor.{u₁, u₂} )) i ((CategoryTheory.Limits.colimitCoyonedaHomIsoLimit' D F).hom f) = { down := f.app (D.obj i) ((CategoryTheory.Limits.colimit.ι (D.op.comp CategoryTheory.coyoneda) (Opposite.op i)).app (D.obj i) (CategoryTheory.CategoryStruct.id (D.obj i))) }