mathlib documentation

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

source
@[reducible]
def category_theory.limits.fan {β : Type w} {C : Type u} [category_theory.category C] (f : β → C) :
Type (max w u v)

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

source
@[reducible]
def category_theory.limits.cofan {β : Type w} {C : Type u} [category_theory.category C] (f : β → C) :
Type (max w u v)

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

source
@[simp]
theorem category_theory.limits.fan.mk_π_app {β : Type w} {C : Type u} [category_theory.category C] {f : β → C} (P : C) (p : Π (b : β), P ⟶ f b) (X : category_theory.discrete β) :
(category_theory.limits.fan.mk P p).π.app X = p X.as
source
@[simp]
theorem category_theory.limits.fan.mk_X {β : Type w} {C : Type u} [category_theory.category C] {f : β → C} (P : C) (p : Π (b : β), P ⟶ f b) :
(category_theory.limits.fan.mk P p).X = P
source
def category_theory.limits.fan.mk {β : Type w} {C : Type u} [category_theory.category C] {f : β → C} (P : C) (p : Π (b : β), P ⟶ f b) :
category_theory.limits.fan f

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

Equations
source
@[simp]
theorem category_theory.limits.cofan.mk_X {β : Type w} {C : Type u} [category_theory.category C] {f : β → C} (P : C) (p : Π (b : β), f b ⟶ P) :
(category_theory.limits.cofan.mk P p).X = P
source
@[simp]
theorem category_theory.limits.cofan.mk_ι_app {β : Type w} {C : Type u} [category_theory.category C] {f : β → C} (P : C) (p : Π (b : β), f b ⟶ P) (X : category_theory.discrete β) :
(category_theory.limits.cofan.mk P p).ι.app X = p X.as
source
def category_theory.limits.cofan.mk {β : Type w} {C : Type u} [category_theory.category C] {f : β → C} (P : C) (p : Π (b : β), f b ⟶ P) :
category_theory.limits.cofan f

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

Equations
source
def category_theory.limits.fan.proj {β : Type w} {C : Type u} [category_theory.category C] {f : β → C} (p : category_theory.limits.fan f) (j : β) :
p.X ⟶ f j

Get the jth map in the fan

Equations
source
@[simp]
theorem category_theory.limits.fan_mk_proj {β : Type w} {C : Type u} [category_theory.category C] {f : β → C} (P : C) (p : Π (b : β), P ⟶ f b) (j : β) :
(category_theory.limits.fan.mk P p).proj j = p j
source
@[reducible]
def category_theory.limits.has_product {β : Type w} {C : Type u} [category_theory.category C] (f : β → C) :
Prop

An abbreviation for has_limit (discrete.functor f).

source
@[reducible]
def category_theory.limits.has_coproduct {β : Type w} {C : Type u} [category_theory.category C] (f : β → C) :
Prop

An abbreviation for has_colimit (discrete.functor f).

source
@[simp]
theorem category_theory.limits.mk_fan_limit_lift {β : Type w} {C : Type u} [category_theory.category C] {f : β → C} (t : category_theory.limits.fan f) (lift : Π (s : category_theory.limits.fan f), s.X ⟶ t.X) (fac : ∀ (s : category_theory.limits.fan f) (j : β), lift s ≫ t.proj j = s.proj j) (uniq : ∀ (s : category_theory.limits.fan f) (m : s.X ⟶ t.X), (∀ (j : β), m ≫ t.proj j = s.proj j) → m = lift s) (s : category_theory.limits.fan f) :
(category_theory.limits.mk_fan_limit t lift fac uniq).lift s = lift s
source
def category_theory.limits.mk_fan_limit {β : Type w} {C : Type u} [category_theory.category C] {f : β → C} (t : category_theory.limits.fan f) (lift : Π (s : category_theory.limits.fan f), s.X ⟶ t.X) (fac : ∀ (s : category_theory.limits.fan f) (j : β), lift s ≫ t.proj j = s.proj j) (uniq : ∀ (s : category_theory.limits.fan f) (m : s.X ⟶ t.X), (∀ (j : β), m ≫ t.proj j = s.proj j) → m = lift s) :
category_theory.limits.is_limit 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

