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 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
                    • =

                    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

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

                        Equations
                        Instances For

                          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

                            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

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

                                Equations
                                Instances For

                                  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 from the opposite of the binary product to the coproduct in the opposite category.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      @[simp]
                                      @[simp]
                                      @[simp]
                                      @[simp]
                                      @[simp]
                                      theorem CategoryTheory.Limits.opProdIsoCoprod_hom_fst {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : C} {B : C} [CategoryTheory.Limits.HasBinaryProduct A B] :
                                      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProdIsoCoprod A B).hom.unop CategoryTheory.Limits.prod.fst = CategoryTheory.Limits.coprod.inl.unop
                                      @[simp]
                                      theorem CategoryTheory.Limits.opProdIsoCoprod_hom_snd {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : C} {B : C} [CategoryTheory.Limits.HasBinaryProduct A B] :
                                      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProdIsoCoprod A B).hom.unop CategoryTheory.Limits.prod.snd = CategoryTheory.Limits.coprod.inr.unop
                                      @[simp]
                                      theorem CategoryTheory.Limits.opProdIsoCoprod_inv_inl {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : C} {B : C} [CategoryTheory.Limits.HasBinaryProduct A B] :
                                      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProdIsoCoprod A B).inv.unop CategoryTheory.Limits.coprod.inl.unop = CategoryTheory.Limits.prod.fst
                                      @[simp]
                                      theorem CategoryTheory.Limits.opProdIsoCoprod_inv_inr {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {A : C} {B : C} [CategoryTheory.Limits.HasBinaryProduct A B] :
                                      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.opProdIsoCoprod A B).inv.unop CategoryTheory.Limits.coprod.inr.unop = CategoryTheory.Limits.prod.snd

                                      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]

                                              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 = Opposite.op 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]

                                                  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 = Opposite.op 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

                                                                        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

                                                                          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