Module

FiniteLocallyConstantPullbacks.lean

Nyll.EtaleFundamentalGroups.Cohomology.FiniteLocallyConstantPullbacks

4 declarations indexed from sourceView source ↗

Module documentation

Pullbacks of finite local systems detected on a geometric stalk

The finite étale realization preserves finite limits, and the Galois fiber functor reflects them. Hence a square of finite locally constant abelian sheaves is cartesian if its actual geometric stalk square is cartesian. This detects kernels without assuming descent of exactness.

Imports5

Nyll.EtaleCohomology.Constructible.Monodromy
Nyll.EtaleFundamentalGroups.Cohomology.FiniteLocallyConstantDetection
Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
Mathlib.CategoryTheory.Sites.Subcanonical
Mathlib.CategoryTheory.Sites.PreservesLimits

Imported by2

theorem

finiteEtaleSheaf_preservesFiniteLimits

L31 ↗

EtaleFundamentalGroups.Cohomology.finiteEtaleSheaf_preservesFiniteLimits

Source context 5 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

Lean source · statement

theorem finiteEtaleSheaf_preservesFiniteLimits (X : Scheme.{u}) :
    PreservesFiniteLimits (finiteEtaleSheaf X)

theorem

localSystemInclusion_preservesFiniteLimits

L43 ↗

EtaleFundamentalGroups.Cohomology.localSystemInclusion_preservesFiniteLimits

Source context 5 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

Lean source · statement

theorem localSystemInclusion_preservesFiniteLimits (X : Scheme.{u}) :
    PreservesFiniteLimits (ObjectProperty.ι (IsEtaleFiniteLocallyConstantSet (X := X)))

theorem

localSystemStalk_reflectsPullbacks

L57 ↗

EtaleFundamentalGroups.Cohomology.localSystemStalk_reflectsPullbacks

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 localSystemStalk_reflectsPullbacks :
    ReflectsLimitsOfShape WalkingCospan
      (ObjectProperty.ι (IsEtaleFiniteLocallyConstantSet (X := X)) ⋙
        (Scheme.pointSmallEtale ξ).sheafFiber)

theorem

isPullback_of_finiteLocallyConstant_abelianStalk

L72 ↗

EtaleFundamentalGroups.Cohomology.isPullback_of_finiteLocallyConstant_abelianStalk

Documentation

A square of finite locally constant abelian sheaves is a pullback if its square at one geometric point is a pullback of actual abelian stalks.

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 isPullback_of_finiteLocallyConstant_abelianStalk
    {P F G H : Sheaf X.smallEtaleTopology AddCommGrpCat.{u}}
    (a : P ⟶ F) (b : P ⟶ G) (f : F ⟶ H) (g : G ⟶ H)
    (w : a ≫ f = b ≫ g)
    (hP : IsEtaleFiniteLocallyConstantSet
      ((sheafCompose X.smallEtaleTopology (forget AddCommGrpCat.{u})).obj P))
    (hF : IsEtaleFiniteLocallyConstantSet
      ((sheafCompose X.smallEtaleTopology (forget AddCommGrpCat.{u})).obj F))
    (hG : IsEtaleFiniteLocallyConstantSet
      ((sheafCompose X.smallEtaleTopology (forget AddCommGrpCat.{u})).obj G))
    (hH : IsEtaleFiniteLocallyConstantSet
      ((sheafCompose X.smallEtaleTopology (forget AddCommGrpCat.{u})).obj H))
    (hp : IsPullback ((Scheme.pointSmallEtale ξ).sheafFiber.map a)
      ((Scheme.pointSmallEtale ξ).sheafFiber.map b)
      ((Scheme.pointSmallEtale ξ).sheafFiber.map f)
      ((Scheme.pointSmallEtale ξ).sheafFiber.map g)) :
    IsPullback a b f g

Module documentation

Pullbacks of finite local systems detected on a geometric stalk

Declarations

finiteEtaleSheaf_preservesFiniteLimits

localSystemInclusion_preservesFiniteLimits

localSystemStalk_reflectsPullbacks

isPullback_of_finiteLocallyConstant_abelianStalk