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
    theorem CategoryTheory.PreGaloisCategory.IsNaturalSMul.naturality {C : Type u₁} :
    ∀ {inst : CategoryTheory.Category.{u₂, u₁} C} {F : CategoryTheory.Functor C FintypeCat} {G : Type u_1} {inst_1 : Group G} {inst_2 : (X : C) → MulAction G (F.obj X)} [self : CategoryTheory.PreGaloisCategory.IsNaturalSMul F G] (g : G) {X Y : C} (f : X Y) (x : (F.obj X)), F.map f (g x) = g F.map f x

    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 trivally acting element of G is the identity.

      Instances
        theorem CategoryTheory.PreGaloisCategory.IsFundamentalGroup.continuous_smul {C : Type u₁} :
        ∀ {inst : CategoryTheory.Category.{u₂, u₁} C} {F : CategoryTheory.Functor C FintypeCat} {inst_1 : CategoryTheory.GaloisCategory C} {G : Type u_1} {inst_2 : Group G} {inst_3 : (X : C) → MulAction G (F.obj X)} {inst_4 : TopologicalSpace G} {inst_5 : TopologicalGroup G} {inst_6 : CompactSpace G} [self : CategoryTheory.PreGaloisCategory.IsFundamentalGroup F G] (X : C), ContinuousSMul G (F.obj X)
        theorem CategoryTheory.PreGaloisCategory.IsFundamentalGroup.non_trivial' {C : Type u₁} :
        ∀ {inst : CategoryTheory.Category.{u₂, u₁} C} {F : CategoryTheory.Functor C FintypeCat} {inst_1 : CategoryTheory.GaloisCategory C} {G : Type u_1} {inst_2 : Group G} {inst_3 : (X : C) → MulAction G (F.obj X)} {inst_4 : TopologicalSpace G} {inst_5 : TopologicalGroup G} {inst_6 : CompactSpace G} [self : CategoryTheory.PreGaloisCategory.IsFundamentalGroup F G] (g : G), (∀ (X : C) (x : (F.obj X)), g x = x)g = 1