ModuleDeckSubgroupIntermediate.lean
Nyll.EtaleFundamentalGroups.GaloisCovers.DeckSubgroupIntermediate
2 declarations indexed from sourceView source ↗ Module documentation
Intermediate objects for subgroups of the actual deck group
The inverse image of a deck subgroup is open because it contains the point stabilizer. Its connected geometric realization gives a quotient morphism with exactly the prescribed subgroup of deck transformations.
Declarations
CategoryTheory.PreGaloisCategory.deckSubgroupOpenPreimage
DocumentationThe actual inverse image of a deck subgroup is open.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v w
open CategoryTheory
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u} [Category.{v} C] [GaloisCategory C]
(F : C ⥤ FintypeCat.{w}) [FiberFunctor F]
(A : C) [IsGalois A] (x : F.obj A)
CategoryTheory.PreGaloisCategory.exists_intermediateObject_of_deckSubgroup
DocumentationAn actual morphism realizing a prescribed subgroup of the deck group. In particular this constructs the intermediate object for a cyclic subgroup.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u v w
open CategoryTheory
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u} [Category.{v} C] [GaloisCategory C]
(F : C ⥤ FintypeCat.{w}) [FiberFunctor F]
(A : C) [IsGalois A] (x : F.obj A)