mathlib documentation

category_theory.limits.shapes.products

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

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

source
def category_theory.limits.cofan {β : Type v} {C : Type u} [category_theory.category C] (f : β → C) :
Type (max 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 v} {C : Type u} [category_theory.category C] {f : β → C} (P : C) (p : Π (b : β), P ⟶ f b) (b : β) :
(category_theory.limits.fan.mk P p).π.app b = p b

source
@[simp]
theorem category_theory.limits.fan.mk_X {β : Type v} {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 v} {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 v} {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 v} {C : Type u} [category_theory.category C] {f : β → C} (P : C) (p : Π (b : β), f b ⟶ P) (b : β) :
(category_theory.limits.cofan.mk P p).ι.app b = p b

source
def category_theory.limits.cofan.mk {β : Type v} {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.has_product {β : Type v} {C : Type u} [category_theory.category C] (f : β → C) :
Prop

An abbreviation for has_limit (discrete.functor f).

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

An abbreviation for has_colimit (discrete.functor f).

source
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
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
def category_theory.limits.pi_obj {β : Type v} {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
def category_theory.limits.sigma_obj {β : Type v} {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
def category_theory.limits.pi.π {β : Type v} {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
def category_theory.limits.sigma.ι {β : Type v} {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
def category_theory.limits.product_is_product {β : Type v} {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
def category_theory.limits.pi.lift {β : Type v} {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
def category_theory.limits.sigma.desc {β : Type v} {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
def category_theory.limits.pi.map {β : Type v} {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
def category_theory.limits.pi.map_iso {β : Type v} {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
def category_theory.limits.sigma.map {β : Type v} {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
def category_theory.limits.sigma.map_iso {β : Type v} {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
def category_theory.limits.pi_comparison {β : Type v} {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.

Equations
source
@[simp]
theorem category_theory.limits.pi_comparison_comp_π {β : Type v} {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 v} {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 v} {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 v} {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
def category_theory.limits.sigma_comparison {β : Type v} {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.

Equations
source
@[simp]
theorem category_theory.limits.ι_comp_sigma_comparison_assoc {β : Type v} {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 v} {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 v} {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 v} {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
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

Instances
source
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