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

• a Fan is a cone over a discrete category
• Fan.mk constructs a fan from an indexed collection of maps
• a Pi is a limit (Discrete.functor f)

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 abbrevs 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} [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.

@[reducible, inline]

abbrev CategoryTheory.Limits.Cofan {β : Type w} {C : Type u} [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.

def CategoryTheory.Limits.Fan.mk {β : Type w} {C : Type u} [Category.{v, u} C] {f : β → C} (P : C) (p : (b : β) → P ⟶ f b) : Fan f

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

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.Fan.mk_pt {β : Type w} {C : Type u} [Category.{v, u} C] {f : β → C} (P : C) (p : (b : β) → P ⟶ f b) : (mk P p).pt = P

def CategoryTheory.Limits.Cofan.mk {β : Type w} {C : Type u} [Category.{v, u} C] {f : β → C} (P : C) (p : (b : β) → f b ⟶ P) : Cofan f

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

@[simp]

theorem CategoryTheory.Limits.Cofan.mk_pt {β : Type w} {C : Type u} [Category.{v, u} C] {f : β → C} (P : C) (p : (b : β) → f b ⟶ P) : (mk P p).pt = P

@[simp]

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

def CategoryTheory.Limits.Fan.proj {β : Type w} {C : Type u} [Category.{v, u} C] {f : β → C} (p : 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.π.)

def CategoryTheory.Limits.Cofan.inj {β : Type w} {C : Type u} [Category.{v, u} C] {f : β → C} (p : 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.ι.)

@[simp]

theorem CategoryTheory.Limits.fan_mk_proj {β : Type w} {C : Type u} [Category.{v, u} C] {f : β → C} (P : C) (p : (b : β) → P ⟶ f b) : (Fan.mk P p).proj = p

@[simp]

theorem CategoryTheory.Limits.cofan_mk_inj {β : Type w} {C : Type u} [Category.{v, u} C] {f : β → C} (P : C) (p : (b : β) → f b ⟶ P) : (Cofan.mk P p).inj = p

@[reducible, inline]

abbrev CategoryTheory.Limits.HasProduct {β : Type w} {C : Type u} [Category.{v, u} C] (f : β → C) : Prop

An abbreviation for HasLimit (Discrete.functor f).

@[reducible, inline]

abbrev CategoryTheory.Limits.HasCoproduct {β : Type w} {C : Type u} [Category.{v, u} C] (f : β → C) : Prop

An abbreviation for HasColimit (Discrete.functor f).

theorem CategoryTheory.Limits.hasCoproduct_of_equiv_of_iso {β : Type w} {α : Type w₂} {C : Type u} [Category.{v, u} C] (f : α → C) (g : β → C) [HasCoproduct f] (e : β ≃ α) (iso : (j : β) → g j ≅ f (e j)) : HasCoproduct g

theorem CategoryTheory.Limits.hasProduct_of_equiv_of_iso {β : Type w} {α : Type w₂} {C : Type u} [Category.{v, u} C] (f : α → C) (g : β → C) [HasProduct f] (e : β ≃ α) (iso : (j : β) → g j ≅ f (e j)) : HasProduct g

def CategoryTheory.Limits.mkFanLimit {β : Type w} {C : Type u} [Category.{v, u} C] {f : β → C} (t : Fan f) (lift : (s : Fan f) → s.pt ⟶ t.pt) (fac : ∀ (s : Fan f) (j : β), CategoryStruct.comp (lift s) (t.proj j) = s.proj j := by cat_disch) (uniq : ∀ (s : Fan f) (m : s.pt ⟶ t.pt), (∀ (j : β), CategoryStruct.comp m (t.proj j) = s.proj j) → m = lift s := by cat_disch) : IsLimit t

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

@[simp]

theorem CategoryTheory.Limits.mkFanLimit_lift {β : Type w} {C : Type u} [Category.{v, u} C] {f : β → C} (t : Fan f) (lift : (s : Fan f) → s.pt ⟶ t.pt) (fac : ∀ (s : Fan f) (j : β), CategoryStruct.comp (lift s) (t.proj j) = s.proj j := by cat_disch) (uniq : ∀ (s : Fan f) (m : s.pt ⟶ t.pt), (∀ (j : β), CategoryStruct.comp m (t.proj j) = s.proj j) → m = lift s := by cat_disch) (s : Fan f) : (mkFanLimit t lift fac uniq).lift s = lift s

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

Constructor for morphisms to the point of a limit fan.

@[deprecated CategoryTheory.Limits.Fan.IsLimit.lift (since := "2026-01-12")]

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

Alias of CategoryTheory.Limits.Fan.IsLimit.lift.

---

Constructor for morphisms to the point of a limit fan.

@[simp]

theorem CategoryTheory.Limits.Fan.IsLimit.fac {β : Type w} {C : Type u} [Category.{v, u} C] {F : β → C} {c : Fan F} (hc : IsLimit c) {A : C} (f : (i : β) → A ⟶ F i) (i : β) : CategoryStruct.comp (lift hc f) (c.proj i) = f i

@[simp]

theorem CategoryTheory.Limits.Fan.IsLimit.fac_assoc {β : Type w} {C : Type u} [Category.{v, u} C] {F : β → C} {c : Fan F} (hc : IsLimit c) {A : C} (f : (i : β) → A ⟶ F i) (i : β) {Z : C} (h : F i ⟶ Z) : CategoryStruct.comp (lift hc f) (CategoryStruct.comp (c.proj i) h) = CategoryStruct.comp (f i) h

@[simp]

theorem CategoryTheory.Limits.Fan.IsLimit.lift_proj {β : Type w} {C : Type u} [Category.{v, u} C] {X : β → C} {c : Fan X} (d : Fan X) (hc : IsLimit c) (i : β) : CategoryStruct.comp (hc.lift d) (c.proj i) = d.proj i

@[simp]

theorem CategoryTheory.Limits.Fan.IsLimit.lift_proj_assoc {β : Type w} {C : Type u} [Category.{v, u} C] {X : β → C} {c : Fan X} (d : Fan X) (hc : IsLimit c) (i : β) {Z : C} (h : X i ⟶ Z) : CategoryStruct.comp (hc.lift d) (CategoryStruct.comp (c.proj i) h) = CategoryStruct.comp (d.proj i) h

theorem CategoryTheory.Limits.Fan.IsLimit.hom_ext {C : Type u} [Category.{v, u} C] {I : Type u_1} {F : I → C} {c : Fan F} (hc : IsLimit c) {A : C} (f g : A ⟶ c.pt) (h : ∀ (i : I), CategoryStruct.comp f (c.proj i) = CategoryStruct.comp g (c.proj i)) : f = g

def CategoryTheory.Limits.mkCofanColimit {β : Type w} {C : Type u} [Category.{v, u} C] {f : β → C} (s : Cofan f) (desc : (t : Cofan f) → s.pt ⟶ t.pt) (fac : ∀ (t : Cofan f) (j : β), CategoryStruct.comp (s.inj j) (desc t) = t.inj j := by cat_disch) (uniq : ∀ (t : Cofan f) (m : s.pt ⟶ t.pt), (∀ (j : β), CategoryStruct.comp (s.inj j) m = t.inj j) → m = desc t := by cat_disch) : IsColimit s

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

@[simp]

theorem CategoryTheory.Limits.mkCofanColimit_desc {β : Type w} {C : Type u} [Category.{v, u} C] {f : β → C} (s : Cofan f) (desc : (t : Cofan f) → s.pt ⟶ t.pt) (fac : ∀ (t : Cofan f) (j : β), CategoryStruct.comp (s.inj j) (desc t) = t.inj j := by cat_disch) (uniq : ∀ (t : Cofan f) (m : s.pt ⟶ t.pt), (∀ (j : β), CategoryStruct.comp (s.inj j) m = t.inj j) → m = desc t := by cat_disch) (t : Cofan f) : (mkCofanColimit s desc fac uniq).desc t = desc t

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

Constructor for morphisms from the point of a colimit cofan.

@[simp]

theorem CategoryTheory.Limits.Cofan.IsColimit.fac {β : Type w} {C : Type u} [Category.{v, u} C] {F : β → C} {c : Cofan F} (hc : IsColimit c) {A : C} (f : (i : β) → F i ⟶ A) (i : β) : CategoryStruct.comp (c.inj i) (desc hc f) = f i

@[simp]

theorem CategoryTheory.Limits.Cofan.IsColimit.fac_assoc {β : Type w} {C : Type u} [Category.{v, u} C] {F : β → C} {c : Cofan F} (hc : IsColimit c) {A : C} (f : (i : β) → F i ⟶ A) (i : β) {Z : C} (h : A ⟶ Z) : CategoryStruct.comp (c.inj i) (CategoryStruct.comp (desc hc f) h) = CategoryStruct.comp (f i) h

@[simp]

theorem CategoryTheory.Limits.Cofan.IsColimit.inj_desc {β : Type w} {C : Type u} [Category.{v, u} C] {X : β → C} {c : Cofan X} (d : Cofan X) (hc : IsColimit c) (i : β) : CategoryStruct.comp (c.inj i) (hc.desc d) = d.inj i

@[simp]

theorem CategoryTheory.Limits.Cofan.IsColimit.inj_desc_assoc {β : Type w} {C : Type u} [Category.{v, u} C] {X : β → C} {c : Cofan X} (d : Cofan X) (hc : IsColimit c) (i : β) {Z : C} (h : d.pt ⟶ Z) : CategoryStruct.comp (c.inj i) (CategoryStruct.comp (hc.desc d) h) = CategoryStruct.comp (d.inj i) h

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

@[reducible, inline]

abbrev CategoryTheory.Limits.HasProductsOfShape (β : Type v) (C : Type u_1) [Category.{u_2, u_1} C] : Prop

An abbreviation for HasLimitsOfShape (Discrete f).

@[reducible, inline]

abbrev CategoryTheory.Limits.HasCoproductsOfShape (β : Type v) (C : Type u_1) [Category.{u_2, u_1} C] : Prop

An abbreviation for HasColimitsOfShape (Discrete f).

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.piObj {β : Type w} {C : Type u} [Category.{v, u} C] (f : β → C) [HasProduct f] : C

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

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.sigmaObj {β : Type w} {C : Type u} [Category.{v, u} C] (f : β → C) [HasCoproduct f] : C

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

def CategoryTheory.Limits.«term∏ᶜ_» : Lean.ParserDescr

notation for categorical products. We need ᶜ to avoid conflict with Finset.prod.

def CategoryTheory.Limits.«term∐_» : Lean.ParserDescr

notation for categorical coproducts

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.Pi.π {β : Type w} {C : Type u} [Category.{v, u} C] (f : β → C) [HasProduct f] (b : β) : ∏ᶜ f ⟶ f b

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

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.Sigma.ι {β : Type w} {C : Type u} [Category.{v, u} C] (f : β → C) [HasCoproduct f] (b : β) : f b ⟶ ∐ f

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

theorem CategoryTheory.Limits.Pi.hom_ext {β : Type w} {C : Type u} [Category.{v, u} C] {f : β → C} [HasProduct f] {X : C} (g₁ g₂ : X ⟶ ∏ᶜ f) (h : ∀ (b : β), CategoryStruct.comp g₁ (π f b) = CategoryStruct.comp g₂ (π f b)) : g₁ = g₂

Without this lemma, limit.hom_ext would be applied, but the goal would involve terms in Discrete β rather than β itself.

theorem CategoryTheory.Limits.Pi.hom_ext_iff {β : Type w} {C : Type u} [Category.{v, u} C] {f : β → C} [HasProduct f] {X : C} {g₁ g₂ : X ⟶ ∏ᶜ f} : g₁ = g₂ ↔ ∀ (b : β), CategoryStruct.comp g₁ (π f b) = CategoryStruct.comp g₂ (π f b)

theorem CategoryTheory.Limits.Sigma.hom_ext {β : Type w} {C : Type u} [Category.{v, u} C] {f : β → C} [HasCoproduct f] {X : C} (g₁ g₂ : ∐ f ⟶ X) (h : ∀ (b : β), CategoryStruct.comp (ι f b) g₁ = CategoryStruct.comp (ι f b) g₂) : g₁ = g₂

Without this lemma, limit.hom_ext would be applied, but the goal would involve terms in Discrete β rather than β itself.

theorem CategoryTheory.Limits.Sigma.hom_ext_iff {β : Type w} {C : Type u} [Category.{v, u} C] {f : β → C} [HasCoproduct f] {X : C} {g₁ g₂ : ∐ f ⟶ X} : g₁ = g₂ ↔ ∀ (b : β), CategoryStruct.comp (ι f b) g₁ = CategoryStruct.comp (ι f b) g₂

noncomputable def CategoryTheory.Limits.productIsProduct {β : Type w} {C : Type u} [Category.{v, u} C] (f : β → C) [HasProduct f] : IsLimit (Fan.mk (∏ᶜ f) (Pi.π f))

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

noncomputable def CategoryTheory.Limits.coproductIsCoproduct {β : Type w} {C : Type u} [Category.{v, u} C] (f : β → C) [HasCoproduct f] : IsColimit (Cofan.mk (∐ f) (Sigma.ι f))

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

theorem CategoryTheory.Limits.Pi.π_comp_eqToHom {C : Type u} [Category.{v, u} C] {J : Type u_1} (f : J → C) [HasProduct f] {j j' : J} (w : j = j') : CategoryStruct.comp (π f j) (eqToHom ⋯) = π f j'

theorem CategoryTheory.Limits.Pi.π_comp_eqToHom_assoc {C : Type u} [Category.{v, u} C] {J : Type u_1} (f : J → C) [HasProduct f] {j j' : J} (w : j = j') {Z : C} (h : f j' ⟶ Z) : CategoryStruct.comp (π f j) (CategoryStruct.comp (eqToHom ⋯) h) = CategoryStruct.comp (π f j') h

@[simp]

theorem CategoryTheory.Limits.Sigma.eqToHom_comp_ι {C : Type u} [Category.{v, u} C] {J : Type u_1} (f : J → C) [HasCoproduct f] {j j' : J} (w : j = j') : CategoryStruct.comp (eqToHom ⋯) (ι f j') = ι f j

@[simp]

theorem CategoryTheory.Limits.Sigma.eqToHom_comp_ι_assoc {C : Type u} [Category.{v, u} C] {J : Type u_1} (f : J → C) [HasCoproduct f] {j j' : J} (w : j = j') {Z : C} (h : ∐ f ⟶ Z) : CategoryStruct.comp (eqToHom ⋯) (CategoryStruct.comp (ι f j') h) = CategoryStruct.comp (ι f j) h

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.Pi.lift {β : Type w} {C : Type u} [Category.{v, u} C] {f : β → C} [HasProduct f] {P : C} (p : (b : β) → P ⟶ f b) : P ⟶ ∏ᶜ f

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

theorem CategoryTheory.Limits.Pi.lift_π {C : Type u} [Category.{v, u} C] {β : Type w} {f : β → C} [HasProduct f] {P : C} (p : (b : β) → P ⟶ f b) (b : β) : CategoryStruct.comp (lift p) (π f b) = p b

theorem CategoryTheory.Limits.Pi.lift_π_assoc {C : Type u} [Category.{v, u} C] {β : Type w} {f : β → C} [HasProduct f] {P : C} (p : (b : β) → P ⟶ f b) (b : β) {Z : C} (h : f b ⟶ Z) : CategoryStruct.comp (lift p) (CategoryStruct.comp (π f b) h) = CategoryStruct.comp (p b) h

def CategoryTheory.Limits.Fan.ext {β : Type w} {C : Type u} [Category.{v, u} C] {f : β → C} {c₁ c₂ : Fan f} (e : c₁.pt ≅ c₂.pt) (w : ∀ (b : β), c₁.proj b = CategoryStruct.comp e.hom (c₂.proj b) := by cat_disch) : c₁ ≅ c₂

A version of Cone.ext for Fans.

@[simp]

theorem CategoryTheory.Limits.Fan.ext_inv_hom {β : Type w} {C : Type u} [Category.{v, u} C] {f : β → C} {c₁ c₂ : Fan f} (e : c₁.pt ≅ c₂.pt) (w : ∀ (b : β), c₁.proj b = CategoryStruct.comp e.hom (c₂.proj b) := by cat_disch) : (ext e w).inv.hom = e.inv

@[simp]

theorem CategoryTheory.Limits.Fan.ext_hom_hom {β : Type w} {C : Type u} [Category.{v, u} C] {f : β → C} {c₁ c₂ : Fan f} (e : c₁.pt ≅ c₂.pt) (w : ∀ (b : β), c₁.proj b = CategoryStruct.comp e.hom (c₂.proj b) := by cat_disch) : (ext e w).hom.hom = e.hom

noncomputable def CategoryTheory.Limits.Fan.isLimitOfIsIsoPiLift {β : Type w} {C : Type u} [Category.{v, u} C] {f : β → C} [HasProduct f] (c : Fan f) [hc : IsIso (Pi.lift c.proj)] : IsLimit c

A fan c on f such that the induced map c.pt ⟶ ∏ f is an iso, is a product.

theorem CategoryTheory.Limits.Fan.nonempty_isLimit_iff_isIso_piLift {β : Type w} {C : Type u} [Category.{v, u} C] {f : β → C} [HasProduct f] (c : Fan f) : Nonempty (IsLimit c) ↔ IsIso (Pi.lift c.proj)

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.Sigma.desc {β : Type w} {C : Type u} [Category.{v, u} C] {f : β → C} [HasCoproduct f] {P : C} (p : (b : β) → f b ⟶ P) : ∐ f ⟶ P

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

theorem CategoryTheory.Limits.Sigma.ι_desc {C : Type u} [Category.{v, u} C] {β : Type w} {f : β → C} [HasCoproduct f] {P : C} (p : (b : β) → f b ⟶ P) (b : β) : CategoryStruct.comp (ι f b) (desc p) = p b

theorem CategoryTheory.Limits.Sigma.ι_desc_assoc {C : Type u} [Category.{v, u} C] {β : Type w} {f : β → C} [HasCoproduct f] {P : C} (p : (b : β) → f b ⟶ P) (b : β) {Z : C} (h : P ⟶ Z) : CategoryStruct.comp (ι f b) (CategoryStruct.comp (desc p) h) = CategoryStruct.comp (p b) h

instance CategoryTheory.Limits.instIsIsoDescι {β : Type w} {C : Type u} [Category.{v, u} C] {f : β → C} [HasCoproduct f] : IsIso (Sigma.desc fun (a : β) => Sigma.ι f a)

def CategoryTheory.Limits.Cofan.ext {β : Type w} {C : Type u} [Category.{v, u} C] {f : β → C} {c₁ c₂ : Cofan f} (e : c₁.pt ≅ c₂.pt) (w : ∀ (b : β), CategoryStruct.comp (c₁.inj b) e.hom = c₂.inj b := by cat_disch) : c₁ ≅ c₂

A version of Cocone.ext for Cofans.

@[simp]

theorem CategoryTheory.Limits.Cofan.ext_inv_hom {β : Type w} {C : Type u} [Category.{v, u} C] {f : β → C} {c₁ c₂ : Cofan f} (e : c₁.pt ≅ c₂.pt) (w : ∀ (b : β), CategoryStruct.comp (c₁.inj b) e.hom = c₂.inj b := by cat_disch) : (ext e w).inv.hom = e.inv

@[simp]

theorem CategoryTheory.Limits.Cofan.ext_hom_hom {β : Type w} {C : Type u} [Category.{v, u} C] {f : β → C} {c₁ c₂ : Cofan f} (e : c₁.pt ≅ c₂.pt) (w : ∀ (b : β), CategoryStruct.comp (c₁.inj b) e.hom = c₂.inj b := by cat_disch) : (ext e w).hom.hom = e.hom

noncomputable def CategoryTheory.Limits.Cofan.isColimitOfIsIsoSigmaDesc {β : Type w} {C : Type u} [Category.{v, u} C] {f : β → C} [HasCoproduct f] (c : Cofan f) [hc : IsIso (Sigma.desc c.inj)] : IsColimit c

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

theorem CategoryTheory.Limits.Cofan.nonempty_isColimit_iff_isIso_sigmaDesc {β : Type w} {C : Type u} [Category.{v, u} C] {f : β → C} [HasCoproduct f] (c : Cofan f) : Nonempty (IsColimit c) ↔ IsIso (Sigma.desc c.inj)

@[deprecated CategoryTheory.Limits.Cofan.nonempty_isColimit_iff_isIso_sigmaDesc (since := "2026-01-21")]

theorem CategoryTheory.Limits.Cofan.isColimit_iff_isIso_sigmaDesc {β : Type w} {C : Type u} [Category.{v, u} C] {f : β → C} [HasCoproduct f] (c : Cofan f) : Nonempty (IsColimit c) ↔ IsIso (Sigma.desc c.inj)

Alias of CategoryTheory.Limits.Cofan.nonempty_isColimit_iff_isIso_sigmaDesc.

def CategoryTheory.Limits.Cofan.isColimitTrans {α : Type w₂} {C : Type u} [Category.{v, u} C] {X : α → C} (c : Cofan X) (hc : IsColimit c) {β : α → Type u_1} {Y : (a : α) → β a → C} (π : (a : α) → (b : β a) → Y a b ⟶ X a) (hs : (a : α) → IsColimit (mk (X a) (π a))) : IsColimit (mk c.pt fun (x : (a : α) × β a) => match x with | ⟨a, b⟩ => CategoryStruct.comp (π a b) (c.inj a))

A coproduct of coproducts is a coproduct

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.Pi.map {β : Type w} {C : Type u} [Category.{v, u} C] {f g : β → C} [HasProduct f] [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.

@[simp]

theorem CategoryTheory.Limits.Pi.map_π {β : Type w} {C : Type u} [Category.{v, u} C] {f g : β → C} [HasProduct f] [HasProduct g] (p : (b : β) → f b ⟶ g b) (b : β) : CategoryStruct.comp (map p) (π g b) = CategoryStruct.comp (π f b) (p b)

@[simp]

theorem CategoryTheory.Limits.Pi.map_π_assoc {β : Type w} {C : Type u} [Category.{v, u} C] {f g : β → C} [HasProduct f] [HasProduct g] (p : (b : β) → f b ⟶ g b) (b : β) {Z : C} (h : g b ⟶ Z) : CategoryStruct.comp (map p) (CategoryStruct.comp (π g b) h) = CategoryStruct.comp (π f b) (CategoryStruct.comp (p b) h)

@[simp]

theorem CategoryTheory.Limits.Pi.map_id {α : Type w₂} {C : Type u} [Category.{v, u} C] {f : α → C} [HasProduct f] : (map fun (a : α) => CategoryStruct.id (f a)) = CategoryStruct.id (∏ᶜ f)

theorem CategoryTheory.Limits.Pi.map_comp_map {α : Type w₂} {C : Type u} [Category.{v, u} C] {f g h : α → C} [HasProduct f] [HasProduct g] [HasProduct h] (q : (a : α) → f a ⟶ g a) (q' : (a : α) → g a ⟶ h a) : CategoryStruct.comp (map q) (map q') = map fun (a : α) => CategoryStruct.comp (q a) (q' a)

instance CategoryTheory.Limits.Pi.map_mono {β : Type w} {C : Type u} [Category.{v, u} C] {f g : β → C} [HasProduct f] [HasProduct g] (p : (b : β) → f b ⟶ g b) [∀ (i : β), Mono (p i)] : Mono (map p)

noncomputable def CategoryTheory.Limits.Pi.map' {β : Type w} {α : Type w₂} {C : Type u} [Category.{v, u} C] {f : α → C} {g : β → C} [HasProduct f] [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.

@[simp]

theorem CategoryTheory.Limits.Pi.map'_comp_π {β : Type w} {α : Type w₂} {C : Type u} [Category.{v, u} C] {f : α → C} {g : β → C} [HasProduct f] [HasProduct g] (p : β → α) (q : (b : β) → f (p b) ⟶ g b) (b : β) : CategoryStruct.comp (map' p q) (π g b) = CategoryStruct.comp (π f (p b)) (q b)

@[simp]

theorem CategoryTheory.Limits.Pi.map'_comp_π_assoc {β : Type w} {α : Type w₂} {C : Type u} [Category.{v, u} C] {f : α → C} {g : β → C} [HasProduct f] [HasProduct g] (p : β → α) (q : (b : β) → f (p b) ⟶ g b) (b : β) {Z : C} (h : g b ⟶ Z) : CategoryStruct.comp (map' p q) (CategoryStruct.comp (π g b) h) = CategoryStruct.comp (π f (p b)) (CategoryStruct.comp (q b) h)

theorem CategoryTheory.Limits.Pi.map'_id_id {α : Type w₂} {C : Type u} [Category.{v, u} C] {f : α → C} [HasProduct f] : (map' id fun (a : α) => CategoryStruct.id (f a)) = CategoryStruct.id (∏ᶜ f)

@[simp]

theorem CategoryTheory.Limits.Pi.map'_id {α : Type w₂} {C : Type u} [Category.{v, u} C] {f g : α → C} [HasProduct f] [HasProduct g] (p : (b : α) → f b ⟶ g b) : map' id p = map p

theorem CategoryTheory.Limits.Pi.map'_comp_map' {β : Type w} {α : Type w₂} {γ : Type w₃} {C : Type u} [Category.{v, u} C] {f : α → C} {g : β → C} {h : γ → C} [HasProduct f] [HasProduct g] [HasProduct h] (p : β → α) (p' : γ → β) (q : (b : β) → f (p b) ⟶ g b) (q' : (c : γ) → g (p' c) ⟶ h c) : CategoryStruct.comp (map' p q) (map' p' q') = map' (p ∘ p') fun (c : γ) => CategoryStruct.comp (q (p' c)) (q' c)

theorem CategoryTheory.Limits.Pi.map'_comp_map {β : Type w} {α : Type w₂} {C : Type u} [Category.{v, u} C] {f : α → C} {g h : β → C} [HasProduct f] [HasProduct g] [HasProduct h] (p : β → α) (q : (b : β) → f (p b) ⟶ g b) (q' : (b : β) → g b ⟶ h b) : CategoryStruct.comp (map' p q) (map q') = map' p fun (b : β) => CategoryStruct.comp (q b) (q' b)

theorem CategoryTheory.Limits.Pi.map_comp_map' {β : Type w} {α : Type w₂} {C : Type u} [Category.{v, u} C] {f g : α → C} {h : β → C} [HasProduct f] [HasProduct g] [HasProduct h] (p : β → α) (q : (a : α) → f a ⟶ g a) (q' : (b : β) → g (p b) ⟶ h b) : CategoryStruct.comp (map q) (map' p q') = map' p fun (b : β) => CategoryStruct.comp (q (p b)) (q' b)

theorem CategoryTheory.Limits.Pi.map'_eq {β : Type w} {α : Type w₂} {C : Type u} [Category.{v, u} C] {f : α → C} {g : β → C} [HasProduct f] [HasProduct g] {p p' : β → α} {q : (b : β) → f (p b) ⟶ g b} {q' : (b : β) → f (p' b) ⟶ g b} (hp : p = p') (hq : ∀ (b : β), CategoryStruct.comp (eqToHom ⋯) (q b) = q' b) : map' p q = map' p' q'

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.Pi.mapIso {β : Type w} {C : Type u} [Category.{v, u} C] {f g : β → C} [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.

instance CategoryTheory.Limits.Pi.map_isIso {β : Type w} {C : Type u} [Category.{v, u} C] {f g : β → C} [HasProductsOfShape β C] (p : (b : β) → f b ⟶ g b) [∀ (b : β), IsIso (p b)] : IsIso (map p)

noncomputable def CategoryTheory.Limits.Pi.cone {α : Type w₂} {C : Type u} [Category.{v, u} C] (X : Functor (Discrete α) C) [HasProduct fun (j : α) => X.obj { as := j }] : Cone X

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

@[simp]

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

@[simp]

theorem CategoryTheory.Limits.Pi.cone_π {α : Type w₂} {C : Type u} [Category.{v, u} C] (X : Functor (Discrete α) C) [HasProduct fun (j : α) => X.obj { as := j }] : (cone X).π = Discrete.natTrans fun (x : Discrete α) => π (fun (j : α) => X.obj { as := j }) x.as

noncomputable def CategoryTheory.Limits.productIsProduct' {α : Type w₂} {C : Type u} [Category.{v, u} C] (X : Functor (Discrete α) C) [HasProduct fun (j : α) => X.obj { as := j }] : IsLimit (Pi.cone X)

The cone Pi.cone X is a limit cone.

noncomputable def CategoryTheory.Limits.Pi.isoLimit {α : Type w₂} {C : Type u} [Category.{v, u} C] (X : Functor (Discrete α) C) [HasProduct fun (j : α) => X.obj { as := j }] [HasLimit X] : (∏ᶜ fun (j : α) => X.obj { as := j }) ≅ limit X

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

@[simp]

theorem CategoryTheory.Limits.Pi.isoLimit_inv_π {α : Type w₂} {C : Type u} [Category.{v, u} C] (X : Functor (Discrete α) C) [HasProduct fun (j : α) => X.obj { as := j }] [HasLimit X] (j : α) : CategoryStruct.comp (isoLimit X).inv (π (fun (j : α) => X.obj { as := j }) j) = limit.π X { as := j }

@[simp]

theorem CategoryTheory.Limits.Pi.isoLimit_inv_π_assoc {α : Type w₂} {C : Type u} [Category.{v, u} C] (X : Functor (Discrete α) C) [HasProduct fun (j : α) => X.obj { as := j }] [HasLimit X] (j : α) {Z : C} (h : X.obj { as := j } ⟶ Z) : CategoryStruct.comp (isoLimit X).inv (CategoryStruct.comp (π (fun (j : α) => X.obj { as := j }) j) h) = CategoryStruct.comp (limit.π X { as := j }) h

@[simp]

theorem CategoryTheory.Limits.Pi.isoLimit_hom_π {α : Type w₂} {C : Type u} [Category.{v, u} C] (X : Functor (Discrete α) C) [HasProduct fun (j : α) => X.obj { as := j }] [HasLimit X] (j : α) : CategoryStruct.comp (isoLimit X).hom (limit.π X { as := j }) = π (fun (j : α) => X.obj { as := j }) j

@[simp]

theorem CategoryTheory.Limits.Pi.isoLimit_hom_π_assoc {α : Type w₂} {C : Type u} [Category.{v, u} C] (X : Functor (Discrete α) C) [HasProduct fun (j : α) => X.obj { as := j }] [HasLimit X] (j : α) {Z : C} (h : X.obj { as := j } ⟶ Z) : CategoryStruct.comp (isoLimit X).hom (CategoryStruct.comp (limit.π X { as := j }) h) = CategoryStruct.comp (π (fun (j : α) => X.obj { as := j }) j) h

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.Sigma.map {β : Type w} {C : Type u} [Category.{v, u} C] {f g : β → C} [HasCoproduct f] [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.

@[simp]

theorem CategoryTheory.Limits.Sigma.ι_map {β : Type w} {C : Type u} [Category.{v, u} C] {f g : β → C} [HasCoproduct f] [HasCoproduct g] (p : (b : β) → f b ⟶ g b) (b : β) : CategoryStruct.comp (ι f b) (map p) = CategoryStruct.comp (p b) (ι g b)

@[simp]

theorem CategoryTheory.Limits.Sigma.ι_map_assoc {β : Type w} {C : Type u} [Category.{v, u} C] {f g : β → C} [HasCoproduct f] [HasCoproduct g] (p : (b : β) → f b ⟶ g b) (b : β) {Z : C} (h : ∐ g ⟶ Z) : CategoryStruct.comp (ι f b) (CategoryStruct.comp (map p) h) = CategoryStruct.comp (p b) (CategoryStruct.comp (ι g b) h)

@[simp]

theorem CategoryTheory.Limits.Sigma.map_id {α : Type w₂} {C : Type u} [Category.{v, u} C] {f : α → C} [HasCoproduct f] : (map fun (a : α) => CategoryStruct.id (f a)) = CategoryStruct.id (∐ f)

theorem CategoryTheory.Limits.Sigma.map_comp_map {α : Type w₂} {C : Type u} [Category.{v, u} C] {f g h : α → C} [HasCoproduct f] [HasCoproduct g] [HasCoproduct h] (q : (a : α) → f a ⟶ g a) (q' : (a : α) → g a ⟶ h a) : CategoryStruct.comp (map q) (map q') = map fun (a : α) => CategoryStruct.comp (q a) (q' a)

instance CategoryTheory.Limits.Sigma.map_epi {β : Type w} {C : Type u} [Category.{v, u} C] {f g : β → C} [HasCoproduct f] [HasCoproduct g] (p : (b : β) → f b ⟶ g b) [∀ (i : β), Epi (p i)] : Epi (map p)

noncomputable def CategoryTheory.Limits.Sigma.map' {β : Type w} {α : Type w₂} {C : Type u} [Category.{v, u} C] {f : α → C} {g : β → C} [HasCoproduct f] [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.

@[simp]

theorem CategoryTheory.Limits.Sigma.ι_comp_map' {β : Type w} {α : Type w₂} {C : Type u} [Category.{v, u} C] {f : α → C} {g : β → C} [HasCoproduct f] [HasCoproduct g] (p : α → β) (q : (a : α) → f a ⟶ g (p a)) (a : α) : CategoryStruct.comp (ι f a) (map' p q) = CategoryStruct.comp (q a) (ι g (p a))

@[simp]

theorem CategoryTheory.Limits.Sigma.ι_comp_map'_assoc {β : Type w} {α : Type w₂} {C : Type u} [Category.{v, u} C] {f : α → C} {g : β → C} [HasCoproduct f] [HasCoproduct g] (p : α → β) (q : (a : α) → f a ⟶ g (p a)) (a : α) {Z : C} (h : ∐ g ⟶ Z) : CategoryStruct.comp (ι f a) (CategoryStruct.comp (map' p q) h) = CategoryStruct.comp (q a) (CategoryStruct.comp (ι g (p a)) h)

