feat(CategoryTheory/Galois): fundamental group is limit of automorphism groups

[chrisflav]

We show that the automorphism group of a fiber functor is isomorphic to the limit of the automorphism groups of all Galois objects.

From this we deduce that the automorphism group of a fiber functor acts transitively on the fibers of connected objects. This is the last essential step towards showing that a fiber functor induces a fully faithful embedding into the category of finite Aut F-types.

---

• [x] depends on: #12841
• [x] depends on: #12839

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#12841~~
• ~~leanprover-community/mathlib4#12839~~ By Dependent Issues (🤖). Happy coding!

[github-actions[bot]]

Import summary

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Galois.Prorepresentability	944	1021	+77 (+8.16%)
Mathlib.Algebra.Category.MonCat.Basic	486	487	+1 (+0.21%)
Mathlib.Algebra.Category.GroupCat.Basic	488	489	+1 (+0.20%)
Mathlib.CategoryTheory.Galois.Basic	849	850	+1 (+0.12%)

[joelriou]

Thanks!

bors d+

[mathlib-bors[bot]]

:v: chrisflav can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[github-actions[bot]]

PR summary

Import changes

Dependency changes

File	Base Count	Head Count	Change
Mathlib.CategoryTheory.Galois.Prorepresentability	944	1021	+77 (+8.16%)
Mathlib.Algebra.Category.MonCat.Basic	486	487	+1 (+0.21%)
Mathlib.Algebra.Category.GroupCat.Basic	488	489	+1 (+0.20%)
Mathlib.CategoryTheory.Galois.Basic	849	850	+1 (+0.12%)

---

Declarations diff

+ AutGalois + AutGalois.ext + AutGalois.π + AutGalois.π_apply + AutGalois.π_surjective + FiberFunctor.isPretransitive_of_isConnected + FiberFunctor.isPretransitive_of_isGalois + FibreFunctor.end_isIso + FibreFunctor.end_isUnit + autGaloisSystem_map_surjective + autIsoFibers + autIsoFibers_inv_app + autMulEquivAutGalois + autMulEquivAutGalois_symm_app + autMulEquivAutGalois_π + endEquivAutGalois + endEquivAutGalois_mul + endEquivAutGalois_π + endEquivSectionsFibers + endEquivSectionsFibers_π + endMulEquivAutGalois + endMulEquivAutGalois_pi + instance (X : C) : MulAction (Aut F) (F.obj X) + instance : Group (AutGalois F) + mulAction_def + sectionsπMonoidHom ++++ uliftFunctor

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[mathlib-bors[bot]]

:v: chrisflav can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[chrisflav]

bors r+

[chrisflav]

Thanks for the review @joelriou !

[mathlib-bors[bot]]

Build failed:

• Build

[chrisflav]

bors r+

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style