Documentation

Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Binary (co)products #

We define a category WalkingPair, which is the index category for a binary (co)product diagram. A convenience method pair X Y constructs the functor from the walking pair, hitting the given objects.

We define prod X Y and coprod X Y as limits and colimits of such functors.

Typeclasses HasBinaryProducts and HasBinaryCoproducts assert the existence of (co)limits shaped as walking pairs.

We include lemmas for simplifying equations involving projections and coprojections, and define braiding and associating isomorphisms, and the product comparison morphism.

References #

The type of objects for the diagram indexing a binary (co)product.

Instances For

    The equivalence swapping left and right.

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

      An equivalence from WalkingPair to Bool, sometimes useful when reindexing limits.

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

        The function on the walking pair, sending the two points to X and Y.

        Equations
        Instances For

          The natural transformation between two functors out of the walking pair, specified by its components.

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

            The natural isomorphism between two functors out of the walking pair, specified by its components.

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

              Every functor out of the walking pair is naturally isomorphic (actually, equal) to a pair

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

                The natural isomorphism between pair X Y ⋙ F and pair (F.obj X) (F.obj Y).

                Equations
                Instances For
                  @[reducible, inline]
                  abbrev CategoryTheory.Limits.BinaryFan {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) (Y : C) :
                  Type (max u v)

                  A binary fan is just a cone on a diagram indexing a product.

                  Equations
                  Instances For
                    def CategoryTheory.Limits.BinaryFan.IsLimit.mk {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (s : CategoryTheory.Limits.BinaryFan X Y) (lift : {T : C} → (T X)(T Y)(T s.pt)) (hl₁ : ∀ {T : C} (f : T X) (g : T Y), CategoryTheory.CategoryStruct.comp (lift f g) s.fst = f) (hl₂ : ∀ {T : C} (f : T X) (g : T Y), CategoryTheory.CategoryStruct.comp (lift f g) s.snd = g) (uniq : ∀ {T : C} (f : T X) (g : T Y) (m : T s.pt), CategoryTheory.CategoryStruct.comp m s.fst = fCategoryTheory.CategoryStruct.comp m s.snd = gm = lift f g) :

                    A convenient way to show that a binary fan is a limit.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      @[reducible, inline]
                      abbrev CategoryTheory.Limits.BinaryCofan {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) (Y : C) :
                      Type (max u v)

                      A binary cofan is just a cocone on a diagram indexing a coproduct.

                      Equations
                      Instances For
                        def CategoryTheory.Limits.BinaryCofan.IsColimit.mk {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} (s : CategoryTheory.Limits.BinaryCofan X Y) (desc : {T : C} → (X T)(Y T)(s.pt T)) (hd₁ : ∀ {T : C} (f : X T) (g : Y T), CategoryTheory.CategoryStruct.comp s.inl (desc f g) = f) (hd₂ : ∀ {T : C} (f : X T) (g : Y T), CategoryTheory.CategoryStruct.comp s.inr (desc f g) = g) (uniq : ∀ {T : C} (f : X T) (g : Y T) (m : s.pt T), CategoryTheory.CategoryStruct.comp s.inl m = fCategoryTheory.CategoryStruct.comp s.inr m = gm = desc f g) :

                        A convenient way to show that a binary cofan is a colimit.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          @[simp]
                          theorem CategoryTheory.Limits.BinaryFan.mk_pt {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {P : C} (π₁ : P X) (π₂ : P Y) :
                          def CategoryTheory.Limits.BinaryFan.mk {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {P : C} (π₁ : P X) (π₂ : P Y) :

                          A binary fan with vertex P consists of the two projections π₁ : P ⟶ X and π₂ : P ⟶ Y.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            @[simp]
                            theorem CategoryTheory.Limits.BinaryCofan.mk_pt {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {P : C} (ι₁ : X P) (ι₂ : Y P) :
                            def CategoryTheory.Limits.BinaryCofan.mk {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {P : C} (ι₁ : X P) (ι₂ : Y P) :

                            A binary cofan with vertex P consists of the two inclusions ι₁ : X ⟶ P and ι₂ : Y ⟶ P.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              @[simp]
                              theorem CategoryTheory.Limits.BinaryFan.mk_fst {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {P : C} (π₁ : P X) (π₂ : P Y) :
                              (CategoryTheory.Limits.BinaryFan.mk π₁ π₂).fst = π₁
                              @[simp]
                              theorem CategoryTheory.Limits.BinaryFan.mk_snd {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {P : C} (π₁ : P X) (π₂ : P Y) :
                              (CategoryTheory.Limits.BinaryFan.mk π₁ π₂).snd = π₂
                              @[simp]
                              theorem CategoryTheory.Limits.BinaryCofan.mk_inl {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {P : C} (ι₁ : X P) (ι₂ : Y P) :
                              (CategoryTheory.Limits.BinaryCofan.mk ι₁ ι₂).inl = ι₁
                              @[simp]
                              theorem CategoryTheory.Limits.BinaryCofan.mk_inr {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {P : C} (ι₁ : X P) (ι₂ : Y P) :
                              (CategoryTheory.Limits.BinaryCofan.mk ι₁ ι₂).inr = ι₂
                              def CategoryTheory.Limits.BinaryFan.isLimitMk {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {W : C} {fst : W X} {snd : W Y} (lift : (s : CategoryTheory.Limits.BinaryFan X Y) → s.pt W) (fac_left : ∀ (s : CategoryTheory.Limits.BinaryFan X Y), CategoryTheory.CategoryStruct.comp (lift s) fst = s.fst) (fac_right : ∀ (s : CategoryTheory.Limits.BinaryFan X Y), CategoryTheory.CategoryStruct.comp (lift s) snd = s.snd) (uniq : ∀ (s : CategoryTheory.Limits.BinaryFan X Y) (m : s.pt W), CategoryTheory.CategoryStruct.comp m fst = s.fstCategoryTheory.CategoryStruct.comp m snd = s.sndm = lift s) :

                              This is a more convenient formulation to show that a BinaryFan constructed using BinaryFan.mk is a limit cone.

                              Equations
                              Instances For
                                def CategoryTheory.Limits.BinaryCofan.isColimitMk {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {W : C} {inl : X W} {inr : Y W} (desc : (s : CategoryTheory.Limits.BinaryCofan X Y) → W s.pt) (fac_left : ∀ (s : CategoryTheory.Limits.BinaryCofan X Y), CategoryTheory.CategoryStruct.comp inl (desc s) = s.inl) (fac_right : ∀ (s : CategoryTheory.Limits.BinaryCofan X Y), CategoryTheory.CategoryStruct.comp inr (desc s) = s.inr) (uniq : ∀ (s : CategoryTheory.Limits.BinaryCofan X Y) (m : W s.pt), CategoryTheory.CategoryStruct.comp inl m = s.inlCategoryTheory.CategoryStruct.comp inr m = s.inrm = desc s) :

                                This is a more convenient formulation to show that a BinaryCofan constructed using BinaryCofan.mk is a colimit cocone.

                                Equations
                                Instances For

                                  If s is a limit binary fan over X and Y, then every pair of morphisms f : W ⟶ X and g : W ⟶ Y induces a morphism l : W ⟶ s.pt satisfying l ≫ s.fst = f and l ≫ s.snd = g.

                                  Equations
                                  Instances For

                                    If s is a colimit binary cofan over X and Y,, then every pair of morphisms f : X ⟶ W and g : Y ⟶ W induces a morphism l : s.pt ⟶ W satisfying s.inl ≫ l = f and s.inr ≫ l = g.

                                    Equations
                                    Instances For

                                      Binary products are symmetric.

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

                                        If X' ≅ X, then X × Y also is the product of X' and Y.

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

                                          If Y' ≅ Y, then X x Y also is the product of X and Y'.

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

                                            Binary coproducts are symmetric.

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

                                              If X' ≅ X, then X ⨿ Y also is the coproduct of X' and Y.

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

                                                If Y' ≅ Y, then X ⨿ Y also is the coproduct of X and Y'.

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

                                                  An abbreviation for HasLimit (pair X Y).

                                                  Equations
                                                  Instances For
                                                    @[reducible, inline]

                                                    An abbreviation for HasColimit (pair X Y).

                                                    Equations
                                                    Instances For
                                                      @[reducible, inline]

                                                      If we have a product of X and Y, we can access it using prod X Y or X ⨯ Y.

                                                      Equations
                                                      Instances For
                                                        @[reducible, inline]

                                                        If we have a coproduct of X and Y, we can access it using coprod X Y or X ⨿ Y.

                                                        Equations
                                                        Instances For

                                                          Notation for the product

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

                                                            Notation for the coproduct

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

                                                              The projection map to the first component of the product.

                                                              Equations
                                                              Instances For
                                                                @[reducible, inline]

                                                                The projection map to the second component of the product.

                                                                Equations
                                                                Instances For
                                                                  @[reducible, inline]

                                                                  The inclusion map from the first component of the coproduct.

                                                                  Equations
                                                                  Instances For
                                                                    @[reducible, inline]

                                                                    The inclusion map from the second component of the coproduct.

                                                                    Equations
                                                                    Instances For

                                                                      The binary fan constructed from the projection maps is a limit.

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

                                                                        The binary cofan constructed from the coprojection maps is a colimit.

                                                                        Equations
                                                                        • One or more equations did not get rendered due to their size.
                                                                        Instances For
                                                                          theorem CategoryTheory.Limits.prod.hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} [CategoryTheory.Limits.HasBinaryProduct X Y] {f : W X Y} {g : W X Y} (h₁ : CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.prod.fst = CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.prod.fst) (h₂ : CategoryTheory.CategoryStruct.comp f CategoryTheory.Limits.prod.snd = CategoryTheory.CategoryStruct.comp g CategoryTheory.Limits.prod.snd) :
                                                                          f = g
                                                                          theorem CategoryTheory.Limits.coprod.hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} [CategoryTheory.Limits.HasBinaryCoproduct X Y] {f : X ⨿ Y W} {g : X ⨿ Y W} (h₁ : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl f = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl g) (h₂ : CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr f = CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr g) :
                                                                          f = g
                                                                          @[reducible, inline]
                                                                          abbrev CategoryTheory.Limits.prod.lift {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} [CategoryTheory.Limits.HasBinaryProduct X Y] (f : W X) (g : W Y) :
                                                                          W X Y

                                                                          If the product of X and Y exists, then every pair of morphisms f : W ⟶ X and g : W ⟶ Y induces a morphism prod.lift f g : W ⟶ X ⨯ Y.

                                                                          Equations
                                                                          Instances For
                                                                            @[reducible, inline]

                                                                            diagonal arrow of the binary product in the category fam I

                                                                            Equations
                                                                            Instances For
                                                                              @[reducible, inline]
                                                                              abbrev CategoryTheory.Limits.coprod.desc {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} [CategoryTheory.Limits.HasBinaryCoproduct X Y] (f : X W) (g : Y W) :
                                                                              X ⨿ Y W

                                                                              If the coproduct of X and Y exists, then every pair of morphisms f : X ⟶ W and g : Y ⟶ W induces a morphism coprod.desc f g : X ⨿ Y ⟶ W.

                                                                              Equations
                                                                              Instances For
                                                                                def CategoryTheory.Limits.prod.lift' {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} [CategoryTheory.Limits.HasBinaryProduct X Y] (f : W X) (g : W Y) :
                                                                                { l : W X Y // CategoryTheory.CategoryStruct.comp l CategoryTheory.Limits.prod.fst = f CategoryTheory.CategoryStruct.comp l CategoryTheory.Limits.prod.snd = g }

                                                                                If the product of X and Y exists, then every pair of morphisms f : W ⟶ X and g : W ⟶ Y induces a morphism l : W ⟶ X ⨯ Y satisfying l ≫ Prod.fst = f and l ≫ Prod.snd = g.

                                                                                Equations
                                                                                Instances For
                                                                                  def CategoryTheory.Limits.coprod.desc' {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} [CategoryTheory.Limits.HasBinaryCoproduct X Y] (f : X W) (g : Y W) :
                                                                                  { l : X ⨿ Y W // CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl l = f CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr l = g }

                                                                                  If the coproduct of X and Y exists, then every pair of morphisms f : X ⟶ W and g : Y ⟶ W induces a morphism l : X ⨿ Y ⟶ W satisfying coprod.inl ≫ l = f and coprod.inr ≫ l = g.

                                                                                  Equations
                                                                                  Instances For

                                                                                    If the products W ⨯ X and Y ⨯ Z exist, then every pair of morphisms f : W ⟶ Y and g : X ⟶ Z induces a morphism prod.map f g : W ⨯ X ⟶ Y ⨯ Z.

                                                                                    Equations
                                                                                    Instances For

                                                                                      If the coproducts W ⨿ X and Y ⨿ Z exist, then every pair of morphisms f : W ⟶ Y and g : W ⟶ Z induces a morphism coprod.map f g : W ⨿ X ⟶ Y ⨿ Z.

                                                                                      Equations
                                                                                      Instances For
                                                                                        @[simp]
                                                                                        @[simp]
                                                                                        @[simp]

                                                                                        If the products W ⨯ X and Y ⨯ Z exist, then every pair of isomorphisms f : W ≅ Y and g : X ≅ Z induces an isomorphism prod.mapIso f g : W ⨯ X ≅ Y ⨯ Z.

                                                                                        Equations
                                                                                        Instances For
                                                                                          @[simp]
                                                                                          @[simp]
                                                                                          @[simp]

                                                                                          If the coproducts W ⨿ X and Y ⨿ Z exist, then every pair of isomorphisms f : W ≅ Y and g : W ≅ Z induces an isomorphism coprod.mapIso f g : W ⨿ X ≅ Y ⨿ Z.

                                                                                          Equations
                                                                                          Instances For

                                                                                            The braiding isomorphism which swaps a binary product.

                                                                                            Equations
                                                                                            • One or more equations did not get rendered due to their size.
                                                                                            Instances For
                                                                                              theorem CategoryTheory.Limits.prod.symmetry'_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] (P : C) (Q : C) [CategoryTheory.Limits.HasBinaryProduct P Q] [CategoryTheory.Limits.HasBinaryProduct Q P] {Z : C} (h : P Q Z) :
                                                                                              CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst) h) = h
                                                                                              theorem CategoryTheory.Limits.prod.symmetry' {C : Type u} [CategoryTheory.Category.{v, u} C] (P : C) (Q : C) [CategoryTheory.Limits.HasBinaryProduct P Q] [CategoryTheory.Limits.HasBinaryProduct Q P] :
                                                                                              CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst) (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst) = CategoryTheory.CategoryStruct.id (P Q)
                                                                                              @[simp]
                                                                                              theorem CategoryTheory.Limits.prod.associator_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] (P : C) (Q : C) (R : C) :
                                                                                              (CategoryTheory.Limits.prod.associator P Q R).hom = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.fst) (CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst CategoryTheory.Limits.prod.snd) CategoryTheory.Limits.prod.snd)
                                                                                              @[simp]
                                                                                              theorem CategoryTheory.Limits.prod.associator_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] (P : C) (Q : C) (R : C) :
                                                                                              (CategoryTheory.Limits.prod.associator P Q R).inv = CategoryTheory.Limits.prod.lift (CategoryTheory.Limits.prod.lift CategoryTheory.Limits.prod.fst (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.fst)) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd CategoryTheory.Limits.prod.snd)

                                                                                              The associator isomorphism for binary products.

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

                                                                                                The left unitor isomorphism for binary products with the terminal object.

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

                                                                                                  The right unitor isomorphism for binary products with the terminal object.

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

                                                                                                    The braiding isomorphism which swaps a binary coproduct.

                                                                                                    Equations
                                                                                                    • One or more equations did not get rendered due to their size.
                                                                                                    Instances For
                                                                                                      theorem CategoryTheory.Limits.coprod.symmetry'_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] (P : C) (Q : C) {Z : C} (h : P ⨿ Q Z) :
                                                                                                      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inl) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inl) h) = h
                                                                                                      theorem CategoryTheory.Limits.coprod.symmetry' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] (P : C) (Q : C) :
                                                                                                      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inl) (CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inl) = CategoryTheory.CategoryStruct.id (P ⨿ Q)
                                                                                                      @[simp]
                                                                                                      theorem CategoryTheory.Limits.coprod.associator_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] (P : C) (Q : C) (R : C) :
                                                                                                      (CategoryTheory.Limits.coprod.associator P Q R).hom = CategoryTheory.Limits.coprod.desc (CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inl (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inr)) (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inr)
                                                                                                      @[simp]
                                                                                                      theorem CategoryTheory.Limits.coprod.associator_inv {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] (P : C) (Q : C) (R : C) :
                                                                                                      (CategoryTheory.Limits.coprod.associator P Q R).inv = CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inl) (CategoryTheory.Limits.coprod.desc (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inl) CategoryTheory.Limits.coprod.inr)

                                                                                                      The associator isomorphism for binary coproducts.

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

                                                                                                        The left unitor isomorphism for binary coproducts with the initial object.

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

                                                                                                          The right unitor isomorphism for binary coproducts with the initial object.

                                                                                                          Equations
                                                                                                          • One or more equations did not get rendered due to their size.
                                                                                                          Instances For
                                                                                                            @[simp]
                                                                                                            @[simp]
                                                                                                            theorem CategoryTheory.Limits.prod.functor_obj_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] (X : C) (Y : C) :
                                                                                                            (CategoryTheory.Limits.prod.functor.obj X).obj Y = (X Y)
                                                                                                            @[simp]
                                                                                                            theorem CategoryTheory.Limits.prod.functor_obj_map {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] (X : C) {Y : C} {Z : C} (g : Y Z) :
                                                                                                            (CategoryTheory.Limits.prod.functor.obj X).map g = CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.id X) g

                                                                                                            The binary product functor.

                                                                                                            Equations
                                                                                                            • One or more equations did not get rendered due to their size.
                                                                                                            Instances For
                                                                                                              def CategoryTheory.Limits.prod.functorLeftComp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryProducts C] (X : C) (Y : C) :
                                                                                                              CategoryTheory.Limits.prod.functor.obj (X Y) (CategoryTheory.Limits.prod.functor.obj Y).comp (CategoryTheory.Limits.prod.functor.obj X)

                                                                                                              The product functor can be decomposed.

                                                                                                              Equations
                                                                                                              Instances For
                                                                                                                @[simp]
                                                                                                                @[simp]
                                                                                                                @[simp]
                                                                                                                theorem CategoryTheory.Limits.coprod.functor_obj_obj {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] (X : C) (Y : C) :
                                                                                                                (CategoryTheory.Limits.coprod.functor.obj X).obj Y = (X ⨿ Y)

                                                                                                                The binary coproduct functor.

                                                                                                                Equations
                                                                                                                • One or more equations did not get rendered due to their size.
                                                                                                                Instances For
                                                                                                                  def CategoryTheory.Limits.coprod.functorLeftComp {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasBinaryCoproducts C] (X : C) (Y : C) :
                                                                                                                  CategoryTheory.Limits.coprod.functor.obj (X ⨿ Y) (CategoryTheory.Limits.coprod.functor.obj Y).comp (CategoryTheory.Limits.coprod.functor.obj X)

                                                                                                                  The coproduct functor can be decomposed.

                                                                                                                  Equations
                                                                                                                  Instances For

                                                                                                                    The product comparison morphism.

                                                                                                                    In CategoryTheory/Limits/Preserves we show this is always an iso iff F preserves binary products.

                                                                                                                    Equations
                                                                                                                    Instances For
                                                                                                                      def CategoryTheory.Limits.prodComparisonNatTrans {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasBinaryProducts D] (F : CategoryTheory.Functor C D) (A : C) :
                                                                                                                      (CategoryTheory.Limits.prod.functor.obj A).comp F F.comp (CategoryTheory.Limits.prod.functor.obj (F.obj A))

                                                                                                                      The product comparison morphism from F(A ⨯ -) to FA ⨯ F-, whose components are given by prodComparison.

                                                                                                                      Equations
                                                                                                                      Instances For
                                                                                                                        def CategoryTheory.Limits.prodComparisonNatIso {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasBinaryProducts D] (A : C) [∀ (B : C), CategoryTheory.IsIso (CategoryTheory.Limits.prodComparison F A B)] :
                                                                                                                        (CategoryTheory.Limits.prod.functor.obj A).comp F F.comp (CategoryTheory.Limits.prod.functor.obj (F.obj A))

                                                                                                                        The natural isomorphism F(A ⨯ -) ≅ FA ⨯ F-, provided each prodComparison F A B is an isomorphism (as B changes).

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

                                                                                                                          The coproduct comparison morphism.

                                                                                                                          In CategoryTheory/Limits/Preserves we show this is always an iso iff F preserves binary coproducts.

                                                                                                                          Equations
                                                                                                                          Instances For
                                                                                                                            def CategoryTheory.Limits.coprodComparisonNatTrans {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{w, u₂} D] [CategoryTheory.Limits.HasBinaryCoproducts C] [CategoryTheory.Limits.HasBinaryCoproducts D] (F : CategoryTheory.Functor C D) (A : C) :
                                                                                                                            F.comp (CategoryTheory.Limits.coprod.functor.obj (F.obj A)) (CategoryTheory.Limits.coprod.functor.obj A).comp F

                                                                                                                            The coproduct comparison morphism from FA ⨿ F- to F(A ⨿ -), whose components are given by coprodComparison.

                                                                                                                            Equations
                                                                                                                            Instances For