Theorems · Theorem · category theory

CategoryTheory.PreGaloisCategory.toAut_surjective_of_isPretransitive

∀ {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).obj]
  [inst_3 : CategoryTheory.PreGaloisCategory.IsNaturalSMul F G] [inst_4 : CategoryTheory.GaloisCategory C]
  [CategoryTheory.PreGaloisCategory.FiberFunctor F] [inst_6 : TopologicalSpace G] [IsTopologicalGroup G]
  [CompactSpace G] [∀ (X : C), ContinuousSMul G (F.obj X).obj],
  (∀ (X : C) [CategoryTheory.PreGaloisCategory.IsGalois X], MulAction.IsPretransitive G (F.obj X).obj) →
    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.

Defined in

Mathlib.CategoryTheory.Galois.IsFundamentalgroup

Cited by

1 results in Mathlib

Foundations

Depth 102 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryGroupMulActionCategoryTheory.PreGaloisCategory.IsNaturalSMulCategoryTheory.GaloisCategoryCategoryTheory.PreGaloisCategory.FiberFunctorTopologicalSpaceIsTopologicalGroupCompactSpaceContinuousSMul