Documentation

Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes

Binary (co)products of type-valued functors #

Defines an explicit construction of binary products and coproducts of type-valued functors.

Also defines isomorphisms to the categorical product and coproduct, respectively.

prod F G is the explicit binary product of type-valued functors F and G.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem CategoryTheory.FunctorToTypes.prod.fst_app {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} {G : CategoryTheory.Functor C (Type w)} :
    ∀ (x : C) (a : (CategoryTheory.FunctorToTypes.prod F G).obj x), CategoryTheory.FunctorToTypes.prod.fst.app x a = a.1

    The first projection of prod F G, onto F.

    Equations
    Instances For
      @[simp]
      theorem CategoryTheory.FunctorToTypes.prod.snd_app {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} {G : CategoryTheory.Functor C (Type w)} :
      ∀ (x : C) (a : (CategoryTheory.FunctorToTypes.prod F G).obj x), CategoryTheory.FunctorToTypes.prod.snd.app x a = a.2

      The second projection of prod F G, onto G.

      Equations
      Instances For
        @[simp]
        theorem CategoryTheory.FunctorToTypes.prod.lift_app {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} {F₁ : CategoryTheory.Functor C (Type w)} {F₂ : CategoryTheory.Functor C (Type w)} (τ₁ : F F₁) (τ₂ : F F₂) (x : C) (y : F.obj x) :
        (CategoryTheory.FunctorToTypes.prod.lift τ₁ τ₂).app x y = (τ₁.app x y, τ₂.app x y)

        Given natural transformations F ⟶ F₁ and F ⟶ F₂, construct a natural transformation F ⟶ prod F₁ F₂.

        Equations
        Instances For
          @[simp]
          theorem CategoryTheory.FunctorToTypes.prod.lift_fst {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} {F₁ : CategoryTheory.Functor C (Type w)} {F₂ : CategoryTheory.Functor C (Type w)} (τ₁ : F F₁) (τ₂ : F F₂) :
          CategoryTheory.CategoryStruct.comp (CategoryTheory.FunctorToTypes.prod.lift τ₁ τ₂) CategoryTheory.FunctorToTypes.prod.fst = τ₁
          @[simp]
          theorem CategoryTheory.FunctorToTypes.prod.lift_snd {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} {F₁ : CategoryTheory.Functor C (Type w)} {F₂ : CategoryTheory.Functor C (Type w)} (τ₁ : F F₁) (τ₂ : F F₂) :
          CategoryTheory.CategoryStruct.comp (CategoryTheory.FunctorToTypes.prod.lift τ₁ τ₂) CategoryTheory.FunctorToTypes.prod.snd = τ₂
          @[simp]
          theorem CategoryTheory.FunctorToTypes.binaryProductCone_pt_map {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) (G : CategoryTheory.Functor C (Type w)) :
          ∀ {X Y : C} (f : X Y) (a : F.obj X × G.obj X), (CategoryTheory.FunctorToTypes.binaryProductCone F G).pt.map f a = (F.map f a.1, G.map f a.2)

          The binary fan whose point is prod F G.

          Equations
          Instances For
            noncomputable def CategoryTheory.FunctorToTypes.prodMk {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} {G : CategoryTheory.Functor C (Type w)} {a : C} (x : F.obj a) (y : G.obj a) :
            (F G).obj a

            Construct an element of (F ⨯ G).obj a from an element of F.obj a and an element of G.obj a.

            Equations
            Instances For
              @[simp]
              theorem CategoryTheory.FunctorToTypes.prodMk_fst {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} {G : CategoryTheory.Functor C (Type w)} {a : C} (x : F.obj a) (y : G.obj a) :
              CategoryTheory.Limits.prod.fst.app a (CategoryTheory.FunctorToTypes.prodMk x y) = x
              @[simp]
              theorem CategoryTheory.FunctorToTypes.prodMk_snd {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} {G : CategoryTheory.Functor C (Type w)} {a : C} (x : F.obj a) (y : G.obj a) :
              CategoryTheory.Limits.prod.snd.app a (CategoryTheory.FunctorToTypes.prodMk x y) = y
              noncomputable def CategoryTheory.FunctorToTypes.binaryProductEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) (G : CategoryTheory.Functor C (Type w)) (a : C) :
              (F G).obj a F.obj a × G.obj a

              (F ⨯ G).obj a is in bijection with the product of F.obj a and G.obj a.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                theorem CategoryTheory.FunctorToTypes.prod_ext'_iff {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} {G : CategoryTheory.Functor C (Type w)} {a : C} {z : (F G).obj a} {w : (F G).obj a} :
                z = w CategoryTheory.Limits.prod.fst.app a z = CategoryTheory.Limits.prod.fst.app a w CategoryTheory.Limits.prod.snd.app a z = CategoryTheory.Limits.prod.snd.app a w
                theorem CategoryTheory.FunctorToTypes.prod_ext' {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) (G : CategoryTheory.Functor C (Type w)) (a : C) (z : (F G).obj a) (w : (F G).obj a) (h1 : CategoryTheory.Limits.prod.fst.app a z = CategoryTheory.Limits.prod.fst.app a w) (h2 : CategoryTheory.Limits.prod.snd.app a z = CategoryTheory.Limits.prod.snd.app a w) :
                z = w

                coprod F G is the explicit binary coproduct of type-valued functors F and G.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  @[simp]
                  theorem CategoryTheory.FunctorToTypes.coprod.inl_app {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} {G : CategoryTheory.Functor C (Type w)} :
                  ∀ (x : C) (x_1 : F.obj x), CategoryTheory.FunctorToTypes.coprod.inl.app x x_1 = Sum.inl x_1

                  The left inclusion of F into coprod F G.

                  Equations
                  • CategoryTheory.FunctorToTypes.coprod.inl = { app := fun (x : C) (x_1 : F.obj x) => Sum.inl x_1, naturality := }
                  Instances For
                    @[simp]
                    theorem CategoryTheory.FunctorToTypes.coprod.inr_app {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} {G : CategoryTheory.Functor C (Type w)} :
                    ∀ (x : C) (x_1 : G.obj x), CategoryTheory.FunctorToTypes.coprod.inr.app x x_1 = Sum.inr x_1

                    The right inclusion of G into coprod F G.

                    Equations
                    • CategoryTheory.FunctorToTypes.coprod.inr = { app := fun (x : C) (x_1 : G.obj x) => Sum.inr x_1, naturality := }
                    Instances For
                      @[simp]
                      theorem CategoryTheory.FunctorToTypes.coprod.desc_app {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} {F₁ : CategoryTheory.Functor C (Type w)} {F₂ : CategoryTheory.Functor C (Type w)} (τ₁ : F₁ F) (τ₂ : F₂ F) (a : C) (x : (CategoryTheory.FunctorToTypes.coprod F₁ F₂).obj a) :
                      (CategoryTheory.FunctorToTypes.coprod.desc τ₁ τ₂).app a x = Sum.casesOn (motive := fun (t : F₁.obj a F₂.obj a) => x = tF.obj a) x (fun (x_1 : F₁.obj a) (h : x = Sum.inl x_1) => τ₁.app a x_1) (fun (x_1 : F₂.obj a) (h : x = Sum.inr x_1) => τ₂.app a x_1)

                      Given natural transformations F₁ ⟶ F and F₂ ⟶ F, construct a natural transformation coprod F₁ F₂ ⟶ F.

                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        @[simp]
                        theorem CategoryTheory.FunctorToTypes.coprod.desc_inl {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} {F₁ : CategoryTheory.Functor C (Type w)} {F₂ : CategoryTheory.Functor C (Type w)} (τ₁ : F₁ F) (τ₂ : F₂ F) :
                        CategoryTheory.CategoryStruct.comp CategoryTheory.FunctorToTypes.coprod.inl (CategoryTheory.FunctorToTypes.coprod.desc τ₁ τ₂) = τ₁
                        @[simp]
                        theorem CategoryTheory.FunctorToTypes.coprod.desc_inr {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} {F₁ : CategoryTheory.Functor C (Type w)} {F₂ : CategoryTheory.Functor C (Type w)} (τ₁ : F₁ F) (τ₂ : F₂ F) :
                        CategoryTheory.CategoryStruct.comp CategoryTheory.FunctorToTypes.coprod.inr (CategoryTheory.FunctorToTypes.coprod.desc τ₁ τ₂) = τ₂
                        @[simp]
                        theorem CategoryTheory.FunctorToTypes.binaryCoproductCocone_pt_map {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) (G : CategoryTheory.Functor C (Type w)) :
                        ∀ {X Y : C} (f : X Y) (x : F.obj X G.obj X), (CategoryTheory.FunctorToTypes.binaryCoproductCocone F G).pt.map f x = Sum.rec (motive := fun (t : F.obj X G.obj X) => x = tF.obj Y G.obj Y) (fun (val : F.obj X) (h : x = Sum.inl val) => Sum.inl (F.map f val)) (fun (val : G.obj X) (h : x = Sum.inr val) => Sum.inr (G.map f val)) x

                        The binary cofan whose point is coprod F G.

                        Equations
                        Instances For

                          coprod F G is a colimit cocone.

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

                            coprod F G is a binary coproduct for F and G.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              @[reducible, inline]
                              noncomputable abbrev CategoryTheory.FunctorToTypes.coprodInl {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} {G : CategoryTheory.Functor C (Type w)} {a : C} (x : F.obj a) :
                              (F ⨿ G).obj a

                              Construct an element of (F ⨿ G).obj a from an element of F.obj a

                              Equations
                              Instances For
                                @[reducible, inline]
                                noncomputable abbrev CategoryTheory.FunctorToTypes.coprodInr {C : Type u} [CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)} {G : CategoryTheory.Functor C (Type w)} {a : C} (x : G.obj a) :
                                (F ⨿ G).obj a

                                Construct an element of (F ⨿ G).obj a from an element of G.obj a

                                Equations
                                Instances For
                                  noncomputable def CategoryTheory.FunctorToTypes.binaryCoproductEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C (Type w)) (G : CategoryTheory.Functor C (Type w)) (a : C) :
                                  (F ⨿ G).obj a F.obj a G.obj a

                                  (F ⨿ G).obj a is in bijection with disjoint union of F.obj a and G.obj a.

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