Module

MonodromySections.lean

Nyll.EtaleFundamentalGroups.Cohomology.MonodromySections

4 declarations indexed from sourceView source ↗

Module documentation

Global sections and fixed geometric monodromy points

For a finite locally constant étale sheaf on a connected scheme, existence of a global section is equivalent to existence of a fixed point in its actual finite monodromy representation. The reverse implication uses fullness of the proved monodromy equivalence, not a descent hypothesis.

Imports7

Nyll.EtaleCohomology.Constructible.Monodromy
Nyll.EtaleCohomology.Constructible.FiniteLocallyConstantSet
Mathlib.CategoryTheory.Action.Concrete
Mathlib.CategoryTheory.Limits.Connected
Mathlib.CategoryTheory.Limits.Types.Products
Mathlib.CategoryTheory.Sites.Sheafification
Mathlib.Topology.Category.FinTopCat

Imported by2

abbrev

unitSheaf

L36 ↗

EtaleFundamentalGroups.Cohomology.unitSheaf

Source context 6 commands

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

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

Lean source · statement

abbrev unitSheaf : Sheaf X.smallEtaleTopology (Type u)

abbrev

unitLocallyConstant

L39 ↗

EtaleFundamentalGroups.Cohomology.unitLocallyConstant

Source context 6 commands

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

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

Lean source · statement

abbrev unitLocallyConstant : EtaleFiniteLocallyConstantSetSheaf X

def

unitMonodromyIso

L43 ↗

EtaleFundamentalGroups.Cohomology.unitMonodromyIso

Source context 6 commands

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

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

Lean source · statement

def unitMonodromyIso :
    ↥(((finiteLocallyConstantSetMonodromy ξ).functor.obj unitLocallyConstant).obj.V) ≅
      PUnit.{u + 1}

theorem

nonempty_globalSection_iff_monodromy_fixed

L52 ↗

EtaleFundamentalGroups.Cohomology.nonempty_globalSection_iff_monodromy_fixed

Documentation

A finite local system has a global section exactly when its geometric monodromy has a fixed point. Only connectedness and a geometric point are used.

Source context 6 commands

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

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

Lean source · statement

theorem nonempty_globalSection_iff_monodromy_fixed
    (F : EtaleFiniteLocallyConstantSetSheaf X) :
    Nonempty ((Functor.const X.Etaleᵒᵖ).obj PUnit ⟶ F.obj.obj) ↔
      ∃ q : ((finiteLocallyConstantSetMonodromy ξ).functor.obj F).obj.V,
        ∀ g : Aut (FiniteEtale.fiber ξ), g • q = q

Module documentation

Global sections and fixed geometric monodromy points

Declarations

unitSheaf

unitLocallyConstant

unitMonodromyIso

nonempty_globalSection_iff_monodromy_fixed