mathlib documentation

category_theory.limits.preserves.shapes.products

Preserving products #

Constructions to relate the notions of preserving products and reflecting products to concrete fans.

In particular, we show that pi_comparison G f is an isomorphism iff G preserves the limit of f.

The property of reflecting products expressed in terms of fans.

Equations
noncomputable def category_theory.limits.preserves_product.iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C D) {J : Type w} (f : J → C) [category_theory.limits.has_product f] [category_theory.limits.has_product (λ (j : J), G.obj (f j))] [category_theory.limits.preserves_limit (category_theory.discrete.functor f) G] :
G.obj ( f) λ (j : J), G.obj (f j)

If G preserves limits, we have an isomorphism from the image of a product to the product of the images.

Equations
noncomputable def category_theory.limits.preserves_coproduct.iso {C : Type u₁} [category_theory.category C] {D : Type u₂} [category_theory.category D] (G : C D) {J : Type w} (f : J → C) [category_theory.limits.has_coproduct f] [category_theory.limits.has_coproduct (λ (j : J), G.obj (f j))] [category_theory.limits.preserves_colimit (category_theory.discrete.functor f) G] :
G.obj ( f) λ (j : J), G.obj (f j)

If G preserves colimits, we have an isomorphism from the image of a coproduct to the coproduct of the images.

Equations