Documentation

Mathlib.CategoryTheory.Limits.Shapes.Products

Categorical (co)products #

This file defines (co)products as special cases of (co)limits.

A product is the categorical generalization of the object Π i, f i where f : ι → C. It is a limit cone over the diagram formed by f, implemented by converting f into a functor Discrete ι ⥤ C.

A coproduct is the dual concept.

Main definitions #

Each of these has a dual.

Implementation notes #

As with the other special shapes in the limits library, all the definitions here are given as abbreviations of the general statements for limits, so all the simp lemmas and theorems about general limits can be used.

@[inline, reducible]
abbrev CategoryTheory.Limits.Fan {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (f : βC) :
Type (max (max w u) v)

A fan over f : β → C consists of a collection of maps from an object P to every f b.

Instances For
    @[inline, reducible]
    abbrev CategoryTheory.Limits.Cofan {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (f : βC) :
    Type (max (max w u) v)

    A cofan over f : β → C consists of a collection of maps from every f b to an object P.

    Instances For
      @[simp]
      theorem CategoryTheory.Limits.Fan.mk_π_app {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : βC} (P : C) (p : (b : β) → P f b) (X : CategoryTheory.Discrete β) :
      (CategoryTheory.Limits.Fan.mk P p).π.app X = p X.as
      @[simp]
      theorem CategoryTheory.Limits.Fan.mk_pt {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : βC} (P : C) (p : (b : β) → P f b) :
      def CategoryTheory.Limits.Fan.mk {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : βC} (P : C) (p : (b : β) → P f b) :

      A fan over f : β → C consists of a collection of maps from an object P to every f b.

      Instances For
        @[simp]
        theorem CategoryTheory.Limits.Cofan.mk_pt {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : βC} (P : C) (p : (b : β) → f b P) :
        @[simp]
        theorem CategoryTheory.Limits.Cofan.mk_ι_app {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : βC} (P : C) (p : (b : β) → f b P) (X : CategoryTheory.Discrete β) :
        (CategoryTheory.Limits.Cofan.mk P p).ι.app X = p X.as
        def CategoryTheory.Limits.Cofan.mk {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : βC} (P : C) (p : (b : β) → f b P) :

        A cofan over f : β → C consists of a collection of maps from every f b to an object P.

        Instances For
          def CategoryTheory.Limits.Fan.proj {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : βC} (p : CategoryTheory.Limits.Fan f) (j : β) :
          p.pt f j

          Get the jth map in the fan

          Instances For
            def CategoryTheory.Limits.Cofan.proj {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : βC} (p : CategoryTheory.Limits.Cofan f) (j : β) :
            f j p.pt

            Get the jth map in the cofan

            Instances For
              @[simp]
              theorem CategoryTheory.Limits.fan_mk_proj {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : βC} (P : C) (p : (b : β) → P f b) (j : β) :
              @[simp]
              theorem CategoryTheory.Limits.cofan_mk_proj {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : βC} (P : C) (p : (b : β) → f b P) (j : β) :
              @[inline, reducible]

              An abbreviation for HasLimit (Discrete.functor f).

              Instances For
                @[inline, reducible]

                An abbreviation for HasColimit (Discrete.functor f).

                Instances For

                  Make a fan f into a limit fan by providing lift, fac, and uniq -- just a convenience lemma to avoid having to go through Discrete

                  Instances For

                    Make a cofan f into a colimit cofan by providing desc, fac, and uniq -- just a convenience lemma to avoid having to go through Discrete

                    Instances For
                      @[inline, reducible]

                      An abbreviation for HasLimitsOfShape (Discrete f).

                      Instances For
                        @[inline, reducible]

                        An abbreviation for HasColimitsOfShape (Discrete f).

                        Instances For
                          @[inline, reducible]

                          piObj f computes the product of a family of elements f. (It is defined as an abbreviation for limit (Discrete.functor f), so for most facts about piObj f, you will just use general facts about limits.)

                          Instances For
                            @[inline, reducible]

                            sigmaObj f computes the coproduct of a family of elements f. (It is defined as an abbreviation for colimit (Discrete.functor f), so for most facts about sigmaObj f, you will just use general facts about colimits.)

                            Instances For

                              notation for categorical products

                              Instances For

                                notation for categorical coproducts

                                Instances For
                                  @[inline, reducible]
                                  abbrev CategoryTheory.Limits.Pi.π {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] (f : βC) [CategoryTheory.Limits.HasProduct f] (b : β) :
                                  f f b

                                  The b-th projection from the pi object over f has the form ∏ f ⟶ f b.

                                  Instances For
                                    @[inline, reducible]

                                    The b-th inclusion into the sigma object over f has the form f b ⟶ ∐ f.

                                    Instances For

                                      The fan constructed of the projections from the product is limiting.

                                      Instances For

                                        The cofan constructed of the inclusions from the coproduct is colimiting.

                                        Instances For
                                          @[inline, reducible]
                                          abbrev CategoryTheory.Limits.Pi.lift {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : βC} [CategoryTheory.Limits.HasProduct f] {P : C} (p : (b : β) → P f b) :
                                          P f

                                          A collection of morphisms P ⟶ f b induces a morphism P ⟶ ∏ f.

                                          Instances For
                                            @[inline, reducible]
                                            abbrev CategoryTheory.Limits.Sigma.desc {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : βC} [CategoryTheory.Limits.HasCoproduct f] {P : C} (p : (b : β) → f b P) :
                                            f P

                                            A collection of morphisms f b ⟶ P induces a morphism ∐ f ⟶ P.

                                            Instances For
                                              @[inline, reducible]
                                              abbrev CategoryTheory.Limits.Pi.map {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : βC} {g : βC} [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] (p : (b : β) → f b g b) :
                                              f g

                                              Construct a morphism between categorical products (indexed by the same type) from a family of morphisms between the factors.

                                              Instances For
                                                def CategoryTheory.Limits.Pi.map' {β : Type w} {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : αC} {g : βC} [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] (p : βα) (q : (b : β) → f (p b) g b) :
                                                f g

                                                Construct a morphism between categorical products from a family of morphisms between the factors.

                                                Instances For
                                                  theorem CategoryTheory.Limits.Pi.map'_comp_map' {β : Type w} {α : Type w₂} {γ : Type w₃} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : αC} {g : βC} {h : γC} [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] [CategoryTheory.Limits.HasProduct h] (p : βα) (p' : γβ) (q : (b : β) → f (p b) g b) (q' : (c : γ) → g (p' c) h c) :
                                                  theorem CategoryTheory.Limits.Pi.map'_eq {β : Type w} {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : αC} {g : βC} [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] {p : βα} {p' : βα} {q : (b : β) → f (p b) g b} {q' : (b : β) → f (p' b) g b} (hp : p = p') (hq : ∀ (b : β), CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : f (p' b) = f (p b))) (q b) = q' b) :
                                                  @[inline, reducible]
                                                  abbrev CategoryTheory.Limits.Pi.mapIso {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : βC} {g : βC} [CategoryTheory.Limits.HasProductsOfShape β C] (p : (b : β) → f b g b) :
                                                  f g

                                                  Construct an isomorphism between categorical products (indexed by the same type) from a family of isomorphisms between the factors.

                                                  Instances For
                                                    @[inline, reducible]
                                                    abbrev CategoryTheory.Limits.Sigma.map {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : βC} {g : βC} [CategoryTheory.Limits.HasCoproduct f] [CategoryTheory.Limits.HasCoproduct g] (p : (b : β) → f b g b) :
                                                    f g

                                                    Construct a morphism between categorical coproducts (indexed by the same type) from a family of morphisms between the factors.

                                                    Instances For
                                                      def CategoryTheory.Limits.Sigma.map' {β : Type w} {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : αC} {g : βC} [CategoryTheory.Limits.HasCoproduct f] [CategoryTheory.Limits.HasCoproduct g] (p : αβ) (q : (a : α) → f a g (p a)) :
                                                      f g

                                                      Construct a morphism between categorical coproducts from a family of morphisms between the factors.

                                                      Instances For
                                                        theorem CategoryTheory.Limits.Sigma.map'_comp_map' {β : Type w} {α : Type w₂} {γ : Type w₃} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : αC} {g : βC} {h : γC} [CategoryTheory.Limits.HasCoproduct f] [CategoryTheory.Limits.HasCoproduct g] [CategoryTheory.Limits.HasCoproduct h] (p : αβ) (p' : βγ) (q : (a : α) → f a g (p a)) (q' : (b : β) → g b h (p' b)) :
                                                        theorem CategoryTheory.Limits.Sigma.map'_eq {β : Type w} {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : αC} {g : βC} [CategoryTheory.Limits.HasCoproduct f] [CategoryTheory.Limits.HasCoproduct g] {p : αβ} {p' : αβ} {q : (a : α) → f a g (p a)} {q' : (a : α) → f a g (p' a)} (hp : p = p') (hq : ∀ (a : α), CategoryTheory.CategoryStruct.comp (q a) (CategoryTheory.eqToHom (_ : g (p a) = g (p' a))) = q' a) :
                                                        @[inline, reducible]
                                                        abbrev CategoryTheory.Limits.Sigma.mapIso {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : βC} {g : βC} [CategoryTheory.Limits.HasCoproductsOfShape β C] (p : (b : β) → f b g b) :
                                                        f g

                                                        Construct an isomorphism between categorical coproducts (indexed by the same type) from a family of isomorphisms between the factors.

                                                        Instances For
                                                          @[simp]
                                                          theorem CategoryTheory.Limits.Pi.whiskerEquiv_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u_1} {K : Type u_2} {f : JC} {g : KC} (e : J K) (w : (j : J) → g (e j) f j) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] :
                                                          (CategoryTheory.Limits.Pi.whiskerEquiv e w).hom = CategoryTheory.Limits.Pi.map' e.symm fun k => CategoryTheory.CategoryStruct.comp (w (e.symm k)).inv (CategoryTheory.eqToHom (_ : g (e (e.symm k)) = g k))
                                                          @[simp]
                                                          theorem CategoryTheory.Limits.Pi.whiskerEquiv_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u_1} {K : Type u_2} {f : JC} {g : KC} (e : J K) (w : (j : J) → g (e j) f j) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] :
                                                          def CategoryTheory.Limits.Pi.whiskerEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u_1} {K : Type u_2} {f : JC} {g : KC} (e : J K) (w : (j : J) → g (e j) f j) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct g] :
                                                          f g

                                                          Two products which differ by an equivalence in the indexing type, and up to isomorphism in the factors, are isomorphic.

                                                          Instances For
                                                            @[simp]
                                                            theorem CategoryTheory.Limits.Sigma.whiskerEquiv_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u_1} {K : Type u_2} {f : JC} {g : KC} (e : J K) (w : (j : J) → g (e j) f j) [CategoryTheory.Limits.HasCoproduct f] [CategoryTheory.Limits.HasCoproduct g] :
                                                            (CategoryTheory.Limits.Sigma.whiskerEquiv e w).inv = CategoryTheory.Limits.Sigma.map' e.symm fun k => CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom (_ : g k = g (e (e.symm k)))) (w (e.symm k)).hom
                                                            @[simp]
                                                            theorem CategoryTheory.Limits.Sigma.whiskerEquiv_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u_1} {K : Type u_2} {f : JC} {g : KC} (e : J K) (w : (j : J) → g (e j) f j) [CategoryTheory.Limits.HasCoproduct f] [CategoryTheory.Limits.HasCoproduct g] :
                                                            def CategoryTheory.Limits.Sigma.whiskerEquiv {C : Type u} [CategoryTheory.Category.{v, u} C] {J : Type u_1} {K : Type u_2} {f : JC} {g : KC} (e : J K) (w : (j : J) → g (e j) f j) [CategoryTheory.Limits.HasCoproduct f] [CategoryTheory.Limits.HasCoproduct g] :
                                                            f g

                                                            Two coproducts which differ by an equivalence in the indexing type, and up to isomorphism in the factors, are isomorphic.

                                                            Instances For
                                                              instance CategoryTheory.Limits.instHasProductSigmaFstSnd {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_2} (f : ιType u_1) (g : (i : ι) → f iC) [∀ (i : ι), CategoryTheory.Limits.HasProduct (g i)] [CategoryTheory.Limits.HasProduct fun i => g i] :
                                                              CategoryTheory.Limits.HasProduct fun p => g p.fst p.snd
                                                              @[simp]
                                                              theorem CategoryTheory.Limits.piPiIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_2} (f : ιType u_1) (g : (i : ι) → f iC) [∀ (i : ι), CategoryTheory.Limits.HasProduct (g i)] [CategoryTheory.Limits.HasProduct fun i => g i] :
                                                              @[simp]
                                                              theorem CategoryTheory.Limits.piPiIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_2} (f : ιType u_1) (g : (i : ι) → f iC) [∀ (i : ι), CategoryTheory.Limits.HasProduct (g i)] [CategoryTheory.Limits.HasProduct fun i => g i] :
                                                              (CategoryTheory.Limits.piPiIso f g).inv = CategoryTheory.Limits.Pi.lift fun i => CategoryTheory.Limits.Pi.lift fun x => CategoryTheory.Limits.Pi.π (fun p => g p.fst p.snd) { fst := i, snd := x }
                                                              def CategoryTheory.Limits.piPiIso {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_2} (f : ιType u_1) (g : (i : ι) → f iC) [∀ (i : ι), CategoryTheory.Limits.HasProduct (g i)] [CategoryTheory.Limits.HasProduct fun i => g i] :
                                                              ( fun i => g i) fun p => g p.fst p.snd

                                                              An iterated product is a product over a sigma type.

                                                              Instances For
                                                                instance CategoryTheory.Limits.instHasCoproductSigmaFstSnd {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_2} (f : ιType u_1) (g : (i : ι) → f iC) [∀ (i : ι), CategoryTheory.Limits.HasCoproduct (g i)] [CategoryTheory.Limits.HasCoproduct fun i => g i] :
                                                                CategoryTheory.Limits.HasCoproduct fun p => g p.fst p.snd
                                                                @[simp]
                                                                theorem CategoryTheory.Limits.sigmaSigmaIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_2} (f : ιType u_1) (g : (i : ι) → f iC) [∀ (i : ι), CategoryTheory.Limits.HasCoproduct (g i)] [CategoryTheory.Limits.HasCoproduct fun i => g i] :
                                                                @[simp]
                                                                theorem CategoryTheory.Limits.sigmaSigmaIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_2} (f : ιType u_1) (g : (i : ι) → f iC) [∀ (i : ι), CategoryTheory.Limits.HasCoproduct (g i)] [CategoryTheory.Limits.HasCoproduct fun i => g i] :
                                                                def CategoryTheory.Limits.sigmaSigmaIso {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_2} (f : ιType u_1) (g : (i : ι) → f iC) [∀ (i : ι), CategoryTheory.Limits.HasCoproduct (g i)] [CategoryTheory.Limits.HasCoproduct fun i => g i] :
                                                                ( fun i => g i) fun p => g p.fst p.snd

                                                                An iterated coproduct is a coproduct over a sigma type.

                                                                Instances For

                                                                  The comparison morphism for the product of f. This is an iso iff G preserves the product of f, see PreservesProduct.ofIsoComparison.

                                                                  Instances For

                                                                    The comparison morphism for the coproduct of f. This is an iso iff G preserves the coproduct of f, see PreservesCoproduct.ofIsoComparison.

                                                                    Instances For
                                                                      @[inline, reducible]

                                                                      An abbreviation for Π J, HasLimitsOfShape (Discrete J) C

                                                                      Instances For
                                                                        @[inline, reducible]

                                                                        An abbreviation for Π J, HasColimitsOfShape (Discrete J) C

                                                                        Instances For
                                                                          theorem CategoryTheory.Limits.hasProducts_of_limit_fans {C : Type u} [CategoryTheory.Category.{v, u} C] (lf : {J : Type w} → (f : JC) → CategoryTheory.Limits.Fan f) (lf_is_limit : {J : Type w} → (f : JC) → CategoryTheory.Limits.IsLimit (lf J f)) :

                                                                          (Co)products over a type with a unique term.

                                                                          @[simp]
                                                                          theorem CategoryTheory.Limits.limitConeOfUnique_cone_π {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [Unique β] (f : βC) :
                                                                          (CategoryTheory.Limits.limitConeOfUnique f).cone = CategoryTheory.Discrete.natTrans fun x => match x with | { as := j } => CategoryTheory.eqToHom (_ : ((CategoryTheory.Functor.const (CategoryTheory.Discrete β)).obj (f default)).obj { as := j } = (CategoryTheory.Discrete.functor f).obj { as := j })

                                                                          The limit cone for the product over an index type with exactly one term.

                                                                          Instances For
                                                                            def CategoryTheory.Limits.productUniqueIso {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [Unique β] (f : βC) :
                                                                            f f default

                                                                            A product over an index type with exactly one term is just the object over that term.

                                                                            Instances For
                                                                              @[simp]

                                                                              The colimit cocone for the coproduct over an index type with exactly one term.

                                                                              Instances For
                                                                                def CategoryTheory.Limits.coproductUniqueIso {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] [Unique β] (f : βC) :
                                                                                f f default

                                                                                A coproduct over an index type with exactly one term is just the object over that term.

                                                                                Instances For

                                                                                  Reindex a categorical product via an equivalence of the index types.

                                                                                  Instances For

                                                                                    Reindex a categorical coproduct via an equivalence of the index types.

                                                                                    Instances For