Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-12 11:06 2241588b

View on Github →

feat(topology/homotopy): Homotopic maps induce naturally isomorphic functors between fundamental groupoid (#11595)

Estimated changes

Modified src/category_theory/category/Groupoid.lean

added theorem category_theory.Groupoid.id_to_functor

Modified src/topology/homotopy/fundamental_groupoid.lean

added theorem fundamental_groupoid.map_eq

Created src/topology/homotopy/induced_maps.lean

added theorem continuous_map.homotopy.apply_one_path

added theorem continuous_map.homotopy.apply_zero_path

added def continuous_map.homotopy.diagonal_path'

added def continuous_map.homotopy.diagonal_path

added theorem continuous_map.homotopy.eq_diag_path

added theorem continuous_map.homotopy.eq_path_of_eq_image

added theorem continuous_map.homotopy.eval_at_eq

added def continuous_map.homotopy.hcast

added theorem continuous_map.homotopy.hcast_def

added theorem continuous_map.homotopy.heq_path_of_eq_image

added def continuous_map.homotopy.prod_to_prod_Top_I

added theorem continuous_map.homotopy.ulift_apply

added def continuous_map.homotopy.ulift_map

added def fundamental_groupoid_functor.equiv_of_homotopy_equiv

added def fundamental_groupoid_functor.homotopic_maps_nat_iso

added def unit_interval.path01

added def unit_interval.uhpath01

added def unit_interval.upath01

Modified src/topology/homotopy/path.lean

added def continuous_map.homotopy.eval_at

added theorem path.homotopic.hpath_hext

Modified src/topology/homotopy/product.lean

added theorem fundamental_groupoid_functor.prod_to_prod_Top_map