feat(AlgebraicTopology/SimplicialSet): the fundamental groupoid, as a pseudofunctor

[joelriou]

---

• depends on: feat(AlgebraicTopology/SimplicialSet/FundamentalGroupoid): homotopic maps induce isomorphic functors #42576
• depends on: chore(CategoryTheory): implicit_reducible for compositions of natural transformations #42528
• depends on: chore(CategoryTheory): composition implicit reducible in Type #42529
• depends on: feat(CategoryTheory/Groupoid): various induction principles for morphisms #42527
• depends on: feat(CategoryTheory): more API for IsoCat #42526
• depends on: feat(AlgebraicTopology/SimplicialSet): the fundamental groupoid #42523

[github-actions]

PR summary 41b6b2bcd7

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)	1025
Mathlib.AlgebraicTopology.SimplicialSet.FundamentalGroupoid.Homotopy (new file) Mathlib.AlgebraicTopology.SimplicialSet.FundamentalGroupoid.Pseudofunctor (new file)	1033

---

Declarations diff (regex)

+ CompStruct.ofSimplicialObjectHomotopy
+ CompStruct.ofSimplicialObjectHomotopy'
+ IsoCat.comp_functor_injective
+ IsoCat.functor_comp_injective
+ IsoCat.objEquiv
+ congrMapFundamentalGroupoid
+ congrMapFundamentalGroupoid'
+ congrMapFundamentalGroupoidOfEq
+ 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'
+ mapFundamentalGroupoidComp
+ mapFundamentalGroupoidId
+ mapFundamentalGroupoid_assoc
+ mapFundamentalGroupoid_comp
+ mapFundamentalGroupoid_comp_id
+ mapFundamentalGroupoid_id
+ mapFundamentalGroupoid_id_comp
+ mapIsoFundamentalGroupoid
+ mk
+ natIsoMk
+ natTransMk
+ natTrans_ext
+ ofSimplicialObjectHomotopy
+ ofSimplicialObjectHomotopy_edge
+ pseudofunctor
+ 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 -- pending)

Computed after the build finishes.

---

No changes to strong technical debt.

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

Current number	Change	Type (weak)
5052	3	exposed public sections

Current commit 41b6b2bcd7
Reference commit e13dd6052c

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/FundamentalGroupoid): homotopic maps induce isomorphic functors #42576
• chore(CategoryTheory): implicit_reducible for compositions of natural transformations #42528
• chore(CategoryTheory): composition implicit reducible in Type #42529
• feat(CategoryTheory/Groupoid): various induction principles for morphisms #42527
• feat(CategoryTheory): more API for IsoCat #42526
• feat(AlgebraicTopology/SimplicialSet): the fundamental groupoid #42523
  By Dependent Issues (🤖). Happy coding!