Module

PointedIntermediateObject.lean

Nyll.EtaleFundamentalGroups.GaloisCovers.PointedIntermediateObject

1 declaration indexed from sourceView source ↗

Module documentation

Pointed intermediate covers and their actual deck transformations

An open subgroup containing the stabilizer of a connected cover is realized by an intermediate connected object and an actual morphism. An original deck transformation lies over this intermediate object exactly when its fiber value is represented by an element of the chosen open subgroup. This is the geometric comparison needed when choosing a cyclic quotient.

Imports2

Imported by2

theorem

exists_pointedIntermediateObject

L30 ↗

CategoryTheory.PreGaloisCategory.exists_pointedIntermediateObject

Documentation

Construct an intermediate connected object, its pointed morphism, and the exact criterion for an original deck transformation to descend over it.

Source context 4 commands

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

noncomputable section
universe u v w
open CategoryTheory
namespace CategoryTheory.PreGaloisCategory

Lean source · statement

theorem exists_pointedIntermediateObject
    {C : Type u} [Category.{v} C] [GaloisCategory C]
    (F : C ⥤ FintypeCat.{w}) [FiberFunctor F]
    (A : C) [IsConnected A] (x : F.obj A)
    (U : OpenSubgroup (Aut F))
    (hU : MulAction.stabilizer (Aut F) x ≤ U.toSubgroup) :
    ∃ (B : C) (_ : IsConnected B) (y : F.obj B) (f : A ⟶ B),
      F.map f x = y ∧
      MulAction.stabilizer (Aut F) y = U.toSubgroup ∧
      ∀ (σ : Aut A) (g : Aut F),
        F.map σ.hom x = g • x →
          (σ.hom ≫ f = f ↔ g ∈ U)

Module documentation

Pointed intermediate covers and their actual deck transformations

Declarations

exists_pointedIntermediateObject