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₁} [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: 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₁} [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.colimitCoyonedaHomIsoLimitLeftOp {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.comp CategoryTheory.coyoneda)] [CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))] : (CategoryTheory.Limits.colimit (D.comp CategoryTheory.coyoneda) ⟶ F) ≅ CategoryTheory.Limits.limit (D.leftOp.comp (F.comp CategoryTheory.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₁} [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.comp CategoryTheory.coyoneda)] [CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))] (f : CategoryTheory.Limits.colimit (D.comp CategoryTheory.coyoneda) ⟶ F) (i : I) : CategoryTheory.Limits.limit.π (D.leftOp.comp (F.comp CategoryTheory.uliftFunctor.{u₁, u₂})) (Opposite.op i) ((CategoryTheory.Limits.colimitCoyonedaHomIsoLimitLeftOp D F).hom f) = { down := f.app (Opposite.unop (D.obj i)) ((CategoryTheory.Limits.colimit.ι (D.comp CategoryTheory.coyoneda) i).app (Opposite.unop (D.obj i)) (CategoryTheory.CategoryStruct.id (Opposite.unop (D.obj i)))) }

noncomputable def CategoryTheory.Limits.colimitYonedaHomIsoLimit {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.unop.comp CategoryTheory.yoneda)] [CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))] : (CategoryTheory.Limits.colimit (D.unop.comp CategoryTheory.yoneda) ⟶ F) ≅ CategoryTheory.Limits.limit (D.comp (F.comp CategoryTheory.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₁} [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.unop.comp CategoryTheory.yoneda)] [CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))] (f : CategoryTheory.Limits.colimit (D.unop.comp CategoryTheory.yoneda) ⟶ F) (i : Iᵒᵖ) : CategoryTheory.Limits.limit.π (D.comp (F.comp CategoryTheory.uliftFunctor.{u₁, u₂})) i ((CategoryTheory.Limits.colimitYonedaHomIsoLimit D F).hom f) = { down := f.app (D.obj i) ((CategoryTheory.Limits.colimit.ι (D.unop.comp CategoryTheory.yoneda) (Opposite.unop i)).app (D.obj i) (CategoryTheory.CategoryStruct.id (Opposite.unop (D.obj i)))) }

noncomputable def CategoryTheory.Limits.colimitYonedaHomIsoLimitOp {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.comp CategoryTheory.yoneda)] [CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))] : (CategoryTheory.Limits.colimit (D.comp CategoryTheory.yoneda) ⟶ F) ≅ CategoryTheory.Limits.limit (D.op.comp (F.comp CategoryTheory.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₁} [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.comp CategoryTheory.yoneda)] [CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))] (f : CategoryTheory.Limits.colimit (D.comp CategoryTheory.yoneda) ⟶ F) (i : Iᵒᵖ) : CategoryTheory.Limits.limit.π (D.op.comp (F.comp CategoryTheory.uliftFunctor.{u₁, u₂})) i ((CategoryTheory.Limits.colimitYonedaHomIsoLimitOp D F).hom f) = { down := f.app (Opposite.op (D.obj (Opposite.unop i))) ((CategoryTheory.Limits.colimit.ι (D.comp CategoryTheory.yoneda) (Opposite.unop i)).app (Opposite.op (D.obj (Opposite.unop i))) (CategoryTheory.CategoryStruct.id (D.obj (Opposite.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₂}))

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₁} [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))) }

noncomputable def CategoryTheory.Limits.colimitCoyonedaHomIsoLimitUnop {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.comp CategoryTheory.coyoneda)] [CategoryTheory.Limits.HasLimitsOfShape I (Type (max u₁ u₂))] : (CategoryTheory.Limits.colimit (D.comp CategoryTheory.coyoneda) ⟶ F) ≅ CategoryTheory.Limits.limit (D.unop.comp (F.comp CategoryTheory.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₁} [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.comp CategoryTheory.coyoneda)] [CategoryTheory.Limits.HasLimitsOfShape I (Type (max u₁ u₂))] (f : CategoryTheory.Limits.colimit (D.comp CategoryTheory.coyoneda) ⟶ F) (i : I) : CategoryTheory.Limits.limit.π (D.unop.comp (F.comp CategoryTheory.uliftFunctor.{u₁, u₂})) i ((CategoryTheory.Limits.colimitCoyonedaHomIsoLimitUnop D F).hom f) = { down := f.app (Opposite.unop (D.obj (Opposite.op i))) ((CategoryTheory.Limits.colimit.ι (D.comp CategoryTheory.coyoneda) (Opposite.op i)).app (Opposite.unop (D.obj (Opposite.op i))) (CategoryTheory.CategoryStruct.id (Opposite.unop (D.obj (Opposite.op i))))) }

noncomputable def CategoryTheory.Limits.colimitYonedaHomIsoLimit' {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.leftOp.comp CategoryTheory.yoneda)] [CategoryTheory.Limits.HasLimitsOfShape I (Type (max u₁ u₂))] : (CategoryTheory.Limits.colimit (D.leftOp.comp CategoryTheory.yoneda) ⟶ F) ≅ CategoryTheory.Limits.limit (D.comp (F.comp CategoryTheory.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₁} [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.leftOp.comp CategoryTheory.yoneda)] [CategoryTheory.Limits.HasLimitsOfShape I (Type (max u₁ u₂))] (f : CategoryTheory.Limits.colimit (D.leftOp.comp CategoryTheory.yoneda) ⟶ F) (i : I) : CategoryTheory.Limits.limit.π (D.comp (F.comp CategoryTheory.uliftFunctor.{u₁, u₂})) i ((CategoryTheory.Limits.colimitYonedaHomIsoLimit' D F).hom f) = { down := f.app (D.obj i) ((CategoryTheory.Limits.colimit.ι (D.leftOp.comp CategoryTheory.yoneda) (Opposite.op i)).app (D.obj i) (CategoryTheory.CategoryStruct.id (Opposite.unop (D.obj i)))) }

noncomputable def CategoryTheory.Limits.colimitYonedaHomIsoLimitRightOp {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.comp CategoryTheory.yoneda)] [CategoryTheory.Limits.HasLimitsOfShape I (Type (max u₁ u₂))] : (CategoryTheory.Limits.colimit (D.comp CategoryTheory.yoneda) ⟶ F) ≅ CategoryTheory.Limits.limit (D.rightOp.comp (F.comp CategoryTheory.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₁} [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.comp CategoryTheory.yoneda)] [CategoryTheory.Limits.HasLimitsOfShape I (Type (max u₁ u₂))] (f : CategoryTheory.Limits.colimit (D.comp CategoryTheory.yoneda) ⟶ F) (i : I) : CategoryTheory.Limits.limit.π (D.rightOp.comp (F.comp CategoryTheory.uliftFunctor.{u₁, u₂})) i ((CategoryTheory.Limits.colimitYonedaHomIsoLimitRightOp D F).hom f) = { down := f.app (Opposite.op (D.obj (Opposite.op i))) ((CategoryTheory.Limits.colimit.ι (D.comp CategoryTheory.yoneda) (Opposite.op i)).app (Opposite.op (D.obj (Opposite.op i))) (CategoryTheory.CategoryStruct.id (D.obj (Opposite.op i)))) }