Module

FiniteLocallyConstantExact.lean

Nyll.EtaleFundamentalGroups.Cohomology.FiniteLocallyConstantExact

3 declarations indexed from sourceView source ↗

Module documentation

Exactness of finite local systems detected on one geometric stalk

Kernels are pullbacks along a zero object. The actual stalk functor detects these pullbacks and detects epimorphisms for finite local systems on a connected scheme. This proves short exactness of the descended sheaves, without assuming exactness as descent data.

Imports6

Nyll.EtaleFundamentalGroups.Cohomology.FiniteLocallyConstantPullbacks
Nyll.EtaleFundamentalGroups.Cohomology.FiniteLocallyConstantEpis
Nyll.EtaleFundamentalGroups.Cohomology.LocalTrivialization
Nyll.EtaleFundamentalGroups.Cohomology.StalkFiber
Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
Mathlib.Algebra.Category.Grp.Zero

Imported by2

theorem

kernel_isPullback

L31 ↗

EtaleFundamentalGroups.Cohomology.kernel_isPullback

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits EtaleCohomology
universe u
namespace EtaleFundamentalGroups.Cohomology

Lean source · statement

theorem kernel_isPullback {C : Type*} [Category* C] [HasZeroMorphisms C]
    {K E H Z : C} (i : K ⟶ E) (p : E ⟶ H) (w : i ≫ p = 0)
    (h : IsLimit (KernelFork.ofι i w)) (hZ : IsZero Z) :
    IsPullback i (0 : K ⟶ Z) p (0 : Z ⟶ H)

def

kernel_of_isPullback

L42 ↗

EtaleFundamentalGroups.Cohomology.kernel_of_isPullback

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits EtaleCohomology
universe u
namespace EtaleFundamentalGroups.Cohomology

Lean source · statement

def kernel_of_isPullback {C : Type*} [Category* C] [HasZeroMorphisms C]
    {K E H Z : C} (i : K ⟶ E) (p : E ⟶ H) (w : i ≫ p = 0)
    (h : IsPullback i (0 : K ⟶ Z) p (0 : Z ⟶ H)) :
    IsLimit (KernelFork.ofι i w)

theorem

shortExact_of_finiteLocallyConstant_abelianStalk

L59 ↗

EtaleFundamentalGroups.Cohomology.shortExact_of_finiteLocallyConstant_abelianStalk

Documentation

A short complex of finite locally constant abelian sheaves on a connected scheme is short exact if its actual stalk at one geometric point is short exact.

Source context 5 commands

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

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

Lean source · statement

theorem shortExact_of_finiteLocallyConstant_abelianStalk
    (S : ShortComplex (Sheaf X.smallEtaleTopology AddCommGrpCat.{u}))
    (h₁ : IsEtaleFiniteLocallyConstantSet
      ((sheafCompose X.smallEtaleTopology (forget AddCommGrpCat.{u})).obj S.X₁))
    (h₂ : IsEtaleFiniteLocallyConstantSet
      ((sheafCompose X.smallEtaleTopology (forget AddCommGrpCat.{u})).obj S.X₂))
    (h₃ : IsEtaleFiniteLocallyConstantSet
      ((sheafCompose X.smallEtaleTopology (forget AddCommGrpCat.{u})).obj S.X₃))
    (hs : (S.map (Scheme.pointSmallEtale ξ).sheafFiber).ShortExact) : S.ShortExact

Module documentation

Exactness of finite local systems detected on one geometric stalk

Declarations

kernel_isPullback

kernel_of_isPullback

shortExact_of_finiteLocallyConstant_abelianStalk