Documentation

Mathlib.CategoryTheory.Limits.Preserves.Shapes.BinaryProducts

Preserving binary products #

Constructions to relate the notions of preserving binary products and reflecting binary products to concrete binary fans.

In particular, we show that ProdComparison G X Y is an isomorphism iff G preserves the product of X and Y.

def CategoryTheory.Limits.isLimitMapConeBinaryFanEquiv {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {P X Y : C} (f : P X) (g : P Y) :

The map of a binary fan is a limit iff the fork consisting of the mapped morphisms is a limit. This essentially lets us commute BinaryFan.mk with Functor.mapCone.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    def CategoryTheory.Limits.mapIsLimitOfPreservesOfIsLimit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {P X Y : C} (f : P X) (g : P Y) [PreservesLimit (pair X Y) G] (l : IsLimit (BinaryFan.mk f g)) :
    IsLimit (BinaryFan.mk (G.map f) (G.map g))

    The property of preserving products expressed in terms of binary fans.

    Equations
    Instances For
      def CategoryTheory.Limits.isLimitOfReflectsOfMapIsLimit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {P X Y : C} (f : P X) (g : P Y) [ReflectsLimit (pair X Y) G] (l : IsLimit (BinaryFan.mk (G.map f) (G.map g))) :

      The property of reflecting products expressed in terms of binary fans.

      Equations
      Instances For

        If G preserves binary products and C has them, then the binary fan constructed of the mapped morphisms of the binary product cone is a limit.

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

          If the product comparison map for G at (X,Y) is an isomorphism, then G preserves the pair of (X,Y).

          def CategoryTheory.Limits.PreservesLimitPair.iso {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) (X Y : C) [HasBinaryProduct X Y] [HasBinaryProduct (G.obj X) (G.obj Y)] [PreservesLimit (pair X Y) G] :
          G.obj (X Y) G.obj X G.obj Y

          If G preserves the product of (X,Y), then the product comparison map for G at (X,Y) is an isomorphism.

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

            If the product comparison maps of G at every pair (X,Y) is an isomorphism, then G preserves binary products.

            The map of a binary cofan is a colimit iff the cofork consisting of the mapped morphisms is a colimit. This essentially lets us commute BinaryCofan.mk with Functor.mapCocone.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              def CategoryTheory.Limits.mapIsColimitOfPreservesOfIsColimit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {P X Y : C} (f : X P) (g : Y P) [PreservesColimit (pair X Y) G] (l : IsColimit (BinaryCofan.mk f g)) :

              The property of preserving coproducts expressed in terms of binary cofans.

              Equations
              Instances For
                def CategoryTheory.Limits.isColimitOfReflectsOfMapIsColimit {C : Type u₁} [Category.{v₁, u₁} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) {P X Y : C} (f : X P) (g : Y P) [ReflectsColimit (pair X Y) G] (l : IsColimit (BinaryCofan.mk (G.map f) (G.map g))) :

                The property of reflecting coproducts expressed in terms of binary cofans.

                Equations
                Instances For

                  If G preserves binary coproducts and C has them, then the binary cofan constructed of the mapped morphisms of the binary product cocone is a colimit.

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

                    If the coproduct comparison map for G at (X,Y) is an isomorphism, then G preserves the pair of (X,Y).

                    If G preserves the coproduct of (X,Y), then the coproduct comparison map for G at (X,Y) is an isomorphism.

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

                      If the coproduct comparison maps of G at every pair (X,Y) is an isomorphism, then G preserves binary coproducts.