ModuleFundamentalGroup.lean
Nyll.EtaleFundamentalGroups.Pi1.GaloisCategories.FundamentalGroup
2 declarations indexed from sourceView source ↗ Module documentation
Fundamental-group kernels in Galois categories
The kernel of the natural action on a fiber functor is the intersection of its point stabilizers.
Imports1
- Mathlib.CategoryTheory.Galois.IsFundamentalgroup
Imported by2
Declarations
CategoryTheory.Aut.one_hom
Source context 2 commands
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
open CategoryTheory
CategoryTheory.PreGaloisCategory.ker_toAut
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
open CategoryTheory
namespace CategoryTheory.PreGaloisCategory
variable {C : Type*} [Category C] (F : C ⥤ FintypeCat)
variable (G : Type*) [Group G] [∀ X, MulAction G (F.obj X)] [IsNaturalSMul F G]