leanprover-community / leanprover-community/mathlib4
general theory of Galois categories
Open
Nobody has claimed this yet.
t-category-theory
- Dominant language
- Lean
- Stars
- 4.1k
- Forks
- 1.7k
- PR merge metrics
- No merged PRs in 30d
Description
This issue is meant as a way to track PRs on the development of the general theory of Galois categories. The rough outline is:
- Prove that any fiber functor
Finduces an equivalence with the category of finite, discreteAut F-sets. HereCshould not be required to be (essentially) small. - Develop the notion of
IsFundamentalGroup F Gfor a fiber functorFand a topological groupG. - Show that an exact functor between Galois categories induces a continuous homomorphism between fundamental groups.
- API for when this induced homomorphism is injective, surjective, etc.
The main chunk of the first point is already in mathlib. Already closed or still open PRs on this topic:
- #16441
- #16478
- #16661
- #16671
- #16664
- #16668
- #16948
- #16552
- #16673
Contributor guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Research direction
Start by reviewing the unchecked goals and the related issues and PRs listed in the tracker, especially the work on IsFundamentalGroup and induced homomorphisms. Use those discussions to identify the relevant existing Galois-category theory and API. Done means the remaining checklist items have been implemented and their corresponding PRs are complete.
Written by the indexing model from the issue text.
Assessment
- Domain
- devtools
- Issue type
- Feature
- Difficulty
- 5/5
- Estimated time
- Over a week
- Activity status
- Stale
- Clarity
- Mostly clear
- Newbie friendliness
- 25/100