Module

FiberIso.lean

Nyll.EtaleFundamentalGroups.GaloisCategories.FiberIso

3 declarations indexed from sourceView source ↗

Module documentation

Isomorphic finite fiber functors

A natural isomorphism of finite-set-valued functors induces an isomorphism of their topological automorphism groups. For fiber functors, the associated finite continuous-action functors agree after restriction along this isomorphism. Changing the natural isomorphism changes the group isomorphism by inner conjugation.

Imports1

Nyll.EtaleFundamentalGroups.GaloisCategories.Functoriality

Imported by10

def

continuousConjAut

L34 ↗

CategoryTheory.PreGaloisCategory.continuousConjAut

Documentation

A natural isomorphism induces a topological isomorphism of automorphism groups.

Source context 6 commands

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

@[expose] public section
noncomputable section
universe u v w
open scoped FintypeCatDiscrete
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u} [Category.{v} C] {F G : C ⥤ FintypeCat.{w}}

Lean source · full declaration

def continuousConjAut (t : F ≅ G) : Aut F ≃ₜ* Aut G where
  toMulEquiv := t.conjAut
  continuous_toFun := continuous_conjAut t
  continuous_invFun :=
    Continuous.continuous_symm_of_equiv_compact_to_t2
      (f := t.conjAut.toEquiv) (continuous_conjAut t)

theorem

continuousConjAut_eq_conj

L42 ↗

CategoryTheory.PreGaloisCategory.continuousConjAut_eq_conj

Documentation

Changing the natural isomorphism changes the group isomorphism by conjugation.

Source context 6 commands

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

@[expose] public section
noncomputable section
universe u v w
open scoped FintypeCatDiscrete
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u} [Category.{v} C] {F G : C ⥤ FintypeCat.{w}}

Lean source · statement

theorem continuousConjAut_eq_conj (t₁ t₂ : F ≅ G) (a : Aut F) :
    continuousConjAut t₂ a =
      MulAut.conj (G := Aut G) (t₁.symm ≪≫ t₂) (continuousConjAut t₁ a)

def

functorToContActionFiberIso

L59 ↗

CategoryTheory.PreGaloisCategory.functorToContActionFiberIso

Documentation

The finite-action equivalences of isomorphic fiber functors are compatible with restriction along the resulting topological group isomorphism.

Source context 7 commands

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

@[expose] public section
noncomputable section
universe u v w
open scoped FintypeCatDiscrete
namespace CategoryTheory.PreGaloisCategory
variable {C : Type u} [Category.{v} C] {F G : C ⥤ FintypeCat.{w}}
variable [GaloisCategory C] [FiberFunctor F] [FiberFunctor G]

Lean source · statement

def functorToContActionFiberIso (t : F ≅ G) :
    functorToContAction F ≅ functorToContAction G ⋙
      (ContAction.resEquiv FintypeCat (continuousConjAut t)).functor

Module documentation

Isomorphic finite fiber functors

Declarations

continuousConjAut

continuousConjAut_eq_conj

functorToContActionFiberIso