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.

noncomputable def CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda {C : Type u₁} [Category.{u₂, u₁} C] {I : Type v₁} [Category.{v₂, v₁} I] (F : Functor I C) [HasColimit F] : coyoneda.obj (Opposite.op (colimit F)) ≅ limit (F.op.comp 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₁} [Category.{u₂, u₁} C] {I : Type v₁} [Category.{v₂, v₁} I] (F : Functor I C) [HasColimit F] (i : I) : CategoryStruct.comp (coyonedaOpColimitIsoLimitCoyoneda F).hom (limit.π (F.op.comp coyoneda) (Opposite.op i)) = coyoneda.map (colimit.ι F i).op

@[simp]

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

@[simp]

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

@[simp]

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

noncomputable def CategoryTheory.Limits.colimitHomIsoLimitYoneda {C : Type u₁} [Category.{u₂, u₁} C] {I : Type v₁} [Category.{v₂, v₁} I] (F : Functor I C) [HasColimit F] [HasLimitsOfShape Iᵒᵖ (Type u₂)] (A : C) : (colimit F ⟶ A) ≅ limit (F.op.comp (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₁} [Category.{u₂, u₁} C] {I : Type v₁} [Category.{v₂, v₁} I] (F : Functor I C) [HasColimit F] [HasLimitsOfShape Iᵒᵖ (Type u₂)] (A : C) (i : I) : CategoryStruct.comp (colimitHomIsoLimitYoneda F A).hom (limit.π (F.op.comp (yoneda.obj A)) (Opposite.op i)) = (coyoneda.map (colimit.ι F i).op).app A

@[simp]

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

@[simp]

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

@[simp]

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

noncomputable def CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda' {C : Type u₁} [Category.{u₂, u₁} C] {I : Type v₁} [Category.{v₂, v₁} I] (F : Functor Iᵒᵖ C) [HasColimit F] : coyoneda.obj (Opposite.op (colimit F)) ≅ limit (F.rightOp.comp 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₁} [Category.{u₂, u₁} C] {I : Type v₁} [Category.{v₂, v₁} I] (F : Functor Iᵒᵖ C) [HasColimit F] (i : I) : CategoryStruct.comp (coyonedaOpColimitIsoLimitCoyoneda' F).hom (limit.π (F.rightOp.comp coyoneda) i) = coyoneda.map (colimit.ι F (Opposite.op i)).op

@[simp]

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

@[simp]

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

@[simp]

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

noncomputable def CategoryTheory.Limits.colimitHomIsoLimitYoneda' {C : Type u₁} [Category.{u₂, u₁} C] {I : Type v₁} [Category.{v₂, v₁} I] (F : Functor Iᵒᵖ C) [HasColimit F] [HasLimitsOfShape I (Type u₂)] (A : C) : (colimit F ⟶ A) ≅ limit (F.rightOp.comp (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₁} [Category.{u₂, u₁} C] {I : Type v₁} [Category.{v₂, v₁} I] (F : Functor Iᵒᵖ C) [HasColimit F] [HasLimitsOfShape I (Type u₂)] (A : C) (i : I) : CategoryStruct.comp (colimitHomIsoLimitYoneda' F A).hom (limit.π (F.rightOp.comp (yoneda.obj A)) i) = (coyoneda.map (colimit.ι F (Opposite.op i)).op).app A

@[simp]

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

@[simp]

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

@[simp]

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

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

Pro-Coyoneda lemma: morphisms from colimit of coyoneda of diagram D to F is limit of F evaluated at D. This variant is for contravariant diagrams, see colimitCoyonedaHomIsoLimit' for a covariant version.

Equations

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

@[simp]

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

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

Pro-Coyoneda lemma: morphisms from colimit of coyoneda of diagram D to F is limit of F evaluated at D. This variant is for contravariant diagrams, see colimitCoyonedaHomIsoLimit' for a covariant version.

Equations

• CategoryTheory.Limits.colimitCoyonedaHomIsoLimitLeftOp D F = CategoryTheory.Limits.colimitCoyonedaHomIsoLimit D.leftOp F

@[simp]

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

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

Ind-Yoneda lemma: morphisms from colimit of yoneda of diagram D to F is limit of F evaluated at D. This version is for covariant diagrams, see colimitYonedaHomIsoLimit' for a contravariant version.

Equations

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

@[simp]

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

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

Ind-Yoneda lemma: morphisms from colimit of yoneda of diagram D to F is limit of F evaluated at D. This version is for covariant diagrams, see colimitYonedaHomIsoLimit' for a contravariant version.

Equations

• CategoryTheory.Limits.colimitYonedaHomIsoLimitOp D F = CategoryTheory.Limits.colimitYonedaHomIsoLimit D.op F

@[simp]

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

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

Pro-Coyoneda lemma: morphisms from colimit of coyoneda of diagram D to F is limit of F evaluated at D. This variant is for covariant diagrams, see colimitCoyonedaHomIsoLimit for a covariant version.

Equations

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

@[simp]

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

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

Pro-Coyoneda lemma: morphisms from colimit of coyoneda of diagram D to F is limit of F evaluated at D. This variant is for covariant diagrams, see colimitCoyonedaHomIsoLimit for a covariant version.

Equations

• CategoryTheory.Limits.colimitCoyonedaHomIsoLimitUnop D F = CategoryTheory.Limits.colimitCoyonedaHomIsoLimit' D.unop F

@[simp]

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

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

Ind-Yoneda lemma: morphisms from colimit of yoneda of diagram D to F is limit of F evaluated at D. This version is for contravariant diagrams, see colimitYonedaHomIsoLimit for a covariant version.

Equations

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

@[simp]

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

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

Ind-Yoneda lemma: morphisms from colimit of yoneda of diagram D to F is limit of F evaluated at D. This version is for contravariant diagrams, see colimitYonedaHomIsoLimit for a covariant version.

Equations

• CategoryTheory.Limits.colimitYonedaHomIsoLimitRightOp D F = CategoryTheory.Limits.colimitYonedaHomIsoLimit' D.rightOp F

@[simp]

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