Theorems · Theorem · category theory

CategoryTheory.PreGaloisCategory.toAut_surjective_isGalois_finite_family

∀ {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] [CategoryTheory.PreGaloisCategory.IsNaturalSMul F G]
  [inst_4 : CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F]
  (t : CategoryTheory.Aut F) {ι : Type u_2} [Finite ι] (X : ι → C)
  [∀ (i : ι), CategoryTheory.PreGaloisCategory.IsGalois (X i)],
  (∀ (X : C) [CategoryTheory.PreGaloisCategory.IsGalois X], MulAction.IsPretransitive G (F.obj X).obj) →
    ∃ g, ∀ (i : ι) (x : (F.obj (X i)).obj), g • x = (CategoryTheory.ConcreteCategory.hom (t.hom.app (X i))) x

Defined in

Mathlib.CategoryTheory.Galois.IsFundamentalgroup

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryGroupMulActionCategoryTheory.PreGaloisCategory.IsNaturalSMulCategoryTheory.GaloisCategoryCategoryTheory.PreGaloisCategory.FiberFunctorFiniteCategoryTheory.PreGaloisCategory.IsGalois