Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-02 07:21 5c4c1c08

View on Github →

feat(topology/homotopy): Fundamental groupoid preserves products (#11459)

Estimated changes

Modified src/category_theory/category/Groupoid.lean

added theorem category_theory.Groupoid.hom_to_functor

added theorem category_theory.Groupoid.pi_iso_pi_hom_π

added def category_theory.Groupoid.pi_limit_cone

added def category_theory.Groupoid.pi_limit_fan

Modified src/category_theory/discrete_category.lean

added def category_theory.discrete.comp_nat_iso_discrete

Modified src/category_theory/groupoid.lean

Modified src/category_theory/pi/basic.lean

added theorem category_theory.functor.eq_to_hom_proj

added def category_theory.functor.pi'

added theorem category_theory.functor.pi'_eval

added theorem category_theory.functor.pi_ext

Modified src/category_theory/products/basic.lean

added def category_theory.functor.prod'

Modified src/topology/homotopy/fundamental_groupoid.lean

modified theorem fundamental_groupoid.comp_eq

added def fundamental_groupoid.from_path

added def fundamental_groupoid.from_top

added theorem fundamental_groupoid.id_eq_path_refl

added def fundamental_groupoid.to_path

added def fundamental_groupoid.to_top

Modified src/topology/homotopy/product.lean

added def fundamental_groupoid_functor.cone_discrete_comp

added theorem fundamental_groupoid_functor.cone_discrete_comp_obj_map_cone

added def fundamental_groupoid_functor.pi_Top_to_pi_cone

added def fundamental_groupoid_functor.pi_iso

added def fundamental_groupoid_functor.pi_to_pi_Top

added def fundamental_groupoid_functor.preserves_product

added def fundamental_groupoid_functor.prod_iso

added def fundamental_groupoid_functor.prod_to_prod_Top

added def fundamental_groupoid_functor.proj

added def fundamental_groupoid_functor.proj_left

added theorem fundamental_groupoid_functor.proj_left_map

added theorem fundamental_groupoid_functor.proj_map

added def fundamental_groupoid_functor.proj_right

added theorem fundamental_groupoid_functor.proj_right_map