theorem CategoryTheory.Limits.Sigma.map'_id_id {α : Type w₂} {C : Type u} [Category.{v, u} C] {f : α → C} [HasCoproduct f] : (map' id fun (a : α) => CategoryStruct.id (f a)) = CategoryStruct.id (∐ f)

@[simp]

theorem CategoryTheory.Limits.Sigma.map'_id {α : Type w₂} {C : Type u} [Category.{v, u} C] {f g : α → C} [HasCoproduct f] [HasCoproduct g] (p : (b : α) → f b ⟶ g b) : map' id p = map p

theorem CategoryTheory.Limits.Sigma.map'_comp_map' {β : Type w} {α : Type w₂} {γ : Type w₃} {C : Type u} [Category.{v, u} C] {f : α → C} {g : β → C} {h : γ → C} [HasCoproduct f] [HasCoproduct g] [HasCoproduct h] (p : α → β) (p' : β → γ) (q : (a : α) → f a ⟶ g (p a)) (q' : (b : β) → g b ⟶ h (p' b)) : CategoryStruct.comp (map' p q) (map' p' q') = map' (p' ∘ p) fun (a : α) => CategoryStruct.comp (q a) (q' (p a))

theorem CategoryTheory.Limits.Sigma.map'_comp_map {β : Type w} {α : Type w₂} {C : Type u} [Category.{v, u} C] {f : α → C} {g h : β → C} [HasCoproduct f] [HasCoproduct g] [HasCoproduct h] (p : α → β) (q : (a : α) → f a ⟶ g (p a)) (q' : (b : β) → g b ⟶ h b) : CategoryStruct.comp (map' p q) (map q') = map' p fun (a : α) => CategoryStruct.comp (q a) (q' (p a))

