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.

@[reducible, inline]
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.

Equations
Instances For
    @[reducible, inline]
    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.

    Equations
    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.

      Equations
      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.

        Equations
        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 "projection" in the fan. (Note that the initial letter of proj matches the greek letter in Cone.π.)

          Equations
          • p.proj j = p.app { as := j }
          Instances For
            def CategoryTheory.Limits.Cofan.inj {β : 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 "injection" in the cofan. (Note that the initial letter of inj matches the greek letter in Cocone.ι.)

            Equations
            • p.inj j = p.app { as := j }
            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_inj {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : βC} (P : C) (p : (b : β) → f b P) (j : β) :
              @[reducible, inline]

              An abbreviation for HasLimit (Discrete.functor f).

              Equations
              Instances For
                @[reducible, inline]

                An abbreviation for HasColimit (Discrete.functor f).

                Equations
                Instances For
                  @[simp]
                  theorem CategoryTheory.Limits.mkFanLimit_lift {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : βC} (t : CategoryTheory.Limits.Fan f) (lift : (s : CategoryTheory.Limits.Fan f) → s.pt t.pt) (fac : autoParam (∀ (s : CategoryTheory.Limits.Fan f) (j : β), CategoryTheory.CategoryStruct.comp (lift s) (t.proj j) = s.proj j) _auto✝) (uniq : autoParam (∀ (s : CategoryTheory.Limits.Fan f) (m : s.pt t.pt), (∀ (j : β), CategoryTheory.CategoryStruct.comp m (t.proj j) = s.proj j)m = lift s) _auto✝) (s : CategoryTheory.Limits.Fan f) :
                  (CategoryTheory.Limits.mkFanLimit t lift fac uniq).lift s = lift s
                  def CategoryTheory.Limits.mkFanLimit {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : βC} (t : CategoryTheory.Limits.Fan f) (lift : (s : CategoryTheory.Limits.Fan f) → s.pt t.pt) (fac : autoParam (∀ (s : CategoryTheory.Limits.Fan f) (j : β), CategoryTheory.CategoryStruct.comp (lift s) (t.proj j) = s.proj j) _auto✝) (uniq : autoParam (∀ (s : CategoryTheory.Limits.Fan f) (m : s.pt t.pt), (∀ (j : β), CategoryTheory.CategoryStruct.comp m (t.proj j) = s.proj j)m = lift s) _auto✝) :

                  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

                  Equations
                  Instances For
                    def CategoryTheory.Limits.Fan.IsLimit.desc {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {F : βC} {c : CategoryTheory.Limits.Fan F} (hc : CategoryTheory.Limits.IsLimit c) {A : C} (f : (i : β) → A F i) :
                    A c.pt

                    Constructor for morphisms to the point of a limit fan.

                    Equations
                    Instances For
                      @[simp]
                      theorem CategoryTheory.Limits.Fan.IsLimit.hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type u_1} {F : IC} {c : CategoryTheory.Limits.Fan F} (hc : CategoryTheory.Limits.IsLimit c) {A : C} (f : A c.pt) (g : A c.pt) (h : ∀ (i : I), CategoryTheory.CategoryStruct.comp f (c.proj i) = CategoryTheory.CategoryStruct.comp g (c.proj i)) :
                      f = g
                      @[simp]
                      theorem CategoryTheory.Limits.mkCofanColimit_desc {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : βC} (s : CategoryTheory.Limits.Cofan f) (desc : (t : CategoryTheory.Limits.Cofan f) → s.pt t.pt) (fac : autoParam (∀ (t : CategoryTheory.Limits.Cofan f) (j : β), CategoryTheory.CategoryStruct.comp (s.inj j) (desc t) = t.inj j) _auto✝) (uniq : autoParam (∀ (t : CategoryTheory.Limits.Cofan f) (m : s.pt t.pt), (∀ (j : β), CategoryTheory.CategoryStruct.comp (s.inj j) m = t.inj j)m = desc t) _auto✝) (t : CategoryTheory.Limits.Cofan f) :
                      (CategoryTheory.Limits.mkCofanColimit s desc fac uniq).desc t = desc t
                      def CategoryTheory.Limits.mkCofanColimit {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : βC} (s : CategoryTheory.Limits.Cofan f) (desc : (t : CategoryTheory.Limits.Cofan f) → s.pt t.pt) (fac : autoParam (∀ (t : CategoryTheory.Limits.Cofan f) (j : β), CategoryTheory.CategoryStruct.comp (s.inj j) (desc t) = t.inj j) _auto✝) (uniq : autoParam (∀ (t : CategoryTheory.Limits.Cofan f) (m : s.pt t.pt), (∀ (j : β), CategoryTheory.CategoryStruct.comp (s.inj j) m = t.inj j)m = desc t) _auto✝) :

                      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

                      Equations
                      Instances For
                        def CategoryTheory.Limits.Cofan.IsColimit.desc {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {F : βC} {c : CategoryTheory.Limits.Cofan F} (hc : CategoryTheory.Limits.IsColimit c) {A : C} (f : (i : β) → F i A) :
                        c.pt A

                        Constructor for morphisms from the point of a colimit cofan.

                        Equations
                        Instances For
                          theorem CategoryTheory.Limits.Cofan.IsColimit.hom_ext {C : Type u} [CategoryTheory.Category.{v, u} C] {I : Type u_1} {F : IC} {c : CategoryTheory.Limits.Cofan F} (hc : CategoryTheory.Limits.IsColimit c) {A : C} (f : c.pt A) (g : c.pt A) (h : ∀ (i : I), CategoryTheory.CategoryStruct.comp (c.inj i) f = CategoryTheory.CategoryStruct.comp (c.inj i) g) :
                          f = g
                          @[reducible, inline]

                          An abbreviation for HasLimitsOfShape (Discrete f).

                          Equations
                          Instances For
                            @[reducible, inline]

                            An abbreviation for HasColimitsOfShape (Discrete f).

                            Equations
                            Instances For
                              @[reducible, inline]

                              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.)

                              Equations
                              Instances For
                                @[reducible, inline]

                                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.)

                                Equations
                                Instances For

                                  notation for categorical products

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

                                    notation for categorical coproducts

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      @[reducible, inline]
                                      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.

                                      Equations
                                      Instances For
                                        @[reducible, inline]

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

                                        Equations
                                        Instances For

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

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

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

                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              @[reducible, inline]
                                              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.

                                              Equations
                                              Instances For
                                                @[reducible, inline]
                                                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.

                                                Equations
                                                Instances For
                                                  @[simp]
                                                  theorem CategoryTheory.Limits.Cofan.ext_inv_hom {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : βC} {c₁ : CategoryTheory.Limits.Cofan f} {c₂ : CategoryTheory.Limits.Cofan f} (e : c₁.pt c₂.pt) (w : autoParam (∀ (b : β), CategoryTheory.CategoryStruct.comp (c₁.inj b) e.hom = c₂.inj b) _auto✝) :
                                                  @[simp]
                                                  theorem CategoryTheory.Limits.Cofan.ext_hom_hom {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : βC} {c₁ : CategoryTheory.Limits.Cofan f} {c₂ : CategoryTheory.Limits.Cofan f} (e : c₁.pt c₂.pt) (w : autoParam (∀ (b : β), CategoryTheory.CategoryStruct.comp (c₁.inj b) e.hom = c₂.inj b) _auto✝) :
                                                  def CategoryTheory.Limits.Cofan.ext {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {f : βC} {c₁ : CategoryTheory.Limits.Cofan f} {c₂ : CategoryTheory.Limits.Cofan f} (e : c₁.pt c₂.pt) (w : autoParam (∀ (b : β), CategoryTheory.CategoryStruct.comp (c₁.inj b) e.hom = c₂.inj b) _auto✝) :
                                                  c₁ c₂

                                                  A version of Cocones.ext for Cofans.

                                                  Equations
                                                  Instances For

                                                    A cofan c on f such that the induced map ∐ f ⟶ c.pt is an iso, is a coproduct.

                                                    Equations
                                                    • One or more equations did not get rendered due to their size.
                                                    Instances For
                                                      @[reducible, inline]
                                                      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.

                                                      Equations
                                                      Instances For
                                                        Equations
                                                        • =
                                                        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.

                                                        Equations
                                                        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'_comp_map {β : 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 : βα) (q : (b : β) → f (p b) g b) (q' : (b : β) → g b h b) :
                                                          theorem CategoryTheory.Limits.Pi.map_comp_map' {β : 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 : βα) (q : (a : α) → f a g a) (q' : (b : β) → g (p b) h b) :
                                                          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 ) (q b) = q' b) :
                                                          @[reducible, inline]
                                                          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.

                                                          Equations
                                                          Instances For
                                                            @[simp]
                                                            theorem CategoryTheory.Limits.Pi.cone_pt {α : Type w₂} {C : Type u} [CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C) [CategoryTheory.Limits.HasProduct fun (j : α) => X.obj { as := j }] :
                                                            (CategoryTheory.Limits.Pi.cone X).pt = fun (j : α) => X.obj { as := j }

                                                            A limit cone for X : Discrete α ⥤ C that is given by ∏ (fun j => X.obj (Discrete.mk j)).

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

                                                              The cone Pi.cone X is a limit cone.

                                                              Equations
                                                              Instances For

                                                                The isomorphism ∏ (fun j => X.obj (Discrete.mk j)) ≅ limit X.

                                                                Equations
                                                                Instances For
                                                                  @[reducible, inline]
                                                                  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.

                                                                  Equations
                                                                  Instances For
                                                                    Equations
                                                                    • =
                                                                    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.

                                                                    Equations
                                                                    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 ) = q' a) :
                                                                      @[reducible, inline]
                                                                      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.

                                                                      Equations
                                                                      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] :
                                                                        @[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.

                                                                        Equations
                                                                        • One or more equations did not get rendered due to their size.
                                                                        Instances For
                                                                          @[simp]
                                                                          @[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.

                                                                          Equations
                                                                          • One or more equations did not get rendered due to their size.
                                                                          Instances For
                                                                            instance CategoryTheory.Limits.instHasProductSigmaFstSndOfPiObj {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} (f : ιType u_2) (g : (i : ι) → f iC) [∀ (i : ι), CategoryTheory.Limits.HasProduct (g i)] [CategoryTheory.Limits.HasProduct fun (i : ι) => g i] :
                                                                            CategoryTheory.Limits.HasProduct fun (p : (i : ι) × f i) => g p.fst p.snd
                                                                            Equations
                                                                            • =
                                                                            @[simp]
                                                                            theorem CategoryTheory.Limits.piPiIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} (f : ιType u_2) (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 : f i) => CategoryTheory.Limits.Pi.π (fun (p : (i : ι) × f i) => g p.fst p.snd) i, x
                                                                            @[simp]
                                                                            theorem CategoryTheory.Limits.piPiIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} (f : ιType u_2) (g : (i : ι) → f iC) [∀ (i : ι), CategoryTheory.Limits.HasProduct (g i)] [CategoryTheory.Limits.HasProduct fun (i : ι) => g i] :
                                                                            (CategoryTheory.Limits.piPiIso f g).hom = CategoryTheory.Limits.Pi.lift fun (x : (i : ι) × f i) => match x with | i, x => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π (fun (i : ι) => g i) i) (CategoryTheory.Limits.Pi.π (g i) x)
                                                                            def CategoryTheory.Limits.piPiIso {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} (f : ιType u_2) (g : (i : ι) → f iC) [∀ (i : ι), CategoryTheory.Limits.HasProduct (g i)] [CategoryTheory.Limits.HasProduct fun (i : ι) => g i] :
                                                                            ( fun (i : ι) => g i) fun (p : (i : ι) × f i) => g p.fst p.snd

                                                                            An iterated product is a product over a sigma type.

                                                                            Equations
                                                                            • One or more equations did not get rendered due to their size.
                                                                            Instances For
                                                                              instance CategoryTheory.Limits.instHasCoproductSigmaFstSndOfSigmaObj {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} (f : ιType u_2) (g : (i : ι) → f iC) [∀ (i : ι), CategoryTheory.Limits.HasCoproduct (g i)] [CategoryTheory.Limits.HasCoproduct fun (i : ι) => g i] :
                                                                              CategoryTheory.Limits.HasCoproduct fun (p : (i : ι) × f i) => g p.fst p.snd
                                                                              Equations
                                                                              • =
                                                                              @[simp]
                                                                              theorem CategoryTheory.Limits.sigmaSigmaIso_hom {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} (f : ιType u_2) (g : (i : ι) → f iC) [∀ (i : ι), CategoryTheory.Limits.HasCoproduct (g i)] [CategoryTheory.Limits.HasCoproduct fun (i : ι) => g i] :
                                                                              (CategoryTheory.Limits.sigmaSigmaIso f g).hom = CategoryTheory.Limits.Sigma.desc fun (i : ι) => CategoryTheory.Limits.Sigma.desc fun (x : f i) => CategoryTheory.Limits.Sigma.ι (fun (p : (i : ι) × f i) => g p.fst p.snd) i, x
                                                                              @[simp]
                                                                              theorem CategoryTheory.Limits.sigmaSigmaIso_inv {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} (f : ιType u_2) (g : (i : ι) → f iC) [∀ (i : ι), CategoryTheory.Limits.HasCoproduct (g i)] [CategoryTheory.Limits.HasCoproduct fun (i : ι) => g i] :
                                                                              (CategoryTheory.Limits.sigmaSigmaIso f g).inv = CategoryTheory.Limits.Sigma.desc fun (x : (i : ι) × f i) => match x with | i, x => CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (g i) x) (CategoryTheory.Limits.Sigma.ι (fun (i : ι) => g i) i)
                                                                              def CategoryTheory.Limits.sigmaSigmaIso {C : Type u} [CategoryTheory.Category.{v, u} C] {ι : Type u_1} (f : ιType u_2) (g : (i : ι) → f iC) [∀ (i : ι), CategoryTheory.Limits.HasCoproduct (g i)] [CategoryTheory.Limits.HasCoproduct fun (i : ι) => g i] :
                                                                              ( fun (i : ι) => g i) fun (p : (i : ι) × f i) => g p.fst p.snd

                                                                              An iterated coproduct is a coproduct over a sigma type.

                                                                              Equations
                                                                              • One or more equations did not get rendered due to their size.
                                                                              Instances For
                                                                                def CategoryTheory.Limits.piComparison {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (f : βC) [CategoryTheory.Limits.HasProduct f] [CategoryTheory.Limits.HasProduct fun (b : β) => G.obj (f b)] :
                                                                                G.obj ( f) fun (b : β) => G.obj (f b)

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

                                                                                Equations
                                                                                Instances For
                                                                                  def CategoryTheory.Limits.sigmaComparison {β : Type w} {C : Type u} [CategoryTheory.Category.{v, u} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (f : βC) [CategoryTheory.Limits.HasCoproduct f] [CategoryTheory.Limits.HasCoproduct fun (b : β) => G.obj (f b)] :
                                                                                  ( fun (b : β) => G.obj (f b)) G.obj ( f)

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

                                                                                  Equations
                                                                                  Instances For
                                                                                    @[reducible, inline]

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

                                                                                    Equations
                                                                                    Instances For
                                                                                      @[reducible, inline]

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

                                                                                      Equations
                                                                                      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 f)) :

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

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

                                                                                        Equations
                                                                                        • One or more equations did not get rendered due to their size.
                                                                                        Instances For
                                                                                          @[instance 100]
                                                                                          Equations
                                                                                          • =
                                                                                          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.

                                                                                          Equations
                                                                                          Instances For

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

                                                                                            Equations
                                                                                            • One or more equations did not get rendered due to their size.
                                                                                            Instances For
                                                                                              @[instance 100]
                                                                                              Equations
                                                                                              • =
                                                                                              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.

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

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

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

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

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