Module

Functoriality.lean

Nyll.EtaleFundamentalGroups.GaloisCategories.Functoriality

8 declarations indexed from sourceView source ↗

Module documentation

Functoriality of automorphism groups of finite fiber functors

Precomposition of a finite-set-valued functor induces a continuous map on its automorphism groups. Conjugating by a natural isomorphism is continuous as well, so the two operations combine into a canonical continuous monoid homomorphism.

Imports3

Mathlib.Algebra.Group.End
Mathlib.CategoryTheory.Conj
Mathlib.CategoryTheory.Galois.Equivalence

Imported by14

lemma

continuous_mapAut_whiskeringLeft

L36 ↗

CategoryTheory.PreGaloisCategory.continuous_mapAut_whiskeringLeft

Documentation

Precomposition induces a continuous map on automorphism groups.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

@[expose] public section
universe u₁ u₂ v₁ v₂ w
open scoped FintypeCatDiscrete
namespace CategoryTheory.PreGaloisCategory
open _root_.CategoryTheory.Functor
variable {C : Type u₁} [Category.{u₂} C]
variable {C' : Type v₁} [Category.{v₂} C']

Lean source · statement

lemma continuous_mapAut_whiskeringLeft
    (H : C ⥤ C') (F' : C' ⥤ FintypeCat.{w}) :
    Continuous (((whiskeringLeft C C' FintypeCat.{w}).obj H).mapAut F')

lemma

continuous_conjAut

L48 ↗

CategoryTheory.PreGaloisCategory.continuous_conjAut

Documentation

Conjugation by a natural isomorphism is continuous on automorphism groups.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

@[expose] public section
universe u₁ u₂ v₁ v₂ w
open scoped FintypeCatDiscrete
namespace CategoryTheory.PreGaloisCategory
open _root_.CategoryTheory.Functor
variable {C : Type u₁} [Category.{u₂} C]
variable {C' : Type v₁} [Category.{v₂} C']

Lean source · statement

lemma continuous_conjAut
    {F G : C ⥤ FintypeCat.{w}} (t : F ≅ G) :
    Continuous t.conjAut

def

autHomOfCompIso

L68 ↗

CategoryTheory.PreGaloisCategory.autHomOfCompIso

Documentation

The continuous homomorphism on automorphism groups induced by precomposition, then transported along a natural isomorphism.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

@[expose] public section
universe u₁ u₂ v₁ v₂ w
open scoped FintypeCatDiscrete
namespace CategoryTheory.PreGaloisCategory
open _root_.CategoryTheory.Functor
variable {C : Type u₁} [Category.{u₂} C]
variable {C' : Type v₁} [Category.{v₂} C']

Lean source · full declaration

def autHomOfCompIso
    (H : C ⥤ C') {F : C ⥤ FintypeCat.{w}}
    {F' : C' ⥤ FintypeCat.{w}} (t : H ⋙ F' ≅ F) :
    Aut F' →ₜ* Aut F where
  toMonoidHom :=
    t.conjAut.toMonoidHom.comp
      (((whiskeringLeft C C' FintypeCat.{w}).obj H).mapAut F')
  continuous_toFun :=
    (continuous_conjAut t).comp (continuous_mapAut_whiskeringLeft H F')

def

transportedPointOfCompIso

L80 ↗

CategoryTheory.PreGaloisCategory.transportedPointOfCompIso

Documentation

Transport a point backwards through the comparison between a composite fiber functor and the original fiber functor.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

@[expose] public section
universe u₁ u₂ v₁ v₂ w
open scoped FintypeCatDiscrete
namespace CategoryTheory.PreGaloisCategory
open _root_.CategoryTheory.Functor
variable {C : Type u₁} [Category.{u₂} C]
variable {C' : Type v₁} [Category.{v₂} C']

Lean source · statement

def transportedPointOfCompIso
    (H : C ⥤ C') {F : C ⥤ FintypeCat.{w}}
    {F' : C' ⥤ FintypeCat.{w}} (t : H ⋙ F' ≅ F)
    (X : C) (x : F.obj X) : F'.obj (H.obj X)

lemma

autHomOfCompIso_apply

L87 ↗

CategoryTheory.PreGaloisCategory.autHomOfCompIso_apply

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

@[expose] public section
universe u₁ u₂ v₁ v₂ w
open scoped FintypeCatDiscrete
namespace CategoryTheory.PreGaloisCategory
open _root_.CategoryTheory.Functor
variable {C : Type u₁} [Category.{u₂} C]
variable {C' : Type v₁} [Category.{v₂} C']

Lean source · statement

lemma autHomOfCompIso_apply
    (H : C ⥤ C') {F : C ⥤ FintypeCat.{w}}
    {F' : C' ⥤ FintypeCat.{w}} (t : H ⋙ F' ≅ F) (a : Aut F') :
    autHomOfCompIso H t a =
      t.conjAut (((whiskeringLeft C C' FintypeCat.{w}).obj H).mapAut F' a)

theorem

stabilizer_transportedPointOfCompIso

L96 ↗

CategoryTheory.PreGaloisCategory.stabilizer_transportedPointOfCompIso

Documentation

The stabilizer of a transported point is the inverse image of its original stabilizer under the homomorphism induced on automorphism groups.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

@[expose] public section
universe u₁ u₂ v₁ v₂ w
open scoped FintypeCatDiscrete
namespace CategoryTheory.PreGaloisCategory
open _root_.CategoryTheory.Functor
variable {C : Type u₁} [Category.{u₂} C]
variable {C' : Type v₁} [Category.{v₂} C']

Lean source · statement

theorem stabilizer_transportedPointOfCompIso
    (H : C ⥤ C') {F : C ⥤ FintypeCat.{w}}
    {F' : C' ⥤ FintypeCat.{w}} (t : H ⋙ F' ≅ F)
    (X : C) (x : F.obj X) :
    MulAction.stabilizer (Aut F') (transportedPointOfCompIso H t X x) =
      (MulAction.stabilizer (Aut F) x).comap
        (autHomOfCompIso H t).toMonoidHom

theorem

autHomOfCompIso_eq_conj

L126 ↗

CategoryTheory.PreGaloisCategory.autHomOfCompIso_eq_conj

Documentation

Changing the comparison isomorphism changes the induced homomorphism by conjugation with the explicit automorphism t₁.symm ≪≫ t₂.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

@[expose] public section
universe u₁ u₂ v₁ v₂ w
open scoped FintypeCatDiscrete
namespace CategoryTheory.PreGaloisCategory
open _root_.CategoryTheory.Functor
variable {C : Type u₁} [Category.{u₂} C]
variable {C' : Type v₁} [Category.{v₂} C']

Lean source · statement

theorem autHomOfCompIso_eq_conj
    (H : C ⥤ C') {F : C ⥤ FintypeCat.{w}}
    {F' : C' ⥤ FintypeCat.{w}} (t₁ t₂ : H ⋙ F' ≅ F) (σ : Aut F') :
    autHomOfCompIso H t₂ σ =
      MulAut.conj (G := Aut F) (t₁.symm ≪≫ t₂ : Aut F)
        (autHomOfCompIso H t₁ σ)

def

functorToContActionCompIso

L158 ↗

CategoryTheory.PreGaloisCategory.functorToContActionCompIso

Documentation

The canonical comparison square between the finite continuous-action functors associated to two fiber functors.

Source context 7 commands

Surrounding namespaces, section variables, and local commands at this declaration.

@[expose] public section
universe u₁ u₂ v₁ v₂ w
open scoped FintypeCatDiscrete
namespace CategoryTheory.PreGaloisCategory
open _root_.CategoryTheory.Functor
variable {C : Type u₁} [Category.{u₂} C]
variable {C' : Type v₁} [Category.{v₂} C']

Lean source · statement

def functorToContActionCompIso
    [GaloisCategory C] [GaloisCategory C']
    {F : C ⥤ FintypeCat.{w}} [FiberFunctor F]
    {F' : C' ⥤ FintypeCat.{w}} [FiberFunctor F']
    (H : C ⥤ C') (t : H ⋙ F' ≅ F) :
    H ⋙ functorToContAction F' ≅
      functorToContAction F ⋙
        ContAction.res FintypeCat (autHomOfCompIso H t)

Module documentation

Functoriality of automorphism groups of finite fiber functors

Declarations