Documentation

Mathlib.CategoryTheory.Galois.IsFundamentalgroup

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

Given this data, we define toAut F G : G →* Aut F in the natural way.

Main results #

TODO #

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.

  • naturality (g : G) {X Y : C} (f : X Y) (x : (F.obj X)) : F.map f (g x) = g F.map f x
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
    Instances For
      @[simp]

      toAut is injective, if only the identity acts trivially on every fiber.

      theorem CategoryTheory.PreGaloisCategory.toAut_surjective_isGalois_finite_family {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) (G : Type u_1) [Group G] [(X : C) → MulAction G (F.obj X)] [CategoryTheory.PreGaloisCategory.IsNaturalSMul F G] [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] (t : CategoryTheory.Aut F) {ι : Type u_2} [Finite ι] (X : ιC) [∀ (i : ι), CategoryTheory.PreGaloisCategory.IsGalois (X i)] (h : ∀ (X : C) [inst : CategoryTheory.PreGaloisCategory.IsGalois X], MulAction.IsPretransitive G (F.obj X)) :
      ∃ (g : G), ∀ (i : ι) (x : (F.obj (X i))), g x = t.hom.app (X i) x

      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.

      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.

      Instances