Module

Support.lean

Nyll.EtaleCohomology.Constructible.Support

3 declarations indexed from sourceView source ↗

Module documentation

Vanishing away from the support

An inverse image disjoint from the image of an open or closed immersion annihilates extension by zero or closed direct image, respectively. These are statements about the actual sheaves, detected by geometric stalks.

Imports12

Nyll.EtaleCohomology.Constructible.LocallyConstant
Nyll.EtaleCohomology.Sites.ClosedImmersionStalks
Nyll.EtaleCohomology.Sites.ExtensionByZeroStalks
Nyll.EtaleCohomology.Sites.PullbackStalks
Mathlib.AlgebraicGeometry.Sites.AffineEtale
Mathlib.AlgebraicGeometry.Sites.EtalePoint
Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
Mathlib.CategoryTheory.Sites.Point.Conservative
Nyll.EtaleCohomology.Sites.ExtensionByZero
Nyll.EtaleCohomology.Sites.SheafFunctors
Mathlib.CategoryTheory.Sites.ConstantSheaf
Mathlib.CategoryTheory.Sites.Sheafification

Imported by2

lemma

isEtaleFiniteTypeLocallyConstant_of_isZero

L35 ↗

EtaleCohomology.isEtaleFiniteTypeLocallyConstant_of_isZero

Documentation

A zero sheaf has the zero finite type constant model.

Source context 5 commands

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

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

Lean source · statement

lemma isEtaleFiniteTypeLocallyConstant_of_isZero
    {G : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)} (hG : IsZero G) :
    IsEtaleFiniteTypeLocallyConstant R G

lemma

etalePullback_extensionByZero_isZero_of_disjoint

L49 ↗

EtaleCohomology.etalePullback_extensionByZero_isZero_of_disjoint

Documentation

Pullback away from an open immersion's image annihilates its zero extension.

Source context 5 commands

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

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

Lean source · statement

lemma etalePullback_extensionByZero_isZero_of_disjoint
    (f : Y ⟶ X) (j : U ⟶ X) [IsOpenImmersion j]
    (h : Disjoint (Set.range f) (Set.range j))
    (G : Sheaf U.smallEtaleTopology (ModuleCat.{u} R)) :
    IsZero ((etalePullback f R).obj ((etaleExtensionByZero j R).obj G))

lemma

etalePullback_closedPushforward_isZero_of_disjoint

L73 ↗

EtaleCohomology.etalePullback_closedPushforward_isZero_of_disjoint

Documentation

Pullback away from a closed immersion's image annihilates its direct image.

Source context 5 commands

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

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

Lean source · statement

lemma etalePullback_closedPushforward_isZero_of_disjoint
    (f : Y ⟶ X) (i : Z ⟶ X) [IsClosedImmersion i]
    (h : Disjoint (Set.range f) (Set.range i))
    (G : Sheaf Z.smallEtaleTopology (ModuleCat.{u} R)) :
    IsZero ((etalePullback f R).obj ((etalePushforward i R).obj G))

Module documentation

Vanishing away from the support

Declarations

isEtaleFiniteTypeLocallyConstant_of_isZero

etalePullback_extensionByZero_isZero_of_disjoint

etalePullback_closedPushforward_isZero_of_disjoint