ModuleFunctorFromHom.lean
Nyll.EtaleFundamentalGroups.GaloisCategories.FunctorFromHom
3 declarations indexed from sourceView source ↗ Module documentation
Functors induced by continuous homomorphisms of Galois groups
A continuous homomorphism between the automorphism groups of two fiber functors induces a functor between the corresponding Galois categories by restriction of finite continuous actions.
Declarations
CategoryTheory.PreGaloisCategory.functorOfContinuousHom
DocumentationThe functor between Galois categories induced contravariantly by a continuous homomorphism between the automorphism groups of their fiber functors.
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
universe u₁ u₂ v₁ v₂ w
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u₁} [Category.{u₂} C] [GaloisCategory C]
variable {C' : Type v₁} [Category.{v₂} C'] [GaloisCategory C']
variable (F : C ⥤ FintypeCat.{w}) [FiberFunctor F]
variable (F' : C' ⥤ FintypeCat.{w}) [FiberFunctor F']
CategoryTheory.PreGaloisCategory.functorOfContinuousHomPreservesFiniteLimits
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
universe u₁ u₂ v₁ v₂ w
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u₁} [Category.{u₂} C] [GaloisCategory C]
variable {C' : Type v₁} [Category.{v₂} C'] [GaloisCategory C']
variable (F : C ⥤ FintypeCat.{w}) [FiberFunctor F]
variable (F' : C' ⥤ FintypeCat.{w}) [FiberFunctor F']
CategoryTheory.PreGaloisCategory.functorOfContinuousHomPreservesFiniteColimits
Source context 10 commands
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
universe u₁ u₂ v₁ v₂ w
noncomputable section
open CategoryTheory Limits
open scoped FintypeCatDiscrete
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u₁} [Category.{u₂} C] [GaloisCategory C]
variable {C' : Type v₁} [Category.{v₂} C'] [GaloisCategory C']
variable (F : C ⥤ FintypeCat.{w}) [FiberFunctor F]
variable (F' : C' ⥤ FintypeCat.{w}) [FiberFunctor F']