Module

Kernels.lean

Nyll.EtaleCohomology.Constructible.Kernels

6 declarations indexed from sourceView source ↗

Module documentation

Kernels and cokernels of constructible sheaves

A common finite adapted stratification reduces both operations to their finite type locally constant counterparts. The argument applies on every affine open without any noetherian hypothesis on the scheme.

Imports5

Nyll.EtaleCohomology.Constructible.Basic
Nyll.EtaleCohomology.Constructible.LocallyConstantKernels
Nyll.EtaleCohomology.Sites.PullbackStalks
Mathlib.CategoryTheory.Limits.Preserves.Shapes.Kernels
Mathlib.RingTheory.Noetherian.Basic

Imported by1

Nyll.EtaleCohomology.Constructible.All

lemma

kernel

L28 ↗

EtaleCohomology.ConstructibleStratification.IsAdaptedTo.kernel

Documentation

A common adapted stratification remains adapted to the 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 ConstructibleStratification.IsAdaptedTo.kernel [IsNoetherianRing R]
    {S : ConstructibleStratification X}
    {G H : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)} (φ : G ⟶ H)
    (hG : S.IsAdaptedTo R G) (hH : S.IsAdaptedTo R H) :
    S.IsAdaptedTo R (kernel φ)

lemma

cokernel

L39 ↗

EtaleCohomology.ConstructibleStratification.IsAdaptedTo.cokernel

Documentation

A common adapted stratification remains adapted to the 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 ConstructibleStratification.IsAdaptedTo.cokernel
    {S : ConstructibleStratification X}
    {G H : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)} (φ : G ⟶ H)
    (hG : S.IsAdaptedTo R G) (hH : S.IsAdaptedTo R H) :
    S.IsAdaptedTo R (cokernel φ)

lemma

kernel

L50 ↗

EtaleCohomology.HasFiniteConstructibleStratification.kernel

Documentation

Finite stratifiability is preserved by kernels over noetherian coefficients.

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 HasFiniteConstructibleStratification.kernel [IsNoetherianRing R]
    {G H : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)} (φ : G ⟶ H)
    (hG : HasFiniteConstructibleStratification R G)
    (hH : HasFiniteConstructibleStratification R H) :
    HasFiniteConstructibleStratification R (kernel φ)

lemma

cokernel

L59 ↗

EtaleCohomology.HasFiniteConstructibleStratification.cokernel

Documentation

Finite stratifiability is preserved by cokernels.

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 HasFiniteConstructibleStratification.cokernel
    {G H : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)} (φ : G ⟶ H)
    (hG : HasFiniteConstructibleStratification R G)
    (hH : HasFiniteConstructibleStratification R H) :
    HasFiniteConstructibleStratification R (cokernel φ)

theorem

kernel

L68 ↗

EtaleCohomology.IsEtaleConstructible.kernel

Documentation

Constructible module sheaves over a noetherian ring are closed under kernels.

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 IsEtaleConstructible.kernel [IsNoetherianRing R]
    {G H : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)} (φ : G ⟶ H)
    (hG : IsEtaleConstructible R G) (hH : IsEtaleConstructible R H) :
    IsEtaleConstructible R (kernel φ)

theorem

cokernel

L78 ↗

EtaleCohomology.IsEtaleConstructible.cokernel

Documentation

Constructible module sheaves are closed under cokernels.

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 IsEtaleConstructible.cokernel
    {G H : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)} (φ : G ⟶ H)
    (hG : IsEtaleConstructible R G) (hH : IsEtaleConstructible R H) :
    IsEtaleConstructible R (cokernel φ)

Module documentation

Kernels and cokernels of constructible sheaves

Declarations

kernel

cokernel

kernel

cokernel

kernel

cokernel