Module

Monodromy.lean

Nyll.EtaleCohomology.Constructible.Monodromy

2 declarations indexed from sourceView source ↗

Module documentation

Monodromy of finite locally constant étale sheaves

For a connected scheme with a geometric point, finite locally constant set sheaves are equivalent to finite sets with a continuous action of the étale fundamental group. The group is the existing EFG automorphism group of the geometric fiber functor. The underlying finite set of this action is naturally isomorphic to the actual geometric stalk, defined by the site's filtered colimit.

The Galois-category equivalence is supplied by mathlib, and the represented-sheaf fiber comparison by finiteEtaleSheafFiberIso. The comparison below also uses the counit of the constructed finite étale representability equivalence, so it applies to every finite locally constant sheaf, not only a represented input.

Imports12

Nyll.EtaleCohomology.Constructible.FiniteEtaleSheaf
Nyll.EtaleCohomology.Constructible.FiniteLocallyConstantEquivalence
Nyll.EtaleCohomology.Constructible.FiniteLocallyConstantSet
Nyll.EtaleFundamentalGroups.Pi1.FiniteEtale.GaloisCategory
Mathlib.AlgebraicGeometry.Sites.EtalePoint
Mathlib.CategoryTheory.Action.Continuous
Mathlib.CategoryTheory.Equivalence
Mathlib.CategoryTheory.Galois.Equivalence
Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
Mathlib.CategoryTheory.Sites.Point.Basic
Mathlib.CategoryTheory.Whiskering
Mathlib.Topology.Category.FinTopCat

Imported by11

def

finiteLocallyConstantSetMonodromy

L49 ↗

EtaleCohomology.finiteLocallyConstantSetMonodromy

Documentation

Finite locally constant sheaves are finite continuous representations of the étale fundamental group on sets.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.PreGaloisCategory
open scoped FintypeCatDiscrete
universe u
namespace EtaleCohomology
variable {X : Scheme.{u}} [ConnectedSpace X]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (ξ : Spec (.of Ω) ⟶ X)

Lean source · statement

def finiteLocallyConstantSetMonodromy :
    EtaleFiniteLocallyConstantSetSheaf X ≌ ContAction FintypeCat.{u} (Aut (FiniteEtale.fiber ξ))

def

finiteLocallyConstantSetMonodromyStalkIso

L56 ↗

EtaleCohomology.finiteLocallyConstantSetMonodromyStalkIso