Preserving products #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 map of a fan is a limit iff the fan consisting of the mapped morphisms is a limit. This
essentially lets us commute fan.mk
with functor.map_cone
.
Equations
- category_theory.limits.is_limit_map_cone_fan_mk_equiv G f g = (category_theory.limits.is_limit.postcompose_hom_equiv (category_theory.discrete.nat_iso (λ (j : category_theory.discrete J), category_theory.iso.refl (G.obj (f j.as)))) (G.map_cone (category_theory.limits.fan.mk P g))).symm.trans (category_theory.limits.is_limit.equiv_iso_limit (category_theory.limits.cones.ext (category_theory.iso.refl ((category_theory.limits.cones.postcompose (category_theory.discrete.nat_iso (λ (j : category_theory.discrete J), category_theory.iso.refl (G.obj (f j.as)))).hom).obj (G.map_cone (category_theory.limits.fan.mk P g))).X) _))
The property of preserving products expressed in terms of fans.
Equations
The property of reflecting products expressed in terms of fans.
Equations
- category_theory.limits.is_limit_of_is_limit_fan_mk_obj G f g t = category_theory.limits.reflects_limit.reflects (⇑((category_theory.limits.is_limit_map_cone_fan_mk_equiv G (λ (j : J), f j) (λ (j : J), g j)).symm) t)
If G
preserves products and C
has them, then the fan constructed of the mapped projection of a
product is a limit.
Equations
- category_theory.limits.is_limit_of_has_product_of_preserves_limit G f = category_theory.limits.is_limit_fan_mk_obj_of_is_limit G f (λ (j : J), category_theory.limits.pi.π f j) (category_theory.limits.product_is_product (λ (j : J), f j))
If pi_comparison G f
is an isomorphism, then G
preserves the limit of f
.
Equations
- category_theory.limits.preserves_product.of_iso_comparison G f = category_theory.limits.preserves_limit_of_preserves_limit_cone (category_theory.limits.product_is_product f) (⇑((category_theory.limits.is_limit_map_cone_fan_mk_equiv G (λ (j : J), f j) (category_theory.limits.pi.π f)).symm) (category_theory.limits.limit.is_limit (category_theory.discrete.functor (λ (j : J), G.obj (f j)))).of_point_iso)
If G
preserves limits, we have an isomorphism from the image of a product to the product of the
images.
The map of a cofan is a colimit iff the cofan consisting of the mapped morphisms is a colimit.
This essentially lets us commute cofan.mk
with functor.map_cocone
.
Equations
- category_theory.limits.is_colimit_map_cocone_cofan_mk_equiv G f g = (category_theory.limits.is_colimit.precompose_hom_equiv (category_theory.discrete.nat_iso (λ (j : category_theory.discrete J), category_theory.iso.refl (G.obj (f j.as)))) (G.map_cocone (category_theory.limits.cofan.mk P g))).symm.trans (category_theory.limits.is_colimit.equiv_iso_colimit (category_theory.limits.cocones.ext (category_theory.iso.refl ((category_theory.limits.cocones.precompose (category_theory.discrete.nat_iso (λ (j : category_theory.discrete J), category_theory.iso.refl (G.obj (f j.as)))).hom).obj (G.map_cocone (category_theory.limits.cofan.mk P g))).X) _))
The property of preserving coproducts expressed in terms of cofans.
Equations
The property of reflecting coproducts expressed in terms of cofans.
Equations
- category_theory.limits.is_colimit_of_is_colimit_cofan_mk_obj G f g t = category_theory.limits.reflects_colimit.reflects (⇑((category_theory.limits.is_colimit_map_cocone_cofan_mk_equiv G (λ (j : J), f j) (λ (j : J), g j)).symm) t)
If G
preserves coproducts and C
has them,
then the cofan constructed of the mapped inclusion of a coproduct is a colimit.
Equations
If sigma_comparison G f
is an isomorphism, then G
preserves the colimit of f
.
Equations
- category_theory.limits.preserves_coproduct.of_iso_comparison G f = category_theory.limits.preserves_colimit_of_preserves_colimit_cocone (category_theory.limits.coproduct_is_coproduct f) (⇑((category_theory.limits.is_colimit_map_cocone_cofan_mk_equiv G (λ (j : J), f j) (category_theory.limits.sigma.ι f)).symm) (category_theory.limits.colimit.is_colimit (category_theory.discrete.functor (λ (j : J), G.obj (f j)))).of_point_iso)
If G
preserves colimits,
we have an isomorphism from the image of a coproduct to the coproduct of the images.