Module

PointedOverTransport.lean

Nyll.EtaleFundamentalGroups.GaloisCategories.PointedOverTransport

5 declarations indexed from sourceView source ↗

Module documentation

Monodromy transport on pointed covers

An actual automorphism of a finite fiber functor transports fibers over a point to fibers over its translate. Under the existing stabilizer comparison, this transport is conjugation by that same automorphism.

Imports2

Imported by2

def

fiberOverOrbitEquiv

L30 ↗

CategoryTheory.PreGaloisCategory.fiberOverOrbitEquiv

Source context 7 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]
variable (F : C ⥤ FintypeCat.{w}) [PreGaloisCategory C] [FiberFunctor F]
variable {X : C} (x : F.obj X) (g : Aut F)

Lean source · full declaration

def fiberOverOrbitEquiv (U : Over X) :
    (fiberOver F x).obj U ≃ (fiberOver F (g • x)).obj U where
  toFun z := ⟨g • z.1, by
    exact ((mulAction_naturality F g U.hom z.1).symm).trans
      (congrArg (g • ·) z.2)⟩
  invFun z := ⟨g⁻¹ • z.1, by
    exact ((mulAction_naturality F g⁻¹ U.hom z.1).symm).trans
      ((congrArg (g⁻¹ • ·) z.2).trans (inv_smul_smul g x))⟩
  left_inv z := by
    apply Subtype.ext
    exact inv_smul_smul g z.1
  right_inv z := by
    apply Subtype.ext
    exact smul_inv_smul g z.1

def

fiberOverOrbitIso

L46 ↗

CategoryTheory.PreGaloisCategory.fiberOverOrbitIso

Documentation

Transport in the actual fibers of objects over a cover.

Source context 7 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]
variable (F : C ⥤ FintypeCat.{w}) [PreGaloisCategory C] [FiberFunctor F]
variable {X : C} (x : F.obj X) (g : Aut F)

Lean source · statement

def fiberOverOrbitIso : fiberOver F x ≅ fiberOver F (g • x)

def

orbitStabilizerConjugate

L56 ↗

CategoryTheory.PreGaloisCategory.orbitStabilizerConjugate

Documentation

Conjugation sends the stabilizer of a point into the stabilizer of its translate.

Source context 7 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]
variable (F : C ⥤ FintypeCat.{w}) [PreGaloisCategory C] [FiberFunctor F]
variable {X : C} (x : F.obj X) (g : Aut F)

Lean source · statement

def orbitStabilizerConjugate (a : MulAction.stabilizer (Aut F) x) :
    MulAction.stabilizer (Aut F) (g • x)

theorem

fiberOverOrbitIso_conj_restrict

L64 ↗

CategoryTheory.PreGaloisCategory.fiberOverOrbitIso_conj_restrict

Documentation

Fiber transport acts on restricted automorphisms by actual conjugation.

Source context 8 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]
variable (F : C ⥤ FintypeCat.{w}) [PreGaloisCategory C] [FiberFunctor F]
variable {X : C} (x : F.obj X) (g : Aut F)
omit [PreGaloisCategory C] [FiberFunctor F] in

Lean source · statement

theorem fiberOverOrbitIso_conj_restrict
    (a : MulAction.stabilizer (Aut F) x) :
    continuousConjAut (fiberOverOrbitIso F x g)
        (restrictAutToFiberOver F x a) =
      restrictAutToFiberOver F (g • x) (orbitStabilizerConjugate F x g a)

theorem

autFiberOverEquivStabilizer_orbit

L77 ↗

CategoryTheory.PreGaloisCategory.autFiberOverEquivStabilizer_orbit

Documentation

The established stabilizer identification intertwines fiber transport and conjugation in the ambient automorphism group.

Source context 7 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]
variable (F : C ⥤ FintypeCat.{w}) [PreGaloisCategory C] [FiberFunctor F]
variable {X : C} (x : F.obj X) (g : Aut F)

Lean source · statement

theorem autFiberOverEquivStabilizer_orbit
    (a : Aut (fiberOver F x)) :
    autFiberOverEquivStabilizer F (g • x)
        (continuousConjAut (fiberOverOrbitIso F x g) a) =
      orbitStabilizerConjugate F x g
        (autFiberOverEquivStabilizer F x a)

Module documentation

Monodromy transport on pointed covers

Declarations

fiberOverOrbitEquiv

fiberOverOrbitIso

orbitStabilizerConjugate

fiberOverOrbitIso_conj_restrict

autFiberOverEquivStabilizer_orbit