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.

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ᵒᵖ.

The isomorphism from the opposite of the coproduct to the product.

Instances For

    The isomorphism from the opposite of the product to the coproduct.

    Instances For

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

      Instances For

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

        Instances For

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

          Instances For

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

            Instances For

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

              Instances For

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

                Instances For

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

                  Instances For

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

                    Instances For

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

                      Instances For

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

                        Instances For

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

                          Instances For

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

                            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.

                              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.

                                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.

                                  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.

                                    Instances For

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

                                      Instances For
                                        @[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]
                                        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ᵒᵖ.

                                        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 in the opposite category gives a limit kernel fork in the original category

                                          Instances For

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

                                            Instances For