Module

LocallyConstantKernels.lean

Nyll.EtaleCohomology.Constructible.LocallyConstantKernels

4 declarations indexed from sourceView source ↗

Module documentation

Kernels and cokernels of finite type locally constant sheaves

The finite local models of the actual sheaf morphism give the kernel and cokernel models. Noetherian coefficients are needed for kernels; cokernels are finite type over any commutative ring.

Imports10

Nyll.EtaleCohomology.Constructible.ConstantMorphism
Nyll.EtaleCohomology.Constructible.LocallyConstant
Nyll.EtaleCohomology.Sites.ConstantPullback
Nyll.EtaleCohomology.Sites.PullbackStalks
Mathlib.Algebra.Category.ModuleCat.EpiMono
Mathlib.AlgebraicGeometry.Sites.AffineEtale
Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
Mathlib.CategoryTheory.Sites.ConstantSheaf
Mathlib.CategoryTheory.Sites.Sheafification
Mathlib.RingTheory.Noetherian.Basic

Imported by3

lemma

constant_kernel

L32 ↗

EtaleCohomology.constant_kernel

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits
namespace EtaleCohomology
variable {X : Scheme.{u}} {R : Type u} [CommRing R]

Lean source · statement

lemma constant_kernel [IsNoetherianRing R]
    (M N : ModuleCat.{u} R) [Module.Finite R M]
    (φ : (constantSheaf X.smallEtaleTopology (ModuleCat.{u} R)).obj M ⟶
      (constantSheaf X.smallEtaleTopology (ModuleCat.{u} R)).obj N) :
    IsEtaleFiniteTypeLocallyConstant R (kernel φ)

lemma

constant_cokernel

L51 ↗

EtaleCohomology.constant_cokernel

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits
namespace EtaleCohomology
variable {X : Scheme.{u}} {R : Type u} [CommRing R]

Lean source · statement

lemma constant_cokernel
    (M N : ModuleCat.{u} R) [Module.Finite R M] [Module.Finite R N]
    (φ : (constantSheaf X.smallEtaleTopology (ModuleCat.{u} R)).obj M ⟶
      (constantSheaf X.smallEtaleTopology (ModuleCat.{u} R)).obj N) :
    IsEtaleFiniteTypeLocallyConstant R (cokernel φ)

theorem

kernel

L76 ↗

EtaleCohomology.IsEtaleFiniteTypeLocallyConstant.kernel

Documentation

Kernels of maps of finite type locally constant sheaves are finite type locally constant over a noetherian coefficient ring.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits
namespace EtaleCohomology
variable {X : Scheme.{u}} {R : Type u} [CommRing R]

Lean source · statement

theorem IsEtaleFiniteTypeLocallyConstant.kernel [IsNoetherianRing R]
    {G H : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)} (φ : G ⟶ H)
    (hG : IsEtaleFiniteTypeLocallyConstant R G)
    (hH : IsEtaleFiniteTypeLocallyConstant R H) :
    IsEtaleFiniteTypeLocallyConstant R (kernel φ)

theorem

cokernel

L103 ↗

EtaleCohomology.IsEtaleFiniteTypeLocallyConstant.cokernel

Documentation

Cokernels preserve finite type local constancy over any coefficient ring.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits
namespace EtaleCohomology
variable {X : Scheme.{u}} {R : Type u} [CommRing R]

Lean source · statement

theorem IsEtaleFiniteTypeLocallyConstant.cokernel
    {G H : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)} (φ : G ⟶ H)
    (hG : IsEtaleFiniteTypeLocallyConstant R G)
    (hH : IsEtaleFiniteTypeLocallyConstant R H) :
    IsEtaleFiniteTypeLocallyConstant R (cokernel φ)

Module documentation

Kernels and cokernels of finite type locally constant sheaves

Declarations

constant_kernel

constant_cokernel

kernel

cokernel