Theorems · Theorem · category theory

CategoryTheory.PreGaloisCategory.nhds_one_has_basis_stabilizers

∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F],
  (nhds 1).HasBasis (fun x => True) fun X => ↑(MulAction.stabilizer (CategoryTheory.Aut F) X.pt)

The stabilizers of points in the fibers of Galois objects form a neighbourhood basis of the identity in Aut F.

Defined in

Mathlib.CategoryTheory.Galois.Topology

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.GaloisCategoryCategoryTheory.PreGaloisCategory.FiberFunctor