ModuleContinuousHomComparison.lean
Nyll.EtaleFundamentalGroups.GaloisCategories.ContinuousHomComparison
2 declarations indexed from sourceView source ↗ Module documentation
Recovering continuous homomorphisms from induced functors
The chosen inverse to the finite continuous-action equivalence supplies a canonical comparison isomorphism for the functor induced by a continuous homomorphism. The equivariance of the chosen counit shows that the resulting homomorphism on automorphism groups is the original one.
Declarations
CategoryTheory.PreGaloisCategory.comparisonIsoOfContinuousHom
DocumentationThe canonical comparison between the composite fiber functor of the functor induced by h and the original fiber functor.
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
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.autHomOfCompIso_comparisonIsoOfContinuousHom
DocumentationThe canonical comparison isomorphism recovers the continuous homomorphism from which the functor was constructed.
Source context 11 commands
Surrounding namespaces, section variables, and local commands at this declaration.
@[expose] public section
universe u₁ u₂ v₁ v₂ w
noncomputable section
open CategoryTheory
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']
omit [GaloisCategory C] [FiberFunctor F] in