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 C] {I : Type v₁} [Category I] (F : Functor I C) [HasColimit F] : Iso (coyoneda.obj { unop := 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.

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

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

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

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

noncomputable def CategoryTheory.Limits.colimitHomIsoLimitYoneda {C : Type u₁} [Category C] {I : Type v₁} [Category I] (F : Functor I C) [HasColimit F] [HasLimitsOfShape (Opposite I) (Type u₂)] (A : C) : Iso (Quiver.Hom (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.

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

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

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

theorem CategoryTheory.Limits.colimitHomIsoLimitYoneda_inv_comp_π_assoc {C : Type u₁} [Category C] {I : Type v₁} [Category I] (F : Functor I C) [HasColimit F] [HasLimitsOfShape (Opposite I) (Type u₂)] (A : C) (i : I) {Z : Type u₂} (h : Quiver.Hom ((coyoneda.obj { unop := F.obj i }).obj A) Z) : Eq (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)) { unop := i }) h)

noncomputable def CategoryTheory.Limits.coyonedaOpColimitIsoLimitCoyoneda' {C : Type u₁} [Category C] {I : Type v₁} [Category I] (F : Functor (Opposite I) C) [HasColimit F] : Iso (coyoneda.obj { unop := 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.

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

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

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

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

noncomputable def CategoryTheory.Limits.colimitHomIsoLimitYoneda' {C : Type u₁} [Category C] {I : Type v₁} [Category I] (F : Functor (Opposite I) C) [HasColimit F] [HasLimitsOfShape I (Type u₂)] (A : C) : Iso (Quiver.Hom (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.

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

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

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

theorem CategoryTheory.Limits.colimitHomIsoLimitYoneda'_inv_comp_π_assoc {C : Type u₁} [Category C] {I : Type v₁} [Category I] (F : Functor (Opposite I) C) [HasColimit F] [HasLimitsOfShape I (Type u₂)] (A : C) (i : I) {Z : Type u₂} (h : Quiver.Hom ((coyoneda.obj { unop := F.obj { unop := i } }).obj A) Z) : Eq (CategoryStruct.comp (colimitHomIsoLimitYoneda' F A).inv (CategoryStruct.comp ((coyoneda.map (colimit.ι F { unop := 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 C] {I : Type v₁} [Category I] (D : Functor (Opposite I) C) (F : Functor C (Type u₂)) [HasColimit (D.rightOp.comp coyoneda)] [HasLimitsOfShape (Opposite I) (Type (max u₁ u₂))] : Iso (Quiver.Hom (colimit (D.rightOp.comp coyoneda)) F) (limit (D.comp (F.comp uliftFunctor)))

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.

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

noncomputable def CategoryTheory.Limits.colimitCoyonedaHomIsoLimitLeftOp {C : Type u₁} [Category C] {I : Type v₁} [Category I] (D : Functor I (Opposite C)) (F : Functor C (Type u₂)) [HasColimit (D.comp coyoneda)] [HasLimitsOfShape (Opposite I) (Type (max u₁ u₂))] : Iso (Quiver.Hom (colimit (D.comp coyoneda)) F) (limit (D.leftOp.comp (F.comp uliftFunctor)))

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

• Eq (CategoryTheory.Limits.colimitCoyonedaHomIsoLimitLeftOp D F) (CategoryTheory.Limits.colimitCoyonedaHomIsoLimit D.leftOp F)

theorem CategoryTheory.Limits.colimitCoyonedaHomIsoLimitLeftOp_π_apply {C : Type u₁} [Category C] {I : Type v₁} [Category I] (D : Functor I (Opposite C)) (F : Functor C (Type u₂)) [HasColimit (D.comp coyoneda)] [HasLimitsOfShape (Opposite I) (Type (max u₁ u₂))] (f : Quiver.Hom (colimit (D.comp coyoneda)) F) (i : I) : Eq (limit.π (D.leftOp.comp (F.comp uliftFunctor)) { unop := 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 C] {I : Type v₁} [Category I] (D : Functor (Opposite I) (Opposite C)) (F : Functor (Opposite C) (Type u₂)) [HasColimit (D.unop.comp yoneda)] [HasLimitsOfShape (Opposite I) (Type (max u₁ u₂))] : Iso (Quiver.Hom (colimit (D.unop.comp yoneda)) F) (limit (D.comp (F.comp uliftFunctor)))

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.

theorem CategoryTheory.Limits.colimitYonedaHomIsoLimit_π_apply {C : Type u₁} [Category C] {I : Type v₁} [Category I] (D : Functor (Opposite I) (Opposite C)) (F : Functor (Opposite C) (Type u₂)) [HasColimit (D.unop.comp yoneda)] [HasLimitsOfShape (Opposite I) (Type (max u₁ u₂))] (f : Quiver.Hom (colimit (D.unop.comp yoneda)) F) (i : Opposite I) : Eq (limit.π (D.comp (F.comp uliftFunctor)) 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 C] {I : Type v₁} [Category I] (D : Functor I C) (F : Functor (Opposite C) (Type u₂)) [HasColimit (D.comp yoneda)] [HasLimitsOfShape (Opposite I) (Type (max u₁ u₂))] : Iso (Quiver.Hom (colimit (D.comp yoneda)) F) (limit (D.op.comp (F.comp uliftFunctor)))

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

• Eq (CategoryTheory.Limits.colimitYonedaHomIsoLimitOp D F) (CategoryTheory.Limits.colimitYonedaHomIsoLimit D.op F)

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

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

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.

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

noncomputable def CategoryTheory.Limits.colimitCoyonedaHomIsoLimitUnop {C : Type u₁} [Category C] {I : Type v₁} [Category I] (D : Functor (Opposite I) (Opposite C)) (F : Functor C (Type u₂)) [HasColimit (D.comp coyoneda)] [HasLimitsOfShape I (Type (max u₁ u₂))] : Iso (Quiver.Hom (colimit (D.comp coyoneda)) F) (limit (D.unop.comp (F.comp uliftFunctor)))

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

• Eq (CategoryTheory.Limits.colimitCoyonedaHomIsoLimitUnop D F) (CategoryTheory.Limits.colimitCoyonedaHomIsoLimit' D.unop F)

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

noncomputable def CategoryTheory.Limits.colimitYonedaHomIsoLimit' {C : Type u₁} [Category C] {I : Type v₁} [Category I] (D : Functor I (Opposite C)) (F : Functor (Opposite C) (Type u₂)) [HasColimit (D.leftOp.comp yoneda)] [HasLimitsOfShape I (Type (max u₁ u₂))] : Iso (Quiver.Hom (colimit (D.leftOp.comp yoneda)) F) (limit (D.comp (F.comp uliftFunctor)))

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.

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

noncomputable def CategoryTheory.Limits.colimitYonedaHomIsoLimitRightOp {C : Type u₁} [Category C] {I : Type v₁} [Category I] (D : Functor (Opposite I) C) (F : Functor (Opposite C) (Type u₂)) [HasColimit (D.comp yoneda)] [HasLimitsOfShape I (Type (max u₁ u₂))] : Iso (Quiver.Hom (colimit (D.comp yoneda)) F) (limit (D.rightOp.comp (F.comp uliftFunctor)))

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

• Eq (CategoryTheory.Limits.colimitYonedaHomIsoLimitRightOp D F) (CategoryTheory.Limits.colimitYonedaHomIsoLimit' D.rightOp F)

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