Module

PointedDeckTransport.lean

Nyll.EtaleFundamentalGroups.GaloisCategories.PointedDeckTransport

4 declarations indexed from sourceView source ↗

Module documentation

Deck transformations and conjugation on pointed cover fibers

An automorphism of the covering object acts by inverse postcomposition on its over-category. Choosing an ambient monodromy element with the same effect on the distinguished point compares its induced fundamental-group map with conjugation. The comparison uses the actual over-category functor.

Imports1

Nyll.EtaleFundamentalGroups.GaloisCategories.PointedOverTransport

Imported by2

theorem

deckFiberPoint

L33 ↗

CategoryTheory.PreGaloisCategory.deckFiberPoint

Source context 10 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) (σ : Aut X) (g : Aut F)
variable (h : F.map σ.hom x = g • x)
omit [PreGaloisCategory C] [FiberFunctor F] in
include h in

Lean source · statement

theorem deckFiberPoint (U : Over X)
    (z : (fiberOver F x).obj ((Over.map σ.inv).obj U)) :
    F.map U.hom z.1 = g • x

def

pointedDeckFiberEquiv

L48 ↗

CategoryTheory.PreGaloisCategory.pointedDeckFiberEquiv

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) (σ : Aut X) (g : Aut F)
variable (h : F.map σ.hom x = g • x)

Lean source · full declaration

def pointedDeckFiberEquiv (U : Over X) :
    (fiberOver F x).obj ((Over.map σ.inv).obj U) ≃ (fiberOver F x).obj U where
  toFun z := ⟨g⁻¹ • z.1, by
    exact ((mulAction_naturality F g⁻¹ U.hom z.1).symm).trans
      ((congrArg (g⁻¹ • ·) (deckFiberPoint F x σ g h U z)).trans
        (inv_smul_smul g x))⟩
  invFun z := ⟨g • z.1, by
    change F.map (U.hom ≫ σ.inv) (g • z.1) = x
    rw [F.map_comp, FintypeCat.comp_apply,
      ← mulAction_naturality F g U.hom z.1, z.2, ← h]
    exact FintypeCat.hom_inv_id_apply (F.mapIso σ) x⟩
  left_inv z := by
    apply Subtype.ext
    exact smul_inv_smul g z.1
  right_inv z := by
    apply Subtype.ext
    exact inv_smul_smul g z.1

def

pointedDeckFiberIso

L68 ↗

CategoryTheory.PreGaloisCategory.pointedDeckFiberIso

Documentation

The geometric deck functor on the over-category, pointed using ambient monodromy with the same endpoint as the deck transformation.

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) (σ : Aut X) (g : Aut F)
variable (h : F.map σ.hom x = g • x)

Lean source · statement

def pointedDeckFiberIso :
    Over.map σ.inv ⋙ fiberOver F x ≅ fiberOver F x

theorem

extendFiberOverAut_pointedDeck

L80 ↗

CategoryTheory.PreGaloisCategory.extendFiberOverAut_pointedDeck

Documentation

The ambient image of the actual deck-induced map on pointed fiber automorphisms is conjugation by the chosen ambient monodromy element.

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) (σ : Aut X) (g : Aut F)
variable (h : F.map σ.hom x = g • x)

Lean source · statement

theorem extendFiberOverAut_pointedDeck
    (a : Aut (fiberOver F x)) :
    extendFiberOverAut F x
        (autHomOfCompIso (Over.map σ.inv) (pointedDeckFiberIso F x σ g h) a) =
      g⁻¹ * extendFiberOverAut F x a * g

Module documentation

Deck transformations and conjugation on pointed cover fibers

Declarations

deckFiberPoint

pointedDeckFiberEquiv

pointedDeckFiberIso

extendFiberOverAut_pointedDeck