Documentation

Mathlib.CategoryTheory.Limits.IndYoneda

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.

TODO #

source
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
  • ⋯ = ⋯
source
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.
Instances For
    source
    @[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
    source
    @[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
    source
    @[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
    source
    @[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)
    source
    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
    • ⋯ = ⋯
    source
    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.
    Instances For
      source
      @[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
      source
      @[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
      source
      @[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
      source
      @[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
      source
      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.
      Instances For
        source
        @[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
        source
        @[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
        source
        @[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
        source
        @[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)
        source
        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.
        Instances For
          source
          @[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
          source
          @[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
          source
          @[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
          source
          @[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)
          source
          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.
          Instances For
            source
            @[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
            source
            @[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
            source
            @[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
            source
            @[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
            source
            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.
            Instances For
              source
              @[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
              source
              @[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
              source
              @[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
              source
              @[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
              source
              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.
              Instances For
                source
                @[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)))) }
                source
                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.
                Instances For
                  source
                  @[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))) }