theorem CategoryTheory.Limits.Sigma.map_comp_map' {β : Type w} {α : Type w₂} {C : Type u} [Category.{v, u} C] {f g : α → C} {h : β → C} [HasCoproduct f] [HasCoproduct g] [HasCoproduct h] (p : α → β) (q : (a : α) → f a ⟶ g a) (q' : (a : α) → g a ⟶ h (p a)) : CategoryStruct.comp (map q) (map' p q') = map' p fun (a : α) => CategoryStruct.comp (q a) (q' a)

theorem CategoryTheory.Limits.Sigma.map'_eq {β : Type w} {α : Type w₂} {C : Type u} [Category.{v, u} C] {f : α → C} {g : β → C} [HasCoproduct f] [HasCoproduct g] {p p' : α → β} {q : (a : α) → f a ⟶ g (p a)} {q' : (a : α) → f a ⟶ g (p' a)} (hp : p = p') (hq : ∀ (a : α), CategoryStruct.comp (q a) (eqToHom ⋯) = q' a) : map' p q = map' p' q'

@[reducible, inline]

noncomputable abbrev CategoryTheory.Limits.Sigma.mapIso {β : Type w} {C : Type u} [Category.{v, u} C] {f g : β → C} [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.

instance CategoryTheory.Limits.Sigma.map_isIso {β : Type w} {C : Type u} [Category.{v, u} C] {f g : β → C} [HasCoproductsOfShape β C] (p : (b : β) → f b ⟶ g b) [∀ (b : β), IsIso (p b)] : IsIso (map p)

noncomputable def CategoryTheory.Limits.Sigma.cocone {α : Type w₂} {C : Type u} [Category.{v, u} C] (X : Functor (Discrete α) C) [HasCoproduct fun (j : α) => X.obj { as := j }] : Cocone X

A colimit cocone for X : Discrete α ⥤ C that is given by ∐ (fun j => X.obj (Discrete.mk j)).

@[simp]

theorem CategoryTheory.Limits.Sigma.cocone_pt {α : Type w₂} {C : Type u} [Category.{v, u} C] (X : Functor (Discrete α) C) [HasCoproduct fun (j : α) => X.obj { as := j }] : (cocone X).pt = ∐ fun (j : α) => X.obj { as := j }

@[simp]

theorem CategoryTheory.Limits.Sigma.cocone_ι {α : Type w₂} {C : Type u} [Category.{v, u} C] (X : Functor (Discrete α) C) [HasCoproduct fun (j : α) => X.obj { as := j }] : (cocone X).ι = Discrete.natTrans fun (x : Discrete α) => ι (fun (j : α) => X.obj { as := j }) x.as

noncomputable def CategoryTheory.Limits.coproductIsCoproduct' {α : Type w₂} {C : Type u} [Category.{v, u} C] (X : Functor (Discrete α) C) [HasCoproduct fun (j : α) => X.obj { as := j }] : IsColimit (Sigma.cocone X)

The cocone Sigma.cocone X is a colimit cocone.

noncomputable def CategoryTheory.Limits.Sigma.isoColimit {α : Type w₂} {C : Type u} [Category.{v, u} C] (X : Functor (Discrete α) C) [HasCoproduct fun (j : α) => X.obj { as := j }] [HasColimit X] : (∐ fun (j : α) => X.obj { as := j }) ≅ colimit X

The isomorphism ∐ (fun j => X.obj (Discrete.mk j)) ≅ colimit X.

@[simp]

theorem CategoryTheory.Limits.Sigma.ι_isoColimit_hom {α : Type w₂} {C : Type u} [Category.{v, u} C] (X : Functor (Discrete α) C) [HasCoproduct fun (j : α) => X.obj { as := j }] [HasColimit X] (j : α) : CategoryStruct.comp (ι (fun (j : α) => X.obj { as := j }) j) (isoColimit X).hom = colimit.ι X { as := j }

@[simp]

theorem CategoryTheory.Limits.Sigma.ι_isoColimit_hom_assoc {α : Type w₂} {C : Type u} [Category.{v, u} C] (X : Functor (Discrete α) C) [HasCoproduct fun (j : α) => X.obj { as := j }] [HasColimit X] (j : α) {Z : C} (h : colimit X ⟶ Z) : CategoryStruct.comp (ι (fun (j : α) => X.obj { as := j }) j) (CategoryStruct.comp (isoColimit X).hom h) = CategoryStruct.comp (colimit.ι X { as := j }) h

@[simp]

theorem CategoryTheory.Limits.Sigma.ι_isoColimit_inv {α : Type w₂} {C : Type u} [Category.{v, u} C] (X : Functor (Discrete α) C) [HasCoproduct fun (j : α) => X.obj { as := j }] [HasColimit X] (j : α) : CategoryStruct.comp (colimit.ι X { as := j }) (isoColimit X).inv = ι (fun (j : α) => X.obj { as := j }) j

@[simp]

theorem CategoryTheory.Limits.Sigma.ι_isoColimit_inv_assoc {α : Type w₂} {C : Type u} [Category.{v, u} C] (X : Functor (Discrete α) C) [HasCoproduct fun (j : α) => X.obj { as := j }] [HasColimit X] (j : α) {Z : C} (h : (∐ fun (j : α) => X.obj { as := j }) ⟶ Z) : CategoryStruct.comp (colimit.ι X { as := j }) (CategoryStruct.comp (isoColimit X).inv h) = CategoryStruct.comp (ι (fun (j : α) => X.obj { as := j }) j) h

noncomputable def CategoryTheory.Limits.Pi.whiskerEquiv {C : Type u} [Category.{v, u} C] {J : Type u_1} {K : Type u_2} {f : J → C} {g : K → C} (e : J ≃ K) (w : (j : J) → g (e j) ≅ f j) [HasProduct f] [HasProduct g] : ∏ᶜ f ≅ ∏ᶜ g

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

@[simp]

theorem CategoryTheory.Limits.Pi.whiskerEquiv_hom {C : Type u} [Category.{v, u} C] {J : Type u_1} {K : Type u_2} {f : J → C} {g : K → C} (e : J ≃ K) (w : (j : J) → g (e j) ≅ f j) [HasProduct f] [HasProduct g] : (whiskerEquiv e w).hom = map' ⇑e.symm fun (k : K) => CategoryStruct.comp (w (e.symm k)).inv (eqToHom ⋯)

@[simp]

theorem CategoryTheory.Limits.Pi.whiskerEquiv_inv {C : Type u} [Category.{v, u} C] {J : Type u_1} {K : Type u_2} {f : J → C} {g : K → C} (e : J ≃ K) (w : (j : J) → g (e j) ≅ f j) [HasProduct f] [HasProduct g] : (whiskerEquiv e w).inv = map' ⇑e fun (j : J) => (w j).hom

noncomputable def CategoryTheory.Limits.Sigma.whiskerEquiv {C : Type u} [Category.{v, u} C] {J : Type u_1} {K : Type u_2} {f : J → C} {g : K → C} (e : J ≃ K) (w : (j : J) → g (e j) ≅ f j) [HasCoproduct f] [HasCoproduct g] : ∐ f ≅ ∐ g

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

@[simp]

theorem CategoryTheory.Limits.Sigma.whiskerEquiv_inv {C : Type u} [Category.{v, u} C] {J : Type u_1} {K : Type u_2} {f : J → C} {g : K → C} (e : J ≃ K) (w : (j : J) → g (e j) ≅ f j) [HasCoproduct f] [HasCoproduct g] : (whiskerEquiv e w).inv = map' ⇑e.symm fun (k : K) => CategoryStruct.comp (eqToHom ⋯) (w (e.symm k)).hom

@[simp]

theorem CategoryTheory.Limits.Sigma.whiskerEquiv_hom {C : Type u} [Category.{v, u} C] {J : Type u_1} {K : Type u_2} {f : J → C} {g : K → C} (e : J ≃ K) (w : (j : J) → g (e j) ≅ f j) [HasCoproduct f] [HasCoproduct g] : (whiskerEquiv e w).hom = map' ⇑e fun (j : J) => (w j).inv

instance CategoryTheory.Limits.instHasProductSigmaFstSndOfPiObj {C : Type u} [Category.{v, u} C] {ι : Type u_1} (f : ι → Type u_2) (g : (i : ι) → f i → C) [∀ (i : ι), HasProduct (g i)] [HasProduct fun (i : ι) => ∏ᶜ g i] : HasProduct fun (p : (i : ι) × f i) => g p.fst p.snd

noncomputable def CategoryTheory.Limits.piPiIso {C : Type u} [Category.{v, u} C] {ι : Type u_1} (f : ι → Type u_2) (g : (i : ι) → f i → C) [∀ (i : ι), HasProduct (g i)] [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.

@[simp]

theorem CategoryTheory.Limits.piPiIso_inv {C : Type u} [Category.{v, u} C] {ι : Type u_1} (f : ι → Type u_2) (g : (i : ι) → f i → C) [∀ (i : ι), HasProduct (g i)] [HasProduct fun (i : ι) => ∏ᶜ g i] : (piPiIso f g).inv = Pi.lift fun (i : ι) => Pi.lift fun (x : f i) => Pi.π (fun (p : (i : ι) × f i) => g p.fst p.snd) ⟨i, x⟩

@[simp]

theorem CategoryTheory.Limits.piPiIso_hom {C : Type u} [Category.{v, u} C] {ι : Type u_1} (f : ι → Type u_2) (g : (i : ι) → f i → C) [∀ (i : ι), HasProduct (g i)] [HasProduct fun (i : ι) => ∏ᶜ g i] : (piPiIso f g).hom = Pi.lift fun (x : (i : ι) × f i) => match x with | ⟨i, x⟩ => CategoryStruct.comp (Pi.π (fun (i : ι) => ∏ᶜ g i) i) (Pi.π (g i) x)

instance CategoryTheory.Limits.instHasCoproductSigmaFstSndOfSigmaObj {C : Type u} [Category.{v, u} C] {ι : Type u_1} (f : ι → Type u_2) (g : (i : ι) → f i → C) [∀ (i : ι), HasCoproduct (g i)] [HasCoproduct fun (i : ι) => ∐ g i] : HasCoproduct fun (p : (i : ι) × f i) => g p.fst p.snd

noncomputable def CategoryTheory.Limits.sigmaSigmaIso {C : Type u} [Category.{v, u} C] {ι : Type u_1} (f : ι → Type u_2) (g : (i : ι) → f i → C) [∀ (i : ι), HasCoproduct (g i)] [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.

@[simp]

theorem CategoryTheory.Limits.sigmaSigmaIso_hom {C : Type u} [Category.{v, u} C] {ι : Type u_1} (f : ι → Type u_2) (g : (i : ι) → f i → C) [∀ (i : ι), HasCoproduct (g i)] [HasCoproduct fun (i : ι) => ∐ g i] : (sigmaSigmaIso f g).hom = Sigma.desc fun (i : ι) => Sigma.desc fun (x : f i) => Sigma.ι (fun (p : (i : ι) × f i) => g p.fst p.snd) ⟨i, x⟩

@[simp]

theorem CategoryTheory.Limits.sigmaSigmaIso_inv {C : Type u} [Category.{v, u} C] {ι : Type u_1} (f : ι → Type u_2) (g : (i : ι) → f i → C) [∀ (i : ι), HasCoproduct (g i)] [HasCoproduct fun (i : ι) => ∐ g i] : (sigmaSigmaIso f g).inv = Sigma.desc fun (x : (i : ι) × f i) => match x with | ⟨i, x⟩ => CategoryStruct.comp (Sigma.ι (g i) x) (Sigma.ι (fun (i : ι) => ∐ g i) i)

noncomputable def CategoryTheory.Limits.piComparison {β : Type w} {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) (f : β → C) [HasProduct f] [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.

@[simp]

theorem CategoryTheory.Limits.piComparison_comp_π {β : Type w} {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) (f : β → C) [HasProduct f] [HasProduct fun (b : β) => G.obj (f b)] (b : β) : CategoryStruct.comp (piComparison G f) (Pi.π (fun (b : β) => G.obj (f b)) b) = G.map (Pi.π f b)

@[simp]

theorem CategoryTheory.Limits.piComparison_comp_π_assoc {β : Type w} {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) (f : β → C) [HasProduct f] [HasProduct fun (b : β) => G.obj (f b)] (b : β) {Z : D} (h : G.obj (f b) ⟶ Z) : CategoryStruct.comp (piComparison G f) (CategoryStruct.comp (Pi.π (fun (b : β) => G.obj (f b)) b) h) = CategoryStruct.comp (G.map (Pi.π f b)) h

@[simp]

theorem CategoryTheory.Limits.map_lift_piComparison {β : Type w} {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) (f : β → C) [HasProduct f] [HasProduct fun (b : β) => G.obj (f b)] (P : C) (g : (j : β) → P ⟶ f j) : CategoryStruct.comp (G.map (Pi.lift g)) (piComparison G f) = Pi.lift fun (j : β) => G.map (g j)

@[simp]

theorem CategoryTheory.Limits.map_lift_piComparison_assoc {β : Type w} {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) (f : β → C) [HasProduct f] [HasProduct fun (b : β) => G.obj (f b)] (P : C) (g : (j : β) → P ⟶ f j) {Z : D} (h : (∏ᶜ fun (b : β) => G.obj (f b)) ⟶ Z) : CategoryStruct.comp (G.map (Pi.lift g)) (CategoryStruct.comp (piComparison G f) h) = CategoryStruct.comp (Pi.lift fun (j : β) => G.map (g j)) h

noncomputable def CategoryTheory.Limits.sigmaComparison {β : Type w} {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) (f : β → C) [HasCoproduct f] [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.

@[simp]

theorem CategoryTheory.Limits.ι_comp_sigmaComparison {β : Type w} {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) (f : β → C) [HasCoproduct f] [HasCoproduct fun (b : β) => G.obj (f b)] (b : β) : CategoryStruct.comp (Sigma.ι (fun (b : β) => G.obj (f b)) b) (sigmaComparison G f) = G.map (Sigma.ι f b)

@[simp]

theorem CategoryTheory.Limits.ι_comp_sigmaComparison_assoc {β : Type w} {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) (f : β → C) [HasCoproduct f] [HasCoproduct fun (b : β) => G.obj (f b)] (b : β) {Z : D} (h : G.obj (∐ f) ⟶ Z) : CategoryStruct.comp (Sigma.ι (fun (b : β) => G.obj (f b)) b) (CategoryStruct.comp (sigmaComparison G f) h) = CategoryStruct.comp (G.map (Sigma.ι f b)) h

@[simp]

theorem CategoryTheory.Limits.sigmaComparison_map_desc {β : Type w} {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) (f : β → C) [HasCoproduct f] [HasCoproduct fun (b : β) => G.obj (f b)] (P : C) (g : (j : β) → f j ⟶ P) : CategoryStruct.comp (sigmaComparison G f) (G.map (Sigma.desc g)) = Sigma.desc fun (j : β) => G.map (g j)

@[simp]

theorem CategoryTheory.Limits.sigmaComparison_map_desc_assoc {β : Type w} {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (G : Functor C D) (f : β → C) [HasCoproduct f] [HasCoproduct fun (b : β) => G.obj (f b)] (P : C) (g : (j : β) → f j ⟶ P) {Z : D} (h : G.obj P ⟶ Z) : CategoryStruct.comp (sigmaComparison G f) (CategoryStruct.comp (G.map (Sigma.desc g)) h) = CategoryStruct.comp (Sigma.desc fun (j : β) => G.map (g j)) h

def CategoryTheory.Limits.Fan.isLimitMapConeEquiv {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {ι : Type u_1} (X : ι → C) (c : Fan X) : IsLimit (F.mapCone c) ≃ IsLimit (mk (F.obj c.pt) fun (i : ι) => F.map (c.proj i))

F.mapCone c being limiting is the same as the induced fan being limiting.

def CategoryTheory.Limits.Cofan.isColimitMapCoconeEquiv {C : Type u} [Category.{v, u} C] {D : Type u₂} [Category.{v₂, u₂} D] (F : Functor C D) {ι : Type u_1} (X : ι → C) (c : Cofan X) : IsColimit (F.mapCocone c) ≃ IsColimit (mk (F.obj c.pt) fun (i : ι) => F.map (c.inj i))

F.mapCocone c being colimiting is the same as the induced cofan being colimiting.

@[reducible, inline]

abbrev CategoryTheory.Limits.HasProducts (C : Type u) [Category.{v, u} C] : Prop

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

@[reducible, inline]

abbrev CategoryTheory.Limits.HasCoproducts (C : Type u) [Category.{v, u} C] : Prop

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

theorem CategoryTheory.Limits.hasProducts_shrink {C : Type u} [Category.{v, u} C] [HasProducts C] : HasProducts C

theorem CategoryTheory.Limits.hasCoproducts_shrink {C : Type u} [Category.{v, u} C] [HasCoproducts C] : HasCoproducts C

theorem CategoryTheory.Limits.has_smallest_products_of_hasProducts {C : Type u} [Category.{v, u} C] [HasProducts C] : HasProducts C

theorem CategoryTheory.Limits.has_smallest_coproducts_of_hasCoproducts {C : Type u} [Category.{v, u} C] [HasCoproducts C] : HasCoproducts C

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

theorem CategoryTheory.Limits.hasCoproducts_of_colimit_cofans {C : Type u} [Category.{v, u} C] (cf : {J : Type w} → (f : J → C) → Cofan f) (cf_isColimit : {J : Type w} → (f : J → C) → IsColimit (cf f)) : HasCoproducts C

@[instance 100]

instance CategoryTheory.Limits.hasProductsOfShape_of_hasProducts {C : Type u} [Category.{v, u} C] [HasProducts C] (J : Type w) : HasProductsOfShape J C

@[instance 100]

instance CategoryTheory.Limits.hasCoproductsOfShape_of_hasCoproducts {C : Type u} [Category.{v, u} C] [HasCoproducts C] (J : Type w) : HasCoproductsOfShape J C

noncomputable def CategoryTheory.Limits.piConst {C : Type u} [Category.{v, u} C] [HasProducts C] : Functor C (Functor Type wᵒᵖ C)

The functor sending (X, n) to the product of copies of X indexed by n.

@[simp]

theorem CategoryTheory.Limits.piConst_map_app {C : Type u} [Category.{v, u} C] [HasProducts C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (n : Type wᵒᵖ) : (piConst.map f).app n = Pi.map fun (x : Opposite.unop n) => f

@[simp]

theorem CategoryTheory.Limits.piConst_obj_obj {C : Type u} [Category.{v, u} C] [HasProducts C] (X : C) (n : Type wᵒᵖ) : (piConst.obj X).obj n = ∏ᶜ fun (x : Opposite.unop n) => X

@[simp]

theorem CategoryTheory.Limits.piConst_obj_map {C : Type u} [Category.{v, u} C] [HasProducts C] (X : C) {X✝ Y✝ : Type wᵒᵖ} (f : X✝ ⟶ Y✝) : (piConst.obj X).map f = Pi.map' f.unop fun (x : Opposite.unop Y✝) => CategoryStruct.id X

noncomputable def CategoryTheory.Limits.piConstAdj {C : Type u} [Category.{v, u} C] [HasProducts C] (X : C) : (piConst.obj X).rightOp ⊣ yoneda.obj X

n ↦ ∏ₙ X is left adjoint to Hom(-, X).

noncomputable def CategoryTheory.Limits.sigmaConst {C : Type u} [Category.{v, u} C] [HasCoproducts C] : Functor C (Functor (Type w) C)

The functor sending (X, n) to the coproduct of copies of X indexed by n.

@[simp]

theorem CategoryTheory.Limits.sigmaConst_map_app {C : Type u} [Category.{v, u} C] [HasCoproducts C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (n : Type w) : (sigmaConst.map f).app n = Sigma.map fun (x : n) => f

@[simp]

theorem CategoryTheory.Limits.sigmaConst_obj_map {C : Type u} [Category.{v, u} C] [HasCoproducts C] (X : C) {X✝ Y✝ : Type w} (f : X✝ ⟶ Y✝) : (sigmaConst.obj X).map f = Sigma.map' f fun (x : X✝) => CategoryStruct.id X

@[simp]

theorem CategoryTheory.Limits.sigmaConst_obj_obj {C : Type u} [Category.{v, u} C] [HasCoproducts C] (X : C) (n : Type w) : (sigmaConst.obj X).obj n = ∐ fun (x : n) => X

noncomputable def CategoryTheory.Limits.sigmaConstAdj {C : Type u} [Category.{v, u} C] [HasCoproducts C] (X : C) : sigmaConst.obj X ⊣ coyoneda.obj (Opposite.op X)

n ↦ ∐ₙ X is left adjoint to Hom(X, -).

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

def CategoryTheory.Limits.limitConeOfUnique {β : Type w} {C : Type u} [Category.{v, u} C] [Unique β] (f : β → C) : LimitCone (Discrete.functor f)

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

@[simp]

theorem CategoryTheory.Limits.limitConeOfUnique_isLimit_lift {β : Type w} {C : Type u} [Category.{v, u} C] [Unique β] (f : β → C) (s : Cone (Discrete.functor f)) : (limitConeOfUnique f).isLimit.lift s = s.π.app default

@[simp]

theorem CategoryTheory.Limits.limitConeOfUnique_cone_pt {β : Type w} {C : Type u} [Category.{v, u} C] [Unique β] (f : β → C) : (limitConeOfUnique f).cone.pt = f default

@[simp]

theorem CategoryTheory.Limits.limitConeOfUnique_cone_π {β : Type w} {C : Type u} [Category.{v, u} C] [Unique β] (f : β → C) : (limitConeOfUnique f).cone.π = Discrete.natTrans fun (x : Discrete β) => match x with | { as := j } => eqToHom ⋯

@[instance 100]

instance CategoryTheory.Limits.hasProduct_unique {β : Type w} {C : Type u} [Category.{v, u} C] [Nonempty β] [Subsingleton β] (f : β → C) : HasProduct f

noncomputable def CategoryTheory.Limits.productUniqueIso {β : Type w} {C : Type u} [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.

@[simp]

theorem CategoryTheory.Limits.productUniqueIso_hom {β : Type w} {C : Type u} [Category.{v, u} C] [Unique β] (f : β → C) : (productUniqueIso f).hom = limit.π (Discrete.functor f) default

@[simp]

theorem CategoryTheory.Limits.productUniqueIso_inv {β : Type w} {C : Type u} [Category.{v, u} C] [Unique β] (f : β → C) : (productUniqueIso f).inv = limit.lift (Discrete.functor f) (limitConeOfUnique f).cone

def CategoryTheory.Limits.Fan.isLimitMkOfUnique {C : Type u} [Category.{v, u} C] {X Y : C} (e : X ≅ Y) (J : Type u_1) [Unique J] : IsLimit (mk X fun (x : J) => e.hom)

Any isomorphism is the projection from a single object product.

def CategoryTheory.Limits.colimitCoconeOfUnique {β : Type w} {C : Type u} [Category.{v, u} C] [Unique β] (f : β → C) : ColimitCocone (Discrete.functor f)

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

@[simp]

theorem CategoryTheory.Limits.colimitCoconeOfUnique_isColimit_desc {β : Type w} {C : Type u} [Category.{v, u} C] [Unique β] (f : β → C) (s : Cocone (Discrete.functor f)) : (colimitCoconeOfUnique f).isColimit.desc s = s.ι.app default

@[simp]

theorem CategoryTheory.Limits.colimitCoconeOfUnique_cocone_ι {β : Type w} {C : Type u} [Category.{v, u} C] [Unique β] (f : β → C) : (colimitCoconeOfUnique f).cocone.ι = Discrete.natTrans fun (x : Discrete β) => match x with | { as := j } => eqToHom ⋯

@[simp]

theorem CategoryTheory.Limits.colimitCoconeOfUnique_cocone_pt {β : Type w} {C : Type u} [Category.{v, u} C] [Unique β] (f : β → C) : (colimitCoconeOfUnique f).cocone.pt = f default

@[instance 100]

instance CategoryTheory.Limits.hasCoproduct_unique {β : Type w} {C : Type u} [Category.{v, u} C] [Nonempty β] [Subsingleton β] (f : β → C) : HasCoproduct f

noncomputable def CategoryTheory.Limits.coproductUniqueIso {β : Type w} {C : Type u} [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.

@[simp]

theorem CategoryTheory.Limits.coproductUniqueIso_hom {β : Type w} {C : Type u} [Category.{v, u} C] [Unique β] (f : β → C) : (coproductUniqueIso f).hom = colimit.desc (Discrete.functor f) (colimitCoconeOfUnique f).cocone

@[simp]

theorem CategoryTheory.Limits.coproductUniqueIso_inv {β : Type w} {C : Type u} [Category.{v, u} C] [Unique β] (f : β → C) : (coproductUniqueIso f).inv = colimit.ι (Discrete.functor f) default

def CategoryTheory.Limits.Cofan.isColimitMkOfUnique {C : Type u} [Category.{v, u} C] {X Y : C} (e : X ≅ Y) (J : Type u_1) [Unique J] : IsColimit (mk Y fun (x : J) => e.hom)

Any isomorphism is the projection from a single object product.

noncomputable def CategoryTheory.Limits.Pi.reindex {β : Type w} {C : Type u} [Category.{v, u} C] {γ : Type w'} (ε : β ≃ γ) (f : γ → C) [HasProduct f] [HasProduct (f ∘ ⇑ε)] : ∏ᶜ f ∘ ⇑ε ≅ ∏ᶜ f

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

@[simp]

theorem CategoryTheory.Limits.Pi.reindex_hom_π {β : Type w} {C : Type u} [Category.{v, u} C] {γ : Type w'} (ε : β ≃ γ) (f : γ → C) [HasProduct f] [HasProduct (f ∘ ⇑ε)] (b : β) : CategoryStruct.comp (reindex ε f).hom (π f (ε b)) = π (f ∘ ⇑ε) b

@[simp]

theorem CategoryTheory.Limits.Pi.reindex_hom_π_assoc {β : Type w} {C : Type u} [Category.{v, u} C] {γ : Type w'} (ε : β ≃ γ) (f : γ → C) [HasProduct f] [HasProduct (f ∘ ⇑ε)] (b : β) {Z : C} (h : f (ε b) ⟶ Z) : CategoryStruct.comp (reindex ε f).hom (CategoryStruct.comp (π f (ε b)) h) = CategoryStruct.comp (π (f ∘ ⇑ε) b) h

@[simp]

theorem CategoryTheory.Limits.Pi.reindex_inv_π {β : Type w} {C : Type u} [Category.{v, u} C] {γ : Type w'} (ε : β ≃ γ) (f : γ → C) [HasProduct f] [HasProduct (f ∘ ⇑ε)] (b : β) : CategoryStruct.comp (reindex ε f).inv (π (f ∘ ⇑ε) b) = π f (ε b)

@[simp]

theorem CategoryTheory.Limits.Pi.reindex_inv_π_assoc {β : Type w} {C : Type u} [Category.{v, u} C] {γ : Type w'} (ε : β ≃ γ) (f : γ → C) [HasProduct f] [HasProduct (f ∘ ⇑ε)] (b : β) {Z : C} (h : (f ∘ ⇑ε) b ⟶ Z) : CategoryStruct.comp (reindex ε f).inv (CategoryStruct.comp (π (f ∘ ⇑ε) b) h) = CategoryStruct.comp (π f (ε b)) h

def CategoryTheory.Limits.Fan.isLimitEquivOfEquiv {β : Type w} {C : Type u} [Category.{v, u} C] {γ : Type w'} (ε : β ≃ γ) {f : γ → C} (c : Fan f) : IsLimit c ≃ IsLimit (mk c.pt fun (i : β) => c.proj (ε i))

Being a limiting fan is stable under equivalences in the index type.

noncomputable def CategoryTheory.Limits.Sigma.reindex {β : Type w} {C : Type u} [Category.{v, u} C] {γ : Type w'} (ε : β ≃ γ) (f : γ → C) [HasCoproduct f] [HasCoproduct (f ∘ ⇑ε)] : ∐ f ∘ ⇑ε ≅ ∐ f

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

@[simp]

theorem CategoryTheory.Limits.Sigma.ι_reindex_hom {β : Type w} {C : Type u} [Category.{v, u} C] {γ : Type w'} (ε : β ≃ γ) (f : γ → C) [HasCoproduct f] [HasCoproduct (f ∘ ⇑ε)] (b : β) : CategoryStruct.comp (ι (f ∘ ⇑ε) b) (reindex ε f).hom = ι f (ε b)

@[simp]

theorem CategoryTheory.Limits.Sigma.ι_reindex_hom_assoc {β : Type w} {C : Type u} [Category.{v, u} C] {γ : Type w'} (ε : β ≃ γ) (f : γ → C) [HasCoproduct f] [HasCoproduct (f ∘ ⇑ε)] (b : β) {Z : C} (h : ∐ f ⟶ Z) : CategoryStruct.comp (ι (f ∘ ⇑ε) b) (CategoryStruct.comp (reindex ε f).hom h) = CategoryStruct.comp (ι f (ε b)) h

@[simp]

theorem CategoryTheory.Limits.Sigma.ι_reindex_inv {β : Type w} {C : Type u} [Category.{v, u} C] {γ : Type w'} (ε : β ≃ γ) (f : γ → C) [HasCoproduct f] [HasCoproduct (f ∘ ⇑ε)] (b : β) : CategoryStruct.comp (ι f (ε b)) (reindex ε f).inv = ι (f ∘ ⇑ε) b

@[simp]

theorem CategoryTheory.Limits.Sigma.ι_reindex_inv_assoc {β : Type w} {C : Type u} [Category.{v, u} C] {γ : Type w'} (ε : β ≃ γ) (f : γ → C) [HasCoproduct f] [HasCoproduct (f ∘ ⇑ε)] (b : β) {Z : C} (h : ∐ f ∘ ⇑ε ⟶ Z) : CategoryStruct.comp (ι f (ε b)) (CategoryStruct.comp (reindex ε f).inv h) = CategoryStruct.comp (ι (f ∘ ⇑ε) b) h

def CategoryTheory.Limits.Cofan.isColimitEquivOfEquiv {β : Type w} {C : Type u} [Category.{v, u} C] {γ : Type w'} (ε : β ≃ γ) {f : γ → C} (c : Cofan f) : IsColimit c ≃ IsColimit (mk c.pt fun (i : β) => c.inj (ε i))

Being a colimiting cofan is stable under equivalences in the index type.

instance CategoryTheory.Limits.instMonoLiftπ {C : Type u} [Category.{v, u} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J C) [HasLimit F] [HasProduct F.obj] : Mono (Pi.lift (limit.π F))

instance CategoryTheory.Limits.instEpiDescι {C : Type u} [Category.{v, u} C] {J : Type u₂} [Category.{v₂, u₂} J] (F : Functor J C) [HasColimit F] [HasCoproduct F.obj] : Epi (Sigma.desc (colimit.ι F))

def CategoryTheory.Limits.Fan.IsLimit.prod {C : Type u} [Category.{v, u} C] {ι : Type u_1} {ι' : Type u_2} {X : ι → ι' → C} (c : (i : ι) → Fan fun (j : ι') => X i j) (hc : (i : ι) → IsLimit (c i)) (c' : Fan fun (i : ι) => (c i).pt) (hc' : IsLimit c') : IsLimit (mk c'.pt fun (p : ι × ι') => CategoryStruct.comp (c'.proj p.1) ((c p.1).proj p.2))

A product over products is a product indexed by a product.

def CategoryTheory.Limits.Cofan.IsColimit.prod {C : Type u} [Category.{v, u} C] {ι : Type u_1} {ι' : Type u_2} {X : ι → ι' → C} (c : (i : ι) → Cofan fun (j : ι') => X i j) (hc : (i : ι) → IsColimit (c i)) (c' : Cofan fun (i : ι) => (c i).pt) (hc' : IsColimit c') : IsColimit (mk c'.pt fun (p : ι × ι') => CategoryStruct.comp ((c p.1).inj p.2) (c'.inj p.1))

A coproduct over coproducts is a coproduct indexed by a product.

noncomputable def CategoryTheory.Limits.piFunctor {C : Type u} [Category.{v, u} C] [HasProducts C] : Functor C (Functor Type wᵒᵖ C)

The functor C ⥤ (Type w)ᵒᵖ ⥤ C which sends X : C and α : Type w to the product of copies of X indexed by α.

@[simp]

theorem CategoryTheory.Limits.piFunctor_obj_obj {C : Type u} [Category.{v, u} C] [HasProducts C] (X : C) (α : Type wᵒᵖ) : (piFunctor.obj X).obj α = ∏ᶜ fun (t : Opposite.unop α) => X

@[simp]

theorem CategoryTheory.Limits.piFunctor_obj_map {C : Type u} [Category.{v, u} C] [HasProducts C] (X : C) {X✝ Y✝ : Type wᵒᵖ} (f : X✝ ⟶ Y✝) : (piFunctor.obj X).map f = Pi.map' f.unop fun (x : Opposite.unop Y✝) => CategoryStruct.id X

@[simp]

theorem CategoryTheory.Limits.piFunctor_map_app {C : Type u} [Category.{v, u} C] [HasProducts C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (T : Type wᵒᵖ) : (piFunctor.map f).app T = Pi.map fun (x : Opposite.unop T) => f

noncomputable def CategoryTheory.Limits.sigmaFunctor {C : Type u} [Category.{v, u} C] [HasCoproducts C] : Functor C (Functor (Type w) C)

The functor C ⥤ Type w ⥤ C which sends X : C and α : Type w to the coproduct of copies of X indexed by α.

@[simp]

theorem CategoryTheory.Limits.sigmaFunctor_obj_obj {C : Type u} [Category.{v, u} C] [HasCoproducts C] (X : C) (α : Type w) : (sigmaFunctor.obj X).obj α = ∐ fun (t : α) => X

@[simp]

theorem CategoryTheory.Limits.sigmaFunctor_map_app {C : Type u} [Category.{v, u} C] [HasCoproducts C] {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) (T : Type w) : (sigmaFunctor.map f).app T = Sigma.map fun (x : T) => f

@[simp]

theorem CategoryTheory.Limits.sigmaFunctor_obj_map {C : Type u} [Category.{v, u} C] [HasCoproducts C] (X : C) {X✝ Y✝ : Type w} (f : X✝ ⟶ Y✝) : (sigmaFunctor.obj X).map f = Sigma.map' f fun (x : X✝) => CategoryStruct.id X