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 X
is compatible with morphisms inC
transitive_of_isGalois
:G
acts transitively onF.obj X
for all Galois objectsX : C
continuous_smul
: the action ofG
onF.obj X
is continuous ifF.obj X
is equipped with the discrete topology for allX : C
.non_trivial': if
g : Gacts trivial on all
F.obj X, then
g = 1`.
Given this data, we define toAut F G : G →* Aut F
in the natural way.
Main results #
toAut_bijective
:toAut F G
is a group isomorphism givenIsFundamentalGroup F G
.toAut_isHomeomorph
:toAut F G
is a homeomorphism givenIsFundamentalGroup F G
.
TODO #
- Develop further equivalent conditions, in particular, relate the condition
non_trivial
withG
being 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.
- transitive_of_isGalois : ∀ (X : C) [inst : CategoryTheory.PreGaloisCategory.IsGalois X], MulAction.IsPretransitive G ↑(F.obj X)
- continuous_smul : ∀ (X : C), ContinuousSMul G ↑(F.obj X)
Instances
Aut F
is a fundamental group for F
.
Equations
- ⋯ = ⋯
Equations
- ⋯ = ⋯
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
.