[Merged by Bors] - feat(CategoryTheory/Galois): fundamental group is limit of automorphism groups by chrisflav · Pull Request #12843 · leanprover-community/mathlib4

chrisflav · 2024-05-12T15:16:09Z

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.

depends on: [Merged by Bors] - feat(CategoryTheory/Limits): pro-coyoneda lemma #12841
depends on: [Merged by Bors] - feat(CategoryTheory/Galois): prorepresentability of fiber functors #12839

…orep.2

…chrisflav/galois-prorep.2

ghost · 2024-05-23T21:46:58Z

This PR/issue depends on:

~~[Merged by Bors] - feat(CategoryTheory/Limits): pro-coyoneda lemma #12841~~
~~[Merged by Bors] - feat(CategoryTheory/Galois): prorepresentability of fiber functors #12839~~
By Dependent Issues (🤖). Happy coding!

…orep.2

Mathlib/CategoryTheory/Galois/Prorepresentability.lean

github-actions · 2024-06-07T12:24:21Z

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%)

Mathlib/CategoryTheory/Galois/Prorepresentability.lean

joelriou · 2024-06-07T17:29:19Z

Thanks!

bors d+

mathlib-bors · 2024-06-07T17:29:22Z

✌️ 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 · 2024-06-07T21:04:13Z

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 · 2024-06-08T10:14:01Z

✌️ 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 · 2024-06-08T10:14:07Z

bors r+

chrisflav · 2024-06-08T10:14:42Z

Thanks for the review @joelriou !

…sm groups (#12843) 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.

mathlib-bors · 2024-06-08T11:23:54Z

Build failed:

Build

…orep.2

chrisflav · 2024-06-08T15:44:02Z

bors r+

…sm groups (#12843) 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.

mathlib-bors · 2024-06-08T17:32:03Z

Pull request successfully merged into master.

Build succeeded:

…sm groups (#12843) 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.

chrisflav added 15 commits March 8, 2024 21:38

prorep

070ad8e

Merge remote-tracking branch 'origin/master' into chrisflav/galois-pr…

f645a4c

…orep.2

Merge remote-tracking branch 'origin/master' into chrisflav/galois-pr…

487ef33

…orep.2

Merge remote-tracking branch 'origin/master' into chrisflav/galois-pr…

746ccf1

…orep.2

finish prorep

d1a42ee

refactor with structure

ca9a741

switch arrows around

afc50fb

remove trailing whitespace

f15c19d

prorepresentability of fiber functors

61eb945

fix imports and lint

7264565

cleanup

de7af7f

make new indyoneda file

977b1b7

update mathlib.lean

c3836bd

fix lint

10f6245

Merge remote-tracking branch 'origin/chrisflav/galois-prorep.3' into …

afcde22

…chrisflav/galois-prorep.2

chrisflav added awaiting-review awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. t-category-theory Category theory labels May 12, 2024

ghost added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label May 12, 2024

chrisflav mentioned this pull request May 12, 2024

[Merged by Bors] - feat(CategoryTheory/Limits): pro-coyoneda lemma #12841

Closed

add doc strings for additive versions

bf3f735

github-actions bot removed the awaiting-CI This PR does not pass CI yet. This label is automatically removed once it does. label May 12, 2024

ghost added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 14, 2024

ghost removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label May 23, 2024

Merge remote-tracking branch 'origin/master' into chrisflav/galois-pr…

fdc3e50

…orep.2

ghost removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label May 24, 2024

joelriou reviewed May 24, 2024

View reviewed changes

Mathlib/CategoryTheory/Galois/Prorepresentability.lean Outdated Show resolved Hide resolved

joelriou added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels May 24, 2024

joelriou reviewed Jun 7, 2024

View reviewed changes

Mathlib/CategoryTheory/Galois/Prorepresentability.lean Outdated Show resolved Hide resolved

joelriou added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Jun 7, 2024

adapt naming suggestion and fix docstring

a724083

chrisflav added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Jun 7, 2024

joelriou reviewed Jun 7, 2024

View reviewed changes

Mathlib/CategoryTheory/Galois/Prorepresentability.lean Outdated Show resolved Hide resolved

joelriou reviewed Jun 7, 2024

View reviewed changes

Mathlib/CategoryTheory/Galois/Prorepresentability.lean Outdated Show resolved Hide resolved

github-actions bot added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Jun 7, 2024

fix style

1075a42

fix docstring

5af9378

chrisflav added 2 commits June 8, 2024 13:26

Merge remote-tracking branch 'origin/master' into chrisflav/galois-pr…

fb21c8c

…orep.2

fix

35b9eb3

mathlib-bors bot changed the title ~~feat(CategoryTheory/Galois): fundamental group is limit of automorphism groups~~ [Merged by Bors] - feat(CategoryTheory/Galois): fundamental group is limit of automorphism groups Jun 8, 2024

mathlib-bors bot closed this Jun 8, 2024

mathlib-bors bot deleted the chrisflav/galois-prorep.2 branch June 8, 2024 17:32

Conversation

chrisflav commented May 12, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

ghost commented May 23, 2024

Uh oh!

Uh oh!

Uh oh!

github-actions bot commented Jun 7, 2024

Import summary

Uh oh!

Uh oh!

Uh oh!

joelriou commented Jun 7, 2024

Uh oh!

mathlib-bors bot commented Jun 7, 2024

Uh oh!

github-actions bot commented Jun 7, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary

Import changes

Declarations diff

Uh oh!

mathlib-bors bot commented Jun 8, 2024

Uh oh!

chrisflav commented Jun 8, 2024

Uh oh!

chrisflav commented Jun 8, 2024

Uh oh!

mathlib-bors bot commented Jun 8, 2024

Uh oh!

chrisflav commented Jun 8, 2024

Uh oh!

mathlib-bors bot commented Jun 8, 2024

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

chrisflav commented May 12, 2024 •

edited

Loading

github-actions bot commented Jun 7, 2024 •

edited

Loading