Universal property of fundamental group #
Let C be a Galois category with fiber functor F. While in informal mathematics, we tend to
identify known groups from other contexts (e.g. the absolute Galois group of a field) with
the automorphism group Aut F of certain fiber functors F, this causes friction in formalization.
Hence, in this file we develop conditions when a topological group G is canonically isomorphic to
the automorphism group Aut F of F. Consequently, the API for Galois categories and their fiber
functors should be stated in terms of an abstract topological group G satisfying
IsFundamentalGroup in the places where Aut F would appear.
Main definition #
Given a compact, topological group G with an action on F.obj X on each X, we say that
G is a fundamental group of F (IsFundamentalGroup F G), if
naturality: theG-action onF.obj Xis compatible with morphisms inCtransitive_of_isGalois:Gacts transitively onF.obj Xfor all Galois objectsX : Ccontinuous_smul: the action ofGonF.obj Xis continuous ifF.obj Xis equipped with the discrete topology for allX : C.non_trivial': ifg : Gacts trivial on allF.obj X, theng = 1`.
Given this data, we define toAut F G : G →* Aut F in the natural way.
Main results #
toAut_bijective:toAut F Gis a group isomorphism givenIsFundamentalGroup F G.toAut_isHomeomorph:toAut F Gis a homeomorphism givenIsFundamentalGroup F G.
TODO #
- Develop further equivalent conditions, in particular, relate the condition
non_trivialwithGbeing aT2Space.
We say G acts naturally on the fibers of F if for every f : X ⟶ Y, the G-actions
on F.obj X and F.obj Y are compatible with F.map f.
Instances
If G acts naturally on F.obj X for each X : C, this is the canonical
group homomorphism into the automorphism group of F.
Equations
- CategoryTheory.PreGaloisCategory.toAut F G = { toFun := fun (g : G) => CategoryTheory.NatIso.ofComponents (CategoryTheory.PreGaloisCategory.isoOnObj✝ F g) ⋯, map_one' := ⋯, map_mul' := ⋯ }
Instances For
toAut is injective, if only the identity acts trivially on every fiber.
If G is a compact, topological group that acts continuously and naturally on the
fibers of F, toAut F G is surjective if and only if it acts transitively on the fibers
of all Galois objects. This is the if direction. For the only if see
isPretransitive_of_surjective.
If toAut F G is surjective, then G acts transitively on the fibers of connected objects.
For a converse see toAut_surjective.
A compact, topological group G with a natural action on F.obj X for each X : C
is a fundamental group of F, if G acts transitively on the fibers of Galois objects,
the action on F.obj X is continuous for all X : C and the only trivially acting element of G
is the identity.
- continuous_smul (X : C) : ContinuousSMul G ↑(F.obj X)
Instances
Aut F is a fundamental group for F.
If G is the fundamental group for F, it is isomorphic to Aut F as groups and
this isomorphism is also a homeomorphism (see toAutMulEquiv_isHomeomorph).
Equations
Instances For
If G is a fundamental group for F, it is canonically homeomorphic to Aut F.