Equations
source
@[reducible]
def category_theory.limits.has_products_of_shape (β : Type v) (C : Type u_1) [category_theory.category C] :
Prop

An abbreviation for has_limits_of_shape (discrete f).

source
@[reducible]
def category_theory.limits.has_coproducts_of_shape (β : Type v) (C : Type u_1) [category_theory.category C] :
Prop

An abbreviation for has_colimits_of_shape (discrete f).

source
@[reducible]
noncomputable def category_theory.limits.pi_obj {β : Type w} {C : Type u} [category_theory.category C] (f : β → C) [category_theory.limits.has_product f] :
C

pi_obj 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 pi_obj f, you will just use general facts about limits.)

source
@[reducible]
noncomputable def category_theory.limits.sigma_obj {β : Type w} {C : Type u} [category_theory.category C] (f : β → C) [category_theory.limits.has_coproduct f] :
C

sigma_obj 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 sigma_obj f, you will just use general facts about colimits.)

source
@[reducible]
noncomputable def category_theory.limits.pi.π {β : Type w} {C : Type u} [category_theory.category C] (f : β → C) [category_theory.limits.has_product f] (b : β) :
∏ f ⟶ f b

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

source
@[reducible]
noncomputable def category_theory.limits.sigma.ι {β : Type w} {C : Type u} [category_theory.category C] (f : β → C) [category_theory.limits.has_coproduct f] (b : β) :
f b ⟶ ∐ f

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

source
noncomputable def category_theory.limits.product_is_product {β : Type w} {C : Type u} [category_theory.category C] (f : β → C) [category_theory.limits.has_product f] :
category_theory.limits.is_limit (category_theory.limits.fan.mk (∏ f) (category_theory.limits.pi.π f))

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

Equations
source
noncomputable def category_theory.limits.coproduct_is_coproduct {β : Type w} {C : Type u} [category_theory.category C] (f : β → C) [category_theory.limits.has_coproduct f] :
category_theory.limits.is_colimit (category_theory.limits.cofan.mk (∐ f) (category_theory.limits.sigma.ι f))

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

Equations
source
@[reducible]
noncomputable def category_theory.limits.pi.lift {β : Type w} {C : Type u} [category_theory.category C] {f : β → C} [category_theory.limits.has_product f] {P : C} (p : Π (b : β), P ⟶ f b) :
P ⟶ ∏ f

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

source
@[reducible]
noncomputable def category_theory.limits.sigma.desc {β : Type w} {C : Type u} [category_theory.category C] {f : β → C} [category_theory.limits.has_coproduct f] {P : C} (p : Π (b : β), f b ⟶ P) :
∐ f ⟶ P

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

source
@[reducible]
noncomputable def category_theory.limits.pi.map {β : Type w} {C : Type u} [category_theory.category C] {f g : β → C} [category_theory.limits.has_product f] [category_theory.limits.has_product 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.

source
@[protected, instance]
def category_theory.limits.pi.map_mono {β : Type w} {C : Type u} [category_theory.category C] {f g : β → C} [category_theory.limits.has_product f] [category_theory.limits.has_product g] (p : Π (b : β), f b ⟶ g b) [∀ (i : β), category_theory.mono (p i)] :
category_theory.mono (category_theory.limits.pi.map p)
source
@[reducible]
noncomputable def category_theory.limits.pi.map_iso {β : Type w} {C : Type u} [category_theory.category C] {f g : β → C} [category_theory.limits.has_products_of_shape β 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.

source
@[reducible]
noncomputable def category_theory.limits.sigma.map {β : Type w} {C : Type u} [category_theory.category C] {f g : β → C} [category_theory.limits.has_coproduct f] [category_theory.limits.has_coproduct 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.

source
@[protected, instance]
def category_theory.limits.sigma.map_epi {β : Type w} {C : Type u} [category_theory.category C] {f g : β → C} [category_theory.limits.has_coproduct f] [category_theory.limits.has_coproduct g] (p : Π (b : β), f b ⟶ g b) [∀ (i : β), category_theory.epi (p i)] :
category_theory.epi (category_theory.limits.sigma.map p)
source
@[reducible]
noncomputable def category_theory.limits.sigma.map_iso {β : Type w} {C : Type u} [category_theory.category C] {f g : β → C} [category_theory.limits.has_coproducts_of_shape β 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.

source
noncomputable def category_theory.limits.pi_comparison {β : Type w} {C : Type u} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) (f : β → C) [category_theory.limits.has_product f] [category_theory.limits.has_product (λ (b : β), G.obj (f b))] :
G.obj (∏ f) ⟶ ∏ λ (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 preserves_product.of_iso_comparison.

Equations
Instances for category_theory.limits.pi_comparison
source
@[simp]
theorem category_theory.limits.pi_comparison_comp_π {β : Type w} {C : Type u} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) (f : β → C) [category_theory.limits.has_product f] [category_theory.limits.has_product (λ (b : β), G.obj (f b))] (b : β) :
category_theory.limits.pi_comparison G f ≫ category_theory.limits.pi.π (λ (b : β), G.obj (f b)) b = G.map (category_theory.limits.pi.π f b)
source
@[simp]
theorem category_theory.limits.pi_comparison_comp_π_assoc {β : Type w} {C : Type u} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) (f : β → C) [category_theory.limits.has_product f] [category_theory.limits.has_product (λ (b : β), G.obj (f b))] (b : β) {X' : D} (f' : G.obj (f b) ⟶ X') :
category_theory.limits.pi_comparison G f ≫ category_theory.limits.pi.π (λ (b : β), G.obj (f b)) b ≫ f' = G.map (category_theory.limits.pi.π f b) ≫ f'
source
@[simp]
theorem category_theory.limits.map_lift_pi_comparison {β : Type w} {C : Type u} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) (f : β → C) [category_theory.limits.has_product f] [category_theory.limits.has_product (λ (b : β), G.obj (f b))] (P : C) (g : Π (j : β), P ⟶ f j) :
G.map (category_theory.limits.pi.lift g) ≫ category_theory.limits.pi_comparison G f = category_theory.limits.pi.lift (λ (j : β), G.map (g j))
source
@[simp]
theorem category_theory.limits.map_lift_pi_comparison_assoc {β : Type w} {C : Type u} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) (f : β → C) [category_theory.limits.has_product f] [category_theory.limits.has_product (λ (b : β), G.obj (f b))] (P : C) (g : Π (j : β), P ⟶ f j) {X' : D} (f' : (∏ λ (b : β), G.obj (f b)) ⟶ X') :
G.map (category_theory.limits.pi.lift g) ≫ category_theory.limits.pi_comparison G f ≫ f' = category_theory.limits.pi.lift (λ (j : β), G.map (g j)) ≫ f'
source
noncomputable def category_theory.limits.sigma_comparison {β : Type w} {C : Type u} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) (f : β → C) [category_theory.limits.has_coproduct f] [category_theory.limits.has_coproduct (λ (b : β), G.obj (f b))] :
(∐ λ (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 preserves_coproduct.of_iso_comparison.

Equations
Instances for category_theory.limits.sigma_comparison
source
@[simp]
theorem category_theory.limits.ι_comp_sigma_comparison_assoc {β : Type w} {C : Type u} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) (f : β → C) [category_theory.limits.has_coproduct f] [category_theory.limits.has_coproduct (λ (b : β), G.obj (f b))] (b : β) {X' : D} (f' : G.obj (∐ f) ⟶ X') :
category_theory.limits.sigma.ι (λ (b : β), G.obj (f b)) b ≫ category_theory.limits.sigma_comparison G f ≫ f' = G.map (category_theory.limits.sigma.ι f b) ≫ f'
source
@[simp]
theorem category_theory.limits.ι_comp_sigma_comparison {β : Type w} {C : Type u} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) (f : β → C) [category_theory.limits.has_coproduct f] [category_theory.limits.has_coproduct (λ (b : β), G.obj (f b))] (b : β) :
category_theory.limits.sigma.ι (λ (b : β), G.obj (f b)) b ≫ category_theory.limits.sigma_comparison G f = G.map (category_theory.limits.sigma.ι f b)
source
@[simp]
theorem category_theory.limits.sigma_comparison_map_desc_assoc {β : Type w} {C : Type u} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) (f : β → C) [category_theory.limits.has_coproduct f] [category_theory.limits.has_coproduct (λ (b : β), G.obj (f b))] (P : C) (g : Π (j : β), f j ⟶ P) {X' : D} (f' : G.obj P ⟶ X') :
category_theory.limits.sigma_comparison G f ≫ G.map (category_theory.limits.sigma.desc g) ≫ f' = category_theory.limits.sigma.desc (λ (j : β), G.map (g j)) ≫ f'
source
@[simp]
theorem category_theory.limits.sigma_comparison_map_desc {β : Type w} {C : Type u} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C ⥤ D) (f : β → C) [category_theory.limits.has_coproduct f] [category_theory.limits.has_coproduct (λ (b : β), G.obj (f b))] (P : C) (g : Π (j : β), f j ⟶ P) :
category_theory.limits.sigma_comparison G f ≫ G.map (category_theory.limits.sigma.desc g) = category_theory.limits.sigma.desc (λ (j : β), G.map (g j))
source
@[reducible]
def category_theory.limits.has_products (C : Type u) [category_theory.category C] :
Prop

An abbreviation for Π J, has_limits_of_shape (discrete J) C

source
@[reducible]
def category_theory.limits.has_coproducts (C : Type u) [category_theory.category C] :
Prop

An abbreviation for Π J, has_colimits_of_shape (discrete J) C

source
theorem category_theory.limits.has_smallest_products_of_has_products {C : Type u} [category_theory.category C] [category_theory.limits.has_products C] :
category_theory.limits.has_products C
source
theorem category_theory.limits.has_smallest_coproducts_of_has_coproducts {C : Type u} [category_theory.category C] [category_theory.limits.has_coproducts C] :
category_theory.limits.has_coproducts C
source
theorem category_theory.limits.has_products_of_limit_fans {C : Type u} [category_theory.category C] (lf : Π {J : Type w} (f : J → C), category_theory.limits.fan f) (lf_is_limit : Π {J : Type w} (f : J → C), category_theory.limits.is_limit (lf f)) :
category_theory.limits.has_products C

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

source
@[simp]
theorem category_theory.limits.limit_cone_of_unique_is_limit_lift {β : Type w} {C : Type u} [category_theory.category C] [unique β] (f : β → C) (s : category_theory.limits.cone (category_theory.discrete.functor f)) :
(category_theory.limits.limit_cone_of_unique f).is_limit.lift s = s.π.app inhabited.default
source
@[simp]
theorem category_theory.limits.limit_cone_of_unique_cone_π_app {β : Type w} {C : Type u} [category_theory.category C] [unique β] (f : β → C) (j : category_theory.discrete β) :
(category_theory.limits.limit_cone_of_unique f).cone.π.app j = category_theory.eq_to_hom _
source
@[simp]
theorem category_theory.limits.limit_cone_of_unique_cone_X {β : Type w} {C : Type u} [category_theory.category C] [unique β] (f : β → C) :
(category_theory.limits.limit_cone_of_unique f).cone.X = f inhabited.default
source
def category_theory.limits.limit_cone_of_unique {β : Type w} {C : Type u} [category_theory.category C] [unique β] (f : β → C) :
category_theory.limits.limit_cone (category_theory.discrete.functor f)

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

Equations
source
@[protected, instance]
def category_theory.limits.has_product_unique {β : Type w} {C : Type u} [category_theory.category C] [unique β] (f : β → C) :
category_theory.limits.has_product f
source
noncomputable def category_theory.limits.product_unique_iso {β : Type w} {C : Type u} [category_theory.category C] [unique β] (f : β → C) :
∏ f ≅ f inhabited.default

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

Equations
source
@[simp]
theorem category_theory.limits.product_unique_iso_hom {β : Type w} {C : Type u} [category_theory.category C] [unique β] (f : β → C) :
(category_theory.limits.product_unique_iso f).hom = category_theory.limits.limit.π (category_theory.discrete.functor f) inhabited.default
source
@[simp]
theorem category_theory.limits.product_unique_iso_inv {β : Type w} {C : Type u} [category_theory.category C] [unique β] (f : β → C) :
(category_theory.limits.product_unique_iso f).inv = category_theory.limits.limit.lift (category_theory.discrete.functor f) (category_theory.limits.limit_cone_of_unique f).cone
source
@[simp]
theorem category_theory.limits.colimit_cocone_of_unique_cocone_X {β : Type w} {C : Type u} [category_theory.category C] [unique β] (f : β → C) :
(category_theory.limits.colimit_cocone_of_unique f).cocone.X = f inhabited.default
source
@[simp]
theorem category_theory.limits.colimit_cocone_of_unique_is_colimit_desc {β : Type w} {C : Type u} [category_theory.category C] [unique β] (f : β → C) (s : category_theory.limits.cocone (category_theory.discrete.functor f)) :
(category_theory.limits.colimit_cocone_of_unique f).is_colimit.desc s = s.ι.app inhabited.default
source
def category_theory.limits.colimit_cocone_of_unique {β : Type w} {C : Type u} [category_theory.category C] [unique β] (f : β → C) :
category_theory.limits.colimit_cocone (category_theory.discrete.functor f)

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

Equations
source
@[simp]
theorem category_theory.limits.colimit_cocone_of_unique_cocone_ι_app {β : Type w} {C : Type u} [category_theory.category C] [unique β] (f : β → C) (j : category_theory.discrete β) :
(category_theory.limits.colimit_cocone_of_unique f).cocone.ι.app j = category_theory.eq_to_hom _
source
@[protected, instance]
def category_theory.limits.has_coproduct_unique {β : Type w} {C : Type u} [category_theory.category C] [unique β] (f : β → C) :
category_theory.limits.has_coproduct f
source
noncomputable def category_theory.limits.coproduct_unique_iso {β : Type w} {C : Type u} [category_theory.category C] [unique β] (f : β → C) :
∐ f ≅ f inhabited.default

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

Equations
source
@[simp]
theorem category_theory.limits.coproduct_unique_iso_inv {β : Type w} {C : Type u} [category_theory.category C] [unique β] (f : β → C) :
(category_theory.limits.coproduct_unique_iso f).inv = category_theory.limits.colimit.ι (category_theory.discrete.functor f) inhabited.default
source
@[simp]
theorem category_theory.limits.coproduct_unique_iso_hom {β : Type w} {C : Type u} [category_theory.category C] [unique β] (f : β → C) :
(category_theory.limits.coproduct_unique_iso f).hom = category_theory.limits.colimit.desc (category_theory.discrete.functor f) (category_theory.limits.colimit_cocone_of_unique f).cocone
source
noncomputable def category_theory.limits.pi.reindex {β : Type w} {C : Type u} [category_theory.category C] {γ : Type v} (ε : β ≃ γ) (f : γ → C) [category_theory.limits.has_product f] [category_theory.limits.has_product (f ∘ ⇑ε)] :
∏ f ∘ ⇑ε ≅ ∏ f

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

Equations
source
@[simp]
theorem category_theory.limits.pi.reindex_hom_π_assoc {β : Type w} {C : Type u} [category_theory.category C] {γ : Type v} (ε : β ≃ γ) (f : γ → C) [category_theory.limits.has_product f] [category_theory.limits.has_product (f ∘ ⇑ε)] (b : β) {X' : C} (f' : f (⇑ε b) ⟶ X') :
(category_theory.limits.pi.reindex ε f).hom ≫ category_theory.limits.pi.π f (⇑ε b) ≫ f' = category_theory.limits.pi.π (f ∘ ⇑ε) b ≫ f'
source
@[simp]
theorem category_theory.limits.pi.reindex_hom_π {β : Type w} {C : Type u} [category_theory.category C] {γ : Type v} (ε : β ≃ γ) (f : γ → C) [category_theory.limits.has_product f] [category_theory.limits.has_product (f ∘ ⇑ε)] (b : β) :
(category_theory.limits.pi.reindex ε f).hom ≫ category_theory.limits.pi.π f (⇑ε b) = category_theory.limits.pi.π (f ∘ ⇑ε) b
source
@[simp]
theorem category_theory.limits.pi.reindex_inv_π {β : Type w} {C : Type u} [category_theory.category C] {γ : Type v} (ε : β ≃ γ) (f : γ → C) [category_theory.limits.has_product f] [category_theory.limits.has_product (f ∘ ⇑ε)] (b : β) :
(category_theory.limits.pi.reindex ε f).inv ≫ category_theory.limits.pi.π (f ∘ ⇑ε) b = category_theory.limits.pi.π f (⇑ε b)
source
@[simp]
theorem category_theory.limits.pi.reindex_inv_π_assoc {β : Type w} {C : Type u} [category_theory.category C] {γ : Type v} (ε : β ≃ γ) (f : γ → C) [category_theory.limits.has_product f] [category_theory.limits.has_product (f ∘ ⇑ε)] (b : β) {X' : C} (f' : (f ∘ ⇑ε) b ⟶ X') :
(category_theory.limits.pi.reindex ε f).inv ≫ category_theory.limits.pi.π (f ∘ ⇑ε) b ≫ f' = category_theory.limits.pi.π f (⇑ε b) ≫ f'
source
noncomputable def category_theory.limits.sigma.reindex {β : Type w} {C : Type u} [category_theory.category C] {γ : Type v} (ε : β ≃ γ) (f : γ → C) [category_theory.limits.has_coproduct f] [category_theory.limits.has_coproduct (f ∘ ⇑ε)] :
∐ f ∘ ⇑ε ≅ ∐ f

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

Equations
source
@[simp]
theorem category_theory.limits.sigma.ι_reindex_hom {β : Type w} {C : Type u} [category_theory.category C] {γ : Type v} (ε : β ≃ γ) (f : γ → C) [category_theory.limits.has_coproduct f] [category_theory.limits.has_coproduct (f ∘ ⇑ε)] (b : β) :
category_theory.limits.sigma.ι (f ∘ ⇑ε) b ≫ (category_theory.limits.sigma.reindex ε f).hom = category_theory.limits.sigma.ι f (⇑ε b)
source
@[simp]
theorem category_theory.limits.sigma.ι_reindex_hom_assoc {β : Type w} {C : Type u} [category_theory.category C] {γ : Type v} (ε : β ≃ γ) (f : γ → C) [category_theory.limits.has_coproduct f] [category_theory.limits.has_coproduct (f ∘ ⇑ε)] (b : β) {X' : C} (f' : ∐ f ⟶ X') :
category_theory.limits.sigma.ι (f ∘ ⇑ε) b ≫ (category_theory.limits.sigma.reindex ε f).hom ≫ f' = category_theory.limits.sigma.ι f (⇑ε b) ≫ f'
source
@[simp]
theorem category_theory.limits.sigma.ι_reindex_inv {β : Type w} {C : Type u} [category_theory.category C] {γ : Type v} (ε : β ≃ γ) (f : γ → C) [category_theory.limits.has_coproduct f] [category_theory.limits.has_coproduct (f ∘ ⇑ε)] (b : β) :
category_theory.limits.sigma.ι f (⇑ε b) ≫ (category_theory.limits.sigma.reindex ε f).inv = category_theory.limits.sigma.ι (f ∘ ⇑ε) b
source
@[simp]
theorem category_theory.limits.sigma.ι_reindex_inv_assoc {β : Type w} {C : Type u} [category_theory.category C] {γ : Type v} (ε : β ≃ γ) (f : γ → C) [category_theory.limits.has_coproduct f] [category_theory.limits.has_coproduct (f ∘ ⇑ε)] (b : β) {X' : C} (f' : ∐ f ∘ ⇑ε ⟶ X') :
category_theory.limits.sigma.ι f (⇑ε b) ≫ (category_theory.limits.sigma.reindex ε f).inv ≫ f' = category_theory.limits.sigma.ι (f ∘ ⇑ε) b ≫ f'