Module

Extensions.lean

Nyll.EtaleCohomology.Constructible.Extensions

4 declarations indexed from sourceView source ↗

Module documentation

Extensions of constructible module sheaves

Over noetherian coefficients, finite type locally constant sheaves are closed under extensions. A finite free presentation of the quotient lifts on an actual étale cover. The middle term then has the cokernel presentation constructed in ExtensionPresentation. Common stratifications give the corresponding closure theorem for constructible sheaves on arbitrary schemes.

Imports13

Nyll.EtaleCohomology.Constructible.Basic
Nyll.EtaleCohomology.Constructible.ExtensionPresentation
Nyll.EtaleCohomology.Constructible.LocallyConstantKernels
Nyll.EtaleCohomology.Constructible.LocallyConstantProducts
Nyll.EtaleCohomology.Sites.FiniteFreeLift
Nyll.EtaleCohomology.Sites.PullbackStalks
Mathlib.Algebra.Category.ModuleCat.EpiMono
Mathlib.AlgebraicGeometry.Sites.AffineEtale
Mathlib.LinearAlgebra.Finsupp.LinearCombination
Mathlib.RingTheory.Finiteness.Finsupp
Mathlib.RingTheory.Noetherian.Basic
Mathlib.CategoryTheory.Sites.ConstantSheaf
Mathlib.CategoryTheory.Sites.Sheafification

Imported by1

Nyll.EtaleCohomology.Constructible.All

theorem

extension

L38 ↗

EtaleCohomology.IsEtaleFiniteTypeLocallyConstant.extension

Documentation

Extensions preserve finite type local constancy over a noetherian 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] [IsNoetherianRing R]

Lean source · statement

theorem IsEtaleFiniteTypeLocallyConstant.extension
    (S : ShortComplex (Sheaf X.smallEtaleTopology (ModuleCat.{u} R)))
    (hS : S.ShortExact)
    (hA : IsEtaleFiniteTypeLocallyConstant R S.X₁)
    (hN : IsEtaleFiniteTypeLocallyConstant R S.X₃) :
    IsEtaleFiniteTypeLocallyConstant R S.X₂

lemma

extension

L87 ↗

EtaleCohomology.ConstructibleStratification.IsAdaptedTo.extension

Documentation

A common adapted stratification for the ends adapts to the extension.

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] [IsNoetherianRing R]

Lean source · statement

lemma ConstructibleStratification.IsAdaptedTo.extension
    {T : ConstructibleStratification X}
    (S : ShortComplex (Sheaf X.smallEtaleTopology (ModuleCat.{u} R)))
    (hS : S.ShortExact) (hA : T.IsAdaptedTo R S.X₁) (hN : T.IsAdaptedTo R S.X₃) :
    T.IsAdaptedTo R S.X₂

lemma

extension

L97 ↗

EtaleCohomology.HasFiniteConstructibleStratification.extension

Documentation

Extensions preserve the existence of a finite constructible stratification.

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] [IsNoetherianRing R]

Lean source · statement

lemma HasFiniteConstructibleStratification.extension
    (S : ShortComplex (Sheaf X.smallEtaleTopology (ModuleCat.{u} R)))
    (hS : S.ShortExact)
    (hA : HasFiniteConstructibleStratification R S.X₁)
    (hN : HasFiniteConstructibleStratification R S.X₃) :
    HasFiniteConstructibleStratification R S.X₂

theorem

extension

L107 ↗

EtaleCohomology.IsEtaleConstructible.extension

Documentation

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

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] [IsNoetherianRing R]

Lean source · statement

theorem IsEtaleConstructible.extension
    (S : ShortComplex (Sheaf X.smallEtaleTopology (ModuleCat.{u} R)))
    (hS : S.ShortExact) (hA : IsEtaleConstructible R S.X₁)
    (hN : IsEtaleConstructible R S.X₃) : IsEtaleConstructible R S.X₂

Module documentation

Extensions of constructible module sheaves

Declarations

extension

extension

extension

extension