Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-10 15:19 47861363

View on Github →

feat(category_theory/limits): explicit isomorphisms between preserved limits (#3602) When G preserves limits, it's nice to be able to quickly obtain the iso G.obj (pi_obj f) ≅ pi_obj (λ j, G.obj (f j)).

Estimated changes

Modified src/algebra/category/Group/limits.lean

Modified src/category_theory/limits/connected.lean

Modified src/category_theory/limits/creates.lean

Modified src/category_theory/limits/functor_category.lean

Modified src/category_theory/limits/over.lean

Renamed src/category_theory/limits/preserves.lean to src/category_theory/limits/preserves/basic.lean

Created src/category_theory/limits/preserves/shapes.lean

added theorem map_lift_comp_preserves_products_iso_hom

added def preserves_limits_iso

added theorem preserves_limits_iso_hom_π

added def preserves_products_iso

added theorem preserves_products_iso_hom_π

Modified src/category_theory/limits/shapes/constructions/preserve_binary_products.lean

Modified src/category_theory/limits/shapes/regular_mono.lean

Modified src/topology/category/Top/limits.lean