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: the G-action on F.obj X is compatible with morphisms in C
• transitive_of_isGalois: G acts transitively on F.obj X for all Galois objects X : C
• continuous_smul: the action of G on F.obj X is continuous if F.obj X is equipped with the discrete topology for all X : C.
• non_trivial': if g : Gacts trivial on allF.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 given IsFundamentalGroup F G.
• toAut_isHomeomorph: toAut F G is a homeomorphism given IsFundamentalGroup F G.

TODO

• Develop further equivalent conditions, in particular, relate the condition non_trivial with G being a T2Space.

class CategoryTheory.PreGaloisCategory.IsNaturalSMul {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)] : Prop

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

def CategoryTheory.PreGaloisCategory.toAut {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] : G →* CategoryTheory.Aut F

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' := ⋯ }

@[simp]

theorem CategoryTheory.PreGaloisCategory.toAut_hom_app_apply {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] (g : G) {X : C} (x : ↑(F.obj X)) : ((CategoryTheory.PreGaloisCategory.toAut F G) g).hom.app X x = g • x

theorem CategoryTheory.PreGaloisCategory.toAut_injective_of_non_trivial {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] (h : ∀ (g : G), (∀ (X : C) (x : ↑(F.obj X)), g • x = x) → g = 1) : Function.Injective ⇑(CategoryTheory.PreGaloisCategory.toAut F G)

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

theorem CategoryTheory.PreGaloisCategory.toAut_continuous {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] [TopologicalSpace G] [TopologicalGroup G] [∀ (X : C), ContinuousSMul G ↑(F.obj X)] : Continuous ⇑(CategoryTheory.PreGaloisCategory.toAut F G)

theorem CategoryTheory.PreGaloisCategory.action_ext_of_isGalois {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 : F ⟶ F} {X : C} [CategoryTheory.PreGaloisCategory.IsGalois X] {g : G} (x : ↑(F.obj X)) (hg : g • x = t.app X x) (y : ↑(F.obj X)) : g • y = t.app X y

theorem CategoryTheory.PreGaloisCategory.toAut_surjective_isGalois {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) (X : C) [CategoryTheory.PreGaloisCategory.IsGalois X] [MulAction.IsPretransitive G ↑(F.obj X)] : ∃ (g : G), ∀ (x : ↑(F.obj X)), g • x = t.hom.app X x

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

theorem CategoryTheory.PreGaloisCategory.toAut_surjective_of_isPretransitive {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] [TopologicalSpace G] [TopologicalGroup G] [CompactSpace G] [∀ (X : C), ContinuousSMul G ↑(F.obj X)] (h : ∀ (X : C) [inst : CategoryTheory.PreGaloisCategory.IsGalois X], MulAction.IsPretransitive G ↑(F.obj X)) : Function.Surjective ⇑(CategoryTheory.PreGaloisCategory.toAut F G)

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.

theorem CategoryTheory.PreGaloisCategory.isPretransitive_of_surjective {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] (h : Function.Surjective ⇑(CategoryTheory.PreGaloisCategory.toAut F G)) (X : C) [CategoryTheory.PreGaloisCategory.IsConnected X] : MulAction.IsPretransitive G ↑(F.obj X)

If toAut F G is surjective, then G acts transitively on the fibers of connected objects. For a converse see toAut_surjective.

class CategoryTheory.PreGaloisCategory.IsFundamentalGroup {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] (G : Type u_1) [Group G] [(X : C) → MulAction G ↑(F.obj X)] [TopologicalSpace G] [TopologicalGroup G] [CompactSpace G] extends CategoryTheory.PreGaloisCategory.IsNaturalSMul F G : Prop

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.

• naturality : ∀ (g : G) {X Y : C} (f : X ⟶ Y) (x : ↑(F.obj X)), F.map f (g • x) = g • F.map f x
• 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)
• non_trivial' : ∀ (g : G), (∀ (X : C) (x : ↑(F.obj X)), g • x = x) → g = 1

theorem CategoryTheory.PreGaloisCategory.IsFundamentalGroup.non_trivial {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] {G : Type u_1} [Group G] [(X : C) → MulAction G ↑(F.obj X)] [TopologicalSpace G] [TopologicalGroup G] [CompactSpace G] [CategoryTheory.PreGaloisCategory.IsFundamentalGroup F G] (g : G) (h : ∀ (X : C) (x : ↑(F.obj X)), g • x = x) : g = 1

instance CategoryTheory.PreGaloisCategory.instIsFundamentalGroupAutFunctorFintypeCat {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] : CategoryTheory.PreGaloisCategory.IsFundamentalGroup F (CategoryTheory.Aut F)

Aut F is a fundamental group for F.

Equations

• ⋯ = ⋯

theorem CategoryTheory.PreGaloisCategory.toAut_bijective {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] (G : Type u_1) [Group G] [(X : C) → MulAction G ↑(F.obj X)] [CategoryTheory.PreGaloisCategory.FiberFunctor F] [TopologicalSpace G] [TopologicalGroup G] [CompactSpace G] [CategoryTheory.PreGaloisCategory.IsFundamentalGroup F G] : Function.Bijective ⇑(CategoryTheory.PreGaloisCategory.toAut F G)

instance CategoryTheory.PreGaloisCategory.instIsPretransitiveαFintypeObjFintypeCatOfIsConnected {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] (G : Type u_1) [Group G] [(X : C) → MulAction G ↑(F.obj X)] [CategoryTheory.PreGaloisCategory.FiberFunctor F] [TopologicalSpace G] [TopologicalGroup G] [CompactSpace G] [CategoryTheory.PreGaloisCategory.IsFundamentalGroup F G] (X : C) [CategoryTheory.PreGaloisCategory.IsConnected X] : MulAction.IsPretransitive G ↑(F.obj X)

Equations

• ⋯ = ⋯

noncomputable def CategoryTheory.PreGaloisCategory.toAutMulEquiv {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] (G : Type u_1) [Group G] [(X : C) → MulAction G ↑(F.obj X)] [CategoryTheory.PreGaloisCategory.FiberFunctor F] [TopologicalSpace G] [TopologicalGroup G] [CompactSpace G] [CategoryTheory.PreGaloisCategory.IsFundamentalGroup F G] : G ≃* CategoryTheory.Aut 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

• CategoryTheory.PreGaloisCategory.toAutMulEquiv F G = MulEquiv.ofBijective (CategoryTheory.PreGaloisCategory.toAut F G) ⋯

theorem CategoryTheory.PreGaloisCategory.toAut_isHomeomorph {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] (G : Type u_1) [Group G] [(X : C) → MulAction G ↑(F.obj X)] [CategoryTheory.PreGaloisCategory.FiberFunctor F] [TopologicalSpace G] [TopologicalGroup G] [CompactSpace G] [CategoryTheory.PreGaloisCategory.IsFundamentalGroup F G] : IsHomeomorph ⇑(CategoryTheory.PreGaloisCategory.toAut F G)

theorem CategoryTheory.PreGaloisCategory.toAutMulEquiv_isHomeomorph {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] (G : Type u_1) [Group G] [(X : C) → MulAction G ↑(F.obj X)] [CategoryTheory.PreGaloisCategory.FiberFunctor F] [TopologicalSpace G] [TopologicalGroup G] [CompactSpace G] [CategoryTheory.PreGaloisCategory.IsFundamentalGroup F G] : IsHomeomorph ⇑(CategoryTheory.PreGaloisCategory.toAutMulEquiv F G)

noncomputable def CategoryTheory.PreGaloisCategory.toAutHomeo {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] (G : Type u_1) [Group G] [(X : C) → MulAction G ↑(F.obj X)] [CategoryTheory.PreGaloisCategory.FiberFunctor F] [TopologicalSpace G] [TopologicalGroup G] [CompactSpace G] [CategoryTheory.PreGaloisCategory.IsFundamentalGroup F G] : G ≃ₜ CategoryTheory.Aut F

If G is a fundamental group for F, it is canonically homeomorphic to Aut F.

Equations

• CategoryTheory.PreGaloisCategory.toAutHomeo F G = IsHomeomorph.homeomorph ⇑(CategoryTheory.PreGaloisCategory.toAut F G) ⋯

@[simp]

theorem CategoryTheory.PreGaloisCategory.toAutMulEquiv_apply {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] {G : Type u_1} [Group G] [(X : C) → MulAction G ↑(F.obj X)] [CategoryTheory.PreGaloisCategory.FiberFunctor F] [TopologicalSpace G] [TopologicalGroup G] [CompactSpace G] [CategoryTheory.PreGaloisCategory.IsFundamentalGroup F G] (g : G) : (CategoryTheory.PreGaloisCategory.toAutMulEquiv F G) g = (CategoryTheory.PreGaloisCategory.toAut F G) g

@[simp]

theorem CategoryTheory.PreGaloisCategory.toAutHomeo_apply {C : Type u₁} [CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) [CategoryTheory.GaloisCategory C] {G : Type u_1} [Group G] [(X : C) → MulAction G ↑(F.obj X)] [CategoryTheory.PreGaloisCategory.FiberFunctor F] [TopologicalSpace G] [TopologicalGroup G] [CompactSpace G] [CategoryTheory.PreGaloisCategory.IsFundamentalGroup F G] (g : G) : (CategoryTheory.PreGaloisCategory.toAutHomeo F G) g = (CategoryTheory.PreGaloisCategory.toAut F G) g