Documentation

Mathlib.CategoryTheory.Limits.Opposites

Limits in C give colimits in Cᵒᵖ. #

We construct limits and colimits in the opposite categories.

Turn a colimit for F : J ⥤ Cᵒᵖ into a limit for F.leftOp : Jᵒᵖ ⥤ C.

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

    Turn a limit of F : J ⥤ Cᵒᵖ into a colimit of F.leftOp : Jᵒᵖ ⥤ C.

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

      Turn a colimit for F : Jᵒᵖ ⥤ C into a limit for F.rightOp : J ⥤ Cᵒᵖ.

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

        Turn a limit for F : Jᵒᵖ ⥤ C into a colimit for F.rightOp : J ⥤ Cᵒᵖ.

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

          Turn a colimit for F : Jᵒᵖ ⥤ Cᵒᵖ into a limit for F.unop : J ⥤ C.

          Equations
          Instances For

            Turn a limit of F : Jᵒᵖ ⥤ Cᵒᵖ into a colimit of F.unop : J ⥤ C.

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

              Turn a colimit for F.leftOp : Jᵒᵖ ⥤ C into a limit for F : J ⥤ Cᵒᵖ.

              Equations
              Instances For

                Turn a limit of F.leftOp : Jᵒᵖ ⥤ C into a colimit of F : J ⥤ Cᵒᵖ.

                Equations
                Instances For

                  Turn a colimit for F.rightOp : J ⥤ Cᵒᵖ into a limit for F : Jᵒᵖ ⥤ C.

                  Equations
                  Instances For

                    Turn a limit for F.rightOp : J ⥤ Cᵒᵖ into a colimit for F : Jᵒᵖ ⥤ C.

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

                      Turn a colimit for F.unop : J ⥤ C into a limit for F : Jᵒᵖ ⥤ Cᵒᵖ.

                      Equations
                      Instances For

                        Turn a limit for F.unop : J ⥤ C into a colimit for F : Jᵒᵖ ⥤ Cᵒᵖ.

                        Equations
                        Instances For

                          Turn a limit for F.leftOp : Jᵒᵖ ⥤ C into a colimit for F : J ⥤ Cᵒᵖ.

                          Equations
                          Instances For

                            Turn a colimit for F.leftOp : Jᵒᵖ ⥤ C into a limit for F : J ⥤ Cᵒᵖ.

                            Equations
                            Instances For

                              Turn a limit for F.rightOp : J ⥤ Cᵒᵖ into a colimit for F : Jᵒᵖ ⥤ C.

                              Equations
                              Instances For

                                Turn a colimit for F.rightOp : J ⥤ Cᵒᵖ into a limit for F : Jᵒᵖ ⥤ C.

                                Equations
                                Instances For

                                  Turn a limit for F.unop : J ⥤ C into a colimit for F : Jᵒᵖ ⥤ Cᵒᵖ.

                                  Equations
                                  Instances For

                                    Turn a colimit for F.unop : J ⥤ C into a limit for F : Jᵒᵖ ⥤ Cᵒᵖ.

                                    Equations
                                    Instances For

                                      Turn a limit for F : J ⥤ Cᵒᵖ into a colimit for F.leftOp : Jᵒᵖ ⥤ C.

                                      Equations
                                      Instances For

                                        Turn a colimit for F : J ⥤ Cᵒᵖ into a limit for F.leftOp : Jᵒᵖ ⥤ C.

                                        Equations
                                        Instances For

                                          Turn a limit for F : Jᵒᵖ ⥤ C into a colimit for F.rightOp : J ⥤ Cᵒᵖ.

                                          Equations
                                          Instances For

                                            Turn a colimit for F : Jᵒᵖ ⥤ C into a limit for F.rightOp : J ⥤ Cᵒᵖ.

                                            Equations
                                            Instances For

                                              Turn a limit for F : Jᵒᵖ ⥤ Cᵒᵖ into a colimit for F.unop : J ⥤ C.

                                              Equations
                                              Instances For

                                                Turn a colimit for F : Jᵒᵖ ⥤ Cᵒᵖ into a limit for F.unop : J ⥤ C.

                                                Equations
                                                Instances For

                                                  If F.leftOp : Jᵒᵖ ⥤ C has a colimit, we can construct a limit for F : J ⥤ Cᵒᵖ.

                                                  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

                                                    The limit of F.leftOp is the unopposite of colimit F.

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

                                                      The limit of F.rightOp is the opposite of colimit F.

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

                                                        The limit of F.unop is the unopposite of colimit F.

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

                                                          If C has colimits of shape Jᵒᵖ, we can construct limits in Cᵒᵖ of shape J.

                                                          If F.leftOp : Jᵒᵖ ⥤ C has a limit, we can construct a colimit for F : J ⥤ Cᵒᵖ.

                                                          The colimit of F.op is the opposite of limit F.

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

                                                            The colimit of F.leftOp is the unopposite of limit F.

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

                                                              The colimit of F.rightOp is the opposite of limit F.

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

                                                                The colimit of F.unop is the unopposite of limit F.

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

                                                                  If C has colimits of shape Jᵒᵖ, we can construct limits in Cᵒᵖ of shape J.