feat(AlgebraicTopology/SimplicialSet/FundamentalGroupoid): homotopic maps induce isomorphic functors

[joelriou]

---

• depends on: feat(AlgebraicTopology/SimplicialSet): the fundamental groupoid #42523
• depends on: feat(CategoryTheory): more API for IsoCat #42526
• depends on: feat(CategoryTheory/Groupoid): various induction principles for morphisms #42527

[github-actions]

PR summary 78e901a951

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.AlgebraicTopology.SimplicialSet.FundamentalGroupoid.Basic (new file)	1027
Mathlib.AlgebraicTopology.SimplicialSet.FundamentalGroupoid.Homotopy (new file)	1035

---

Declarations diff (regex)

+ CompStruct.ofSimplicialObjectHomotopy
+ CompStruct.ofSimplicialObjectHomotopy'
+ IsoCat.comp_functor_injective
+ IsoCat.functor_comp_injective
+ IsoCat.objEquiv
+ congrMapFundamentalGroupoid
+ congrMapFundamentalGroupoid'
+ desc'
+ descMap
+ descMap_homMk
+ diagOfSimplicialObjectHomotopy
+ diagOfSimplicialObjectHomotopy_edge
+ diagOfSimplicialObjectHomotopy_edge'
+ equivFreeGroupoid
+ equivalence
+ equivalenceFreeGroupoid
+ instance : Category (FundamentalGroupoid X)
+ instance : Groupoid (FundamentalGroupoid X)
+ instance {X Y : SSet.Truncated.{u} 2} (f : X ⟶ Y) [IsIso f] :
+ isEquivalence_mapFundamentalGroupoid
+ isoCat
+ isoCatFreeGroupoid
+ isoCatMapFundamentalGroupoid
+ lift_unique'
+ mapFundamentalGroupoid_comp
+ mapFundamentalGroupoid_id
+ mapIsoFundamentalGroupoid
+ mk
+ natIsoMk
+ natTransMk
+ ofSimplicialObjectHomotopy
+ ofSimplicialObjectHomotopy_edge
+ rec
++ Edge.CompStruct.homMk_comp
++ FundamentalGroupoid
++ desc
++ desc_map_homMk
++ desc_obj_mk
++ functor_ext
++ homMk
++ homMk_id
++ mapFundamentalGroupoid
++ mapFundamentalGroupoid_map_homMk
++ mapFundamentalGroupoid_obj_mk
++ mk_surjective
+++++ hom_rec

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

Declarations diff (Lean)

✅ Lean-aware diff — post-build, computed from the Lean environment (commit 78e901a).

• +83 new declarations
• −0 removed declarations

+CategoryTheory.FreeGroupoid.hom_rec
+CategoryTheory.FreeGroupoid.lift_unique'
+CategoryTheory.InducedCategory.equivalence
+CategoryTheory.InducedCategory.isoCat
+CategoryTheory.InducedCategory.isoCat_functor
+CategoryTheory.InducedCategory.isoCat_inverse_map_hom
+CategoryTheory.InducedCategory.isoCat_inverse_obj
+CategoryTheory.IsoCat.comp_functor_injective
+CategoryTheory.IsoCat.functor_comp_injective
+CategoryTheory.IsoCat.objEquiv
+CategoryTheory.IsoCat.objEquiv_apply
+CategoryTheory.IsoCat.objEquiv_symm_apply
+Quiver.FreeGroupoid.hom_rec
+SSet.Edge.CompStruct.homMk_comp
+SSet.Edge.CompStruct.homMk_comp_assoc
+SSet.Edge.CompStruct.ofSimplicialObjectHomotopy
+SSet.Edge.CompStruct.ofSimplicialObjectHomotopy'
+SSet.Edge.diagOfSimplicialObjectHomotopy
+SSet.Edge.diagOfSimplicialObjectHomotopy_edge
+SSet.Edge.diagOfSimplicialObjectHomotopy_edge'
+SSet.Edge.ofSimplicialObjectHomotopy
+SSet.Edge.ofSimplicialObjectHomotopy_edge
+SSet.FundamentalGroupoid
+SSet.FundamentalGroupoid.desc
+SSet.FundamentalGroupoid.desc_map_homMk
+SSet.FundamentalGroupoid.desc_obj_mk
+SSet.FundamentalGroupoid.functor_ext
+SSet.FundamentalGroupoid.homMk
+SSet.FundamentalGroupoid.homMk_id
+SSet.FundamentalGroupoid.hom_rec
+SSet.FundamentalGroupoid.mk
+SSet.FundamentalGroupoid.mk_surjective
+SSet.FundamentalGroupoid.natIsoMk
+SSet.FundamentalGroupoid.natIsoMk_hom_app
+SSet.FundamentalGroupoid.natIsoMk_inv_app
+SSet.FundamentalGroupoid.natTransMk
+SSet.FundamentalGroupoid.natTransMk_app
+SSet.FundamentalGroupoid.rec
+SSet.Truncated.Edge.CompStruct.homMk_comp
+SSet.Truncated.Edge.CompStruct.homMk_comp_assoc
+SSet.Truncated.FundamentalGroupoid
+SSet.Truncated.FundamentalGroupoid.casesOn
+SSet.Truncated.FundamentalGroupoid.ctorIdx
+SSet.Truncated.FundamentalGroupoid.desc
+SSet.Truncated.FundamentalGroupoid.descMap
+SSet.Truncated.FundamentalGroupoid.descMap_homMk
+SSet.Truncated.FundamentalGroupoid.desc_map_homMk
+SSet.Truncated.FundamentalGroupoid.desc_obj_mk
+SSet.Truncated.FundamentalGroupoid.equivFreeGroupoid
+SSet.Truncated.FundamentalGroupoid.equivalenceFreeGroupoid
+SSet.Truncated.FundamentalGroupoid.functor_ext
+SSet.Truncated.FundamentalGroupoid.homMk
+SSet.Truncated.FundamentalGroupoid.homMk_id
+SSet.Truncated.FundamentalGroupoid.hom_rec
+SSet.Truncated.FundamentalGroupoid.instCategory
+SSet.Truncated.FundamentalGroupoid.instGroupoid
+SSet.Truncated.FundamentalGroupoid.isoCatFreeGroupoid
+SSet.Truncated.FundamentalGroupoid.mk
+SSet.Truncated.FundamentalGroupoid.mk.inj
+SSet.Truncated.FundamentalGroupoid.mk.injEq
+SSet.Truncated.FundamentalGroupoid.mk.noConfusion
+SSet.Truncated.FundamentalGroupoid.mk.sizeOf_spec
+SSet.Truncated.FundamentalGroupoid.mk_surjective
+SSet.Truncated.FundamentalGroupoid.noConfusion
+SSet.Truncated.FundamentalGroupoid.noConfusionType
+SSet.Truncated.FundamentalGroupoid.pt
+SSet.Truncated.FundamentalGroupoid.rec
+SSet.Truncated.FundamentalGroupoid.recOn
+SSet.Truncated.HomotopyCategory.hom_rec
+SSet.Truncated.instIsEquivalenceFundamentalGroupoidMapFundamentalGroupoidOfIsIsoOfNatNat
+SSet.Truncated.mapFundamentalGroupoid
+SSet.Truncated.mapFundamentalGroupoid_comp
+SSet.Truncated.mapFundamentalGroupoid_id
+SSet.Truncated.mapFundamentalGroupoid_map_homMk
+SSet.Truncated.mapFundamentalGroupoid_obj_mk
+SSet.Truncated.mapIsoFundamentalGroupoid
+SSet.congrMapFundamentalGroupoid
+SSet.congrMapFundamentalGroupoid'
+SSet.isEquivalence_mapFundamentalGroupoid
+SSet.isoCatMapFundamentalGroupoid
+SSet.mapFundamentalGroupoid
+SSet.mapFundamentalGroupoid_map_homMk
+SSet.mapFundamentalGroupoid_obj_mk

---

No changes to strong technical debt.

Increase in weak tech debt: (relative, absolute) = (2.00, 0.00)

Current number	Change	Type (weak)
5051	2	exposed public sections

Current commit 78e901a951
Reference commit daa38bd533

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[mathlib-dependent-issues]

This PR/issue depends on:

• feat(AlgebraicTopology/SimplicialSet): the fundamental groupoid #42523
• feat(CategoryTheory): more API for IsoCat #42526
• feat(CategoryTheory/Groupoid): various induction principles for morphisms #42527
  By Dependent Issues (🤖). Happy coding!