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 #

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

    limitOpIsoOpColimit for contravariant functor.

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

      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

        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

          Variant of coyonedaOoColimitIsoLimitCoyoneda for contravariant F.

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

            Variant of colimitHomIsoLimitYoneda for contravariant F.

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

              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

                A variant of colimitCoyonedaHomIsoLimit for a contravariant diagram.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[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))) }