NYLL
Module

FiniteLocallyConstantEpis.lean

Nyll.EtaleFundamentalGroups.Cohomology.FiniteLocallyConstantEpis
6 declarations indexed from sourceView source ↗

Module documentation

Surjectivity detected at one geometric stalk

For finite local systems on a connected scheme, a surjective stalk map at one geometric point gives an epimorphism of actual abelian sheaves. Faithful Galois fiber functors reflect epimorphisms and every geometric fiber functor preserves them. The conservative family of geometric points then detects the epimorphism in the ambient category of all abelian sheaves.

Imports6
Imported by2

Declarations

abbrev

localSystemStalk

L36 ↗
EtaleFundamentalGroups.Cohomology.localSystemStalk
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
abbrev localSystemStalk : EtaleFiniteLocallyConstantSetSheaf X ⥤ Type u
def

localSystemStalkIso

L40 ↗
EtaleFundamentalGroups.Cohomology.localSystemStalkIso
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
def localSystemStalkIso :
    ((finiteEtaleEquivFiniteLocallyConstantSetSheaf X).inverse ⋙ FiniteEtale.fiber ξ) ⋙
      forget FintypeCat ≅ localSystemStalk ξ
theorem

localSystemStalk_faithful

L45 ↗
EtaleFundamentalGroups.Cohomology.localSystemStalk_faithful
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 localSystemStalk_faithful : (localSystemStalk ξ).Faithful
theorem

localSystemStalk_preservesEpis

L48 ↗
EtaleFundamentalGroups.Cohomology.localSystemStalk_preservesEpis
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 localSystemStalk_preservesEpis :
    (localSystemStalk ξ).PreservesEpimorphisms
theorem

surjective_finiteLocallyConstant_stalk_of_surjective

L54 ↗
EtaleFundamentalGroups.Cohomology.surjective_finiteLocallyConstant_stalk_of_surjective
Documentation

Surjectivity of a map of finite local systems at one geometric stalk implies surjectivity at every geometric stalk on the connected base.

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 surjective_finiteLocallyConstant_stalk_of_surjective
    {F G : EtaleFiniteLocallyConstantSetSheaf X} (f : F ⟶ G)
    (hf : Function.Surjective ((Scheme.pointSmallEtale ξ).sheafFiber.map f.hom))
    {Ω' : Type u} [Field Ω'] [IsSepClosed Ω'] (ζ : Spec (.of Ω') ⟶ X) :
    Function.Surjective ((Scheme.pointSmallEtale ζ).sheafFiber.map f.hom)
theorem

epi_of_surjective_finiteLocallyConstant_abelianStalk

L69 ↗
EtaleFundamentalGroups.Cohomology.epi_of_surjective_finiteLocallyConstant_abelianStalk
Documentation

A surjective geometric stalk detects an epimorphism of abelian sheaves whose underlying set sheaves are finite locally constant.

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 epi_of_surjective_finiteLocallyConstant_abelianStalk
    {F G : Sheaf X.smallEtaleTopology AddCommGrpCat.{u}} (f : F ⟶ G)
    (hF : IsEtaleFiniteLocallyConstantSet
      ((sheafCompose X.smallEtaleTopology (forget AddCommGrpCat.{u})).obj F))
    (hG : IsEtaleFiniteLocallyConstantSet
      ((sheafCompose X.smallEtaleTopology (forget AddCommGrpCat.{u})).obj G))
    (hf : Function.Surjective ((Scheme.pointSmallEtale ξ).sheafFiber.map f)) :
    Epi f

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.