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)

instance CategoryTheory.Limits.instHasLimitOppositeOpOfHasColimit {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.op

Equations

• ⋯ = ⋯

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 ≅ { unop := 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_π_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 { unop := i } ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitOpIsoOpColimit F).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F.op { unop := i }) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F i).op h

@[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 { unop := i }) = (CategoryTheory.Limits.colimit.ι F i).op

@[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 : { unop := 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 { unop := i }) 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 { unop := i }

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 ≅ { unop := 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_π_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 { unop := i }).op h

@[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 { unop := i }).op

@[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 : { unop := F.obj { unop := i } } ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitRightOpIsoOpColimit F).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F { unop := i }).op h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F.rightOp i) 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 { unop := i }).op = CategoryTheory.Limits.limit.π F.rightOp i

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 { unop := 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_π_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 { unop := i }) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda F).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.op.comp CategoryTheory.coyoneda) { unop := i }) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.coyoneda.map (CategoryTheory.Limits.colimit.ι F i).op) h

@[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) { unop := i }) = CategoryTheory.coyoneda.map (CategoryTheory.Limits.colimit.ι F i).op

@[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 { unop := 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) { unop := i }) 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) { unop := i }

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_π_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 { unop := i }) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitHomIsoLimitYoneda F A).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.op.comp (CategoryTheory.yoneda.obj A)) { unop := i }) h) = CategoryTheory.CategoryStruct.comp ((CategoryTheory.coyoneda.map (CategoryTheory.Limits.colimit.ι F i).op).app A) h

@[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)) { unop := i }) = (CategoryTheory.coyoneda.map (CategoryTheory.Limits.colimit.ι F i).op).app A

@[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 { unop := 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)) { unop := i }) 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)) { unop := i }

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 { unop := 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_π_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 { unop := i }).op) h

@[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 { unop := i }).op

@[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 { unop := F.obj { unop := i } } ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda' F).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.coyoneda.map (CategoryTheory.Limits.colimit.ι F { unop := i }).op) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.rightOp.comp CategoryTheory.coyoneda) i) 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 { unop := i }).op) = CategoryTheory.Limits.limit.π (F.rightOp.comp CategoryTheory.coyoneda) i

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_π_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 { unop := i }).op).app A) h

@[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 { unop := i }).op).app A

@[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 { unop := F.obj { unop := i } }).obj A ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitHomIsoLimitYoneda' F A).inv (CategoryTheory.CategoryStruct.comp ((CategoryTheory.coyoneda.map (CategoryTheory.Limits.colimit.ι F { unop := i }).op).app A) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.rightOp.comp (CategoryTheory.yoneda.obj A)) i) 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 { unop := i }).op).app A) = CategoryTheory.Limits.limit.π (F.rightOp.comp (CategoryTheory.yoneda.obj A)) 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.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₂} )) { unop := i } ((CategoryTheory.Limits.colimitCoyonedaHomIsoLimit D F).hom f) = { down := f.app (D.obj { unop := i }) ((CategoryTheory.Limits.colimit.ι (D.rightOp.comp CategoryTheory.coyoneda) i).app (D.obj { unop := i }) (CategoryTheory.CategoryStruct.id (D.obj { unop := 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) { unop := i }).app (D.obj i) (CategoryTheory.CategoryStruct.id (D.obj i))) }