Module

FiniteLocallyConstantDetection.lean

Nyll.EtaleFundamentalGroups.Cohomology.FiniteLocallyConstantDetection

2 declarations indexed from sourceView source ↗

Module documentation

Detecting finite local-system isomorphisms at a geometric point

On a connected scheme, bijectivity at one geometric stalk detects an isomorphism of finite locally constant sheaves. This is deduced from the actual monodromy equivalence and its comparison with the geometric stalk. The abelian version forgets the group structure only to detect the inverse.

Imports5

Nyll.EtaleCohomology.Constructible.Monodromy
Mathlib.CategoryTheory.Action.Basic
Mathlib.CategoryTheory.NatIso
Mathlib.CategoryTheory.Types.Basic
Mathlib.Algebra.Category.Grp.FilteredColimits

Imported by4

theorem

isIso_of_bijective_finiteLocallyConstant_stalk

L36 ↗

EtaleFundamentalGroups.Cohomology.isIso_of_bijective_finiteLocallyConstant_stalk

Documentation

One geometric stalk detects isomorphisms of finite locally constant set sheaves on a connected scheme.

Source context 6 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory 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 isIso_of_bijective_finiteLocallyConstant_stalk
    {F G : EtaleFiniteLocallyConstantSetSheaf X} (f : F ⟶ G)
    (hf : Function.Bijective ((Scheme.pointSmallEtale ξ).sheafFiber.map f.hom)) :
    IsIso f

theorem

isIso_of_bijective_finiteLocallyConstant_abelianStalk

L56 ↗

EtaleFundamentalGroups.Cohomology.isIso_of_bijective_finiteLocallyConstant_abelianStalk