Documentation

Mathlib.CategoryTheory.Limits.Opposites

Limits in C give colimits in Cᵒᵖ. #

We also give special cases for (co)products, (co)equalizers, and pullbacks / pushouts.

@[deprecated CategoryTheory.Limits.IsLimit.op]

Alias of CategoryTheory.Limits.IsLimit.op.


If t : Cone F is a limit cone, then t.op : Cocone F.op is a colimit cocone.

Equations
Instances For
    @[deprecated CategoryTheory.Limits.IsColimit.unop]

    Alias of CategoryTheory.Limits.IsColimit.unop.


    If t : Cocone F.op is a colimit cocone, then t.unop : Cone F. is a limit cone.

    Equations
    Instances For
      @[deprecated CategoryTheory.Limits.IsLimit.unop]

      Alias of CategoryTheory.Limits.IsLimit.unop.


      If t : Cone F.op is a limit cone, then t.unop : Cocone F is a colimit cocone.

      Equations
      Instances For

        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 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 limit of F.leftOp : Jᵒᵖ ⥤ C into a colimit of F : J ⥤ Cᵒᵖ.

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

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

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

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

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

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

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

                        If C has products indexed by X, then Cᵒᵖ has coproducts indexed by X.

                        Equations
                        • =

                        If C has coproducts indexed by X, then Cᵒᵖ has products indexed by X.

                        Equations
                        • =
                        Equations
                        • =
                        def CategoryTheory.Limits.Cofan.op {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : αC} (c : CategoryTheory.Limits.Cofan Z) :
                        CategoryTheory.Limits.Fan fun (x : α) => { unop := Z x }

                        A Cofan gives a Fan in the opposite category.

                        Equations
                        Instances For

                          If a Cofan is colimit, then its opposite is limit.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            def CategoryTheory.Limits.opCoproductIsoProduct' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : αC} {c : CategoryTheory.Limits.Cofan Z} {f : CategoryTheory.Limits.Fan fun (x : α) => { unop := Z x }} (hc : CategoryTheory.Limits.IsColimit c) (hf : CategoryTheory.Limits.IsLimit f) :
                            { unop := c.pt } f.pt

                            The canonical isomorphism from the opposite of an abstract coproduct to the corresponding product in the opposite category.

                            Equations
                            Instances For
                              def CategoryTheory.Limits.opCoproductIsoProduct {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} (Z : αC) [CategoryTheory.Limits.HasCoproduct Z] :
                              { unop := Z } fun (x : α) => { unop := Z x }

                              The canonical isomorphism from the opposite of the coproduct to the product in the opposite category.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                def CategoryTheory.Limits.Fan.op {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : αC} (f : CategoryTheory.Limits.Fan Z) :
                                CategoryTheory.Limits.Cofan fun (x : α) => { unop := Z x }

                                A Fan gives a Cofan in the opposite category.

                                Equations
                                Instances For

                                  If a Fan is limit, then its opposite is colimit.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For
                                    def CategoryTheory.Limits.opProductIsoCoproduct' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : αC} {f : CategoryTheory.Limits.Fan Z} {c : CategoryTheory.Limits.Cofan fun (x : α) => { unop := Z x }} (hf : CategoryTheory.Limits.IsLimit f) (hc : CategoryTheory.Limits.IsColimit c) :
                                    { unop := f.pt } c.pt

                                    The canonical isomorphism from the opposite of an abstract product to the corresponding coproduct in the opposite category.

                                    Equations
                                    Instances For
                                      def CategoryTheory.Limits.opProductIsoCoproduct {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} (Z : αC) [CategoryTheory.Limits.HasProduct Z] :
                                      { unop := Z } fun (x : α) => { unop := Z x }

                                      The canonical isomorphism from the opposite of the product to the coproduct in the opposite category.

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

                                        The canonical isomorphism relating Span f.op g.op and (Cospan f g).op

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

                                          The canonical isomorphism relating (Cospan f g).op and Span f.op g.op

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

                                            The canonical isomorphism relating Cospan f.op g.op and (Span f g).op

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

                                              The canonical isomorphism relating (Span f g).op and Cospan f.op g.op

                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                @[simp]
                                                theorem CategoryTheory.Limits.PushoutCocone.unop_pt {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} {f : X Y} {g : X Z} (c : CategoryTheory.Limits.PushoutCocone f g) :
                                                c.unop.pt = c.pt.unop

                                                The obvious map PushoutCocone f g → PullbackCone f.unop g.unop

                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  theorem CategoryTheory.Limits.PushoutCocone.unop_fst {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} {f : X Y} {g : X Z} (c : CategoryTheory.Limits.PushoutCocone f g) :
                                                  c.unop.fst = c.inl.unop
                                                  theorem CategoryTheory.Limits.PushoutCocone.unop_snd {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} {f : X Y} {g : X Z} (c : CategoryTheory.Limits.PushoutCocone f g) :
                                                  c.unop.snd = c.inr.unop
                                                  @[simp]
                                                  theorem CategoryTheory.Limits.PushoutCocone.op_pt {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} {f : X Y} {g : X Z} (c : CategoryTheory.Limits.PushoutCocone f g) :
                                                  c.op.pt = { unop := c.pt }

                                                  The obvious map PushoutCocone f.op g.op → PullbackCone f g

                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    theorem CategoryTheory.Limits.PushoutCocone.op_fst {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} {f : X Y} {g : X Z} (c : CategoryTheory.Limits.PushoutCocone f g) :
                                                    c.op.fst = c.inl.op
                                                    theorem CategoryTheory.Limits.PushoutCocone.op_snd {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} {f : X Y} {g : X Z} (c : CategoryTheory.Limits.PushoutCocone f g) :
                                                    c.op.snd = c.inr.op
                                                    @[simp]
                                                    theorem CategoryTheory.Limits.PullbackCone.unop_pt {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} {f : X Z} {g : Y Z} (c : CategoryTheory.Limits.PullbackCone f g) :
                                                    c.unop.pt = c.pt.unop

                                                    The obvious map PullbackCone f g → PushoutCocone f.unop g.unop

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      theorem CategoryTheory.Limits.PullbackCone.unop_inl {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} {f : X Z} {g : Y Z} (c : CategoryTheory.Limits.PullbackCone f g) :
                                                      c.unop.inl = c.fst.unop
                                                      theorem CategoryTheory.Limits.PullbackCone.unop_inr {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : Cᵒᵖ} {Y : Cᵒᵖ} {Z : Cᵒᵖ} {f : X Z} {g : Y Z} (c : CategoryTheory.Limits.PullbackCone f g) :
                                                      c.unop.inr = c.snd.unop
                                                      @[simp]
                                                      theorem CategoryTheory.Limits.PullbackCone.op_pt {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} {f : X Z} {g : Y Z} (c : CategoryTheory.Limits.PullbackCone f g) :
                                                      c.op.pt = { unop := c.pt }

                                                      The obvious map PullbackCone f g → PushoutCocone f.op g.op

                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        theorem CategoryTheory.Limits.PullbackCone.op_inl {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} {f : X Z} {g : Y Z} (c : CategoryTheory.Limits.PullbackCone f g) :
                                                        c.op.inl = c.fst.op
                                                        theorem CategoryTheory.Limits.PullbackCone.op_inr {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} {f : X Z} {g : Y Z} (c : CategoryTheory.Limits.PullbackCone f g) :
                                                        c.op.inr = c.snd.op
                                                        def CategoryTheory.Limits.PullbackCone.opUnop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} {f : X Z} {g : Y Z} (c : CategoryTheory.Limits.PullbackCone f g) :
                                                        c.op.unop c

                                                        If c is a pullback cone, then c.op.unop is isomorphic to c.

                                                        Equations
                                                        Instances For

                                                          If c is a pullback cone in Cᵒᵖ, then c.unop.op is isomorphic to c.

                                                          Equations
                                                          Instances For
                                                            def CategoryTheory.Limits.PushoutCocone.opUnop {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} {f : X Y} {g : X Z} (c : CategoryTheory.Limits.PushoutCocone f g) :
                                                            c.op.unop c

                                                            If c is a pushout cocone, then c.op.unop is isomorphic to c.

                                                            Equations
                                                            Instances For

                                                              If c is a pushout cocone in Cᵒᵖ, then c.unop.op is isomorphic to c.

                                                              Equations
                                                              Instances For

                                                                A pushout cone is a colimit cocone if and only if the corresponding pullback cone in the opposite category is a limit cone.

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

                                                                  A pushout cone is a colimit cocone in Cᵒᵖ if and only if the corresponding pullback cone in C is a limit cone.

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

                                                                    A pullback cone is a limit cone if and only if the corresponding pushout cocone in the opposite category is a colimit cocone.

                                                                    Equations
                                                                    Instances For

                                                                      A pullback cone is a limit cone in Cᵒᵖ if and only if the corresponding pushout cocone in C is a colimit cocone.

                                                                      Equations
                                                                      Instances For

                                                                        The pullback of f and g in C is isomorphic to the pushout of f.op and g.op in Cᵒᵖ.

                                                                        Equations
                                                                        • One or more equations did not get rendered due to their size.
                                                                        Instances For
                                                                          @[simp]
                                                                          @[simp]
                                                                          theorem CategoryTheory.Limits.pullbackIsoUnopPushout_inv_fst {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPushout f.op g.op] :
                                                                          CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackIsoUnopPushout f g).inv CategoryTheory.Limits.pullback.fst = CategoryTheory.Limits.pushout.inl.unop
                                                                          @[simp]
                                                                          @[simp]
                                                                          theorem CategoryTheory.Limits.pullbackIsoUnopPushout_inv_snd {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPushout f.op g.op] :
                                                                          CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackIsoUnopPushout f g).inv CategoryTheory.Limits.pullback.snd = CategoryTheory.Limits.pushout.inr.unop
                                                                          @[simp]
                                                                          theorem CategoryTheory.Limits.pullbackIsoUnopPushout_hom_inl {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPushout f.op g.op] :
                                                                          CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.pullbackIsoUnopPushout f g).hom.op = CategoryTheory.Limits.pullback.fst.op
                                                                          @[simp]
                                                                          theorem CategoryTheory.Limits.pullbackIsoUnopPushout_hom_inr {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} (f : X Z) (g : Y Z) [CategoryTheory.Limits.HasPullback f g] [CategoryTheory.Limits.HasPushout f.op g.op] :
                                                                          CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.pullbackIsoUnopPushout f g).hom.op = CategoryTheory.Limits.pullback.snd.op

                                                                          The pushout of f and g in C is isomorphic to the pullback of f.op and g.op in Cᵒᵖ.

                                                                          Equations
                                                                          • One or more equations did not get rendered due to their size.
                                                                          Instances For
                                                                            @[simp]
                                                                            theorem CategoryTheory.Limits.pushoutIsoUnopPullback_inl_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} (f : X Z) (g : X Y) [CategoryTheory.Limits.HasPushout f g] [CategoryTheory.Limits.HasPullback f.op g.op] :
                                                                            CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.pushoutIsoUnopPullback f g).hom = CategoryTheory.Limits.pullback.fst.unop
                                                                            @[simp]
                                                                            theorem CategoryTheory.Limits.pushoutIsoUnopPullback_inr_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} (f : X Z) (g : X Y) [CategoryTheory.Limits.HasPushout f g] [CategoryTheory.Limits.HasPullback f.op g.op] :
                                                                            CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.pushoutIsoUnopPullback f g).hom = CategoryTheory.Limits.pullback.snd.unop
                                                                            @[simp]
                                                                            theorem CategoryTheory.Limits.pushoutIsoUnopPullback_inv_fst {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} (f : X Z) (g : X Y) [CategoryTheory.Limits.HasPushout f g] [CategoryTheory.Limits.HasPullback f.op g.op] :
                                                                            CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutIsoUnopPullback f g).inv.op CategoryTheory.Limits.pullback.fst = CategoryTheory.Limits.pushout.inl.op
                                                                            @[simp]
                                                                            theorem CategoryTheory.Limits.pushoutIsoUnopPullback_inv_snd {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {X : C} {Y : C} {Z : C} (f : X Z) (g : X Y) [CategoryTheory.Limits.HasPushout f g] [CategoryTheory.Limits.HasPullback f.op g.op] :
                                                                            CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushoutIsoUnopPullback f g).inv.op CategoryTheory.Limits.pullback.snd = CategoryTheory.Limits.pushout.inr.op

                                                                            A colimit cokernel cofork gives a limit kernel fork in the opposite category

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

                                                                              A colimit cokernel cofork in the opposite category gives a limit kernel fork in the original category

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

                                                                                A limit kernel fork gives a colimit cokernel cofork in the opposite category

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

                                                                                  A limit kernel fork in the opposite category gives a colimit cokernel cofork in the original category

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