Module

ClosedImmersionStalks.lean

Nyll.EtaleCohomology.Sites.ClosedImmersionStalks

3 declarations indexed from sourceView source ↗

Module documentation

Stalks of direct image along a closed immersion

At a geometric point of the closed subscheme, the stalk of direct image is the original stalk. Initiality of the constructed neighborhood functor and the comparison of colimits supply the natural isomorphism. The result holds for arbitrary schemes and commutative coefficient rings. Outside the closed subscheme, restriction to its open complement vanishes, so the stalk is zero.

Imports18

Nyll.EtaleCohomology.Sites.BaseChange
Nyll.EtaleCohomology.Sites.ClosedNeighborhoods
Nyll.EtaleCohomology.Sites.EmptySections
Nyll.EtaleCohomology.Sites.ExtensionByZero
Nyll.EtaleCohomology.Sites.PullbackStalks
Nyll.EtaleCohomology.Sites.RestrictionStalks
Nyll.EtaleCohomology.Sites.SheafFunctors
Mathlib.Algebra.Category.ModuleCat.Colimits
Mathlib.AlgebraicGeometry.Sites.EtalePoint
Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Mathlib.AlgebraicGeometry.OpenImmersion
Mathlib.CategoryTheory.Elements
Mathlib.CategoryTheory.Functor.Flat
Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
Mathlib.CategoryTheory.Sites.Point.Comap
Mathlib.CategoryTheory.Sites.Sheaf

Imported by5

lemma

openEtaleRestriction_pushforward_isZero_of_disjoint

L46 ↗

EtaleCohomology.openEtaleRestriction_pushforward_isZero_of_disjoint

Documentation

Restricting direct image to an open subscheme disjoint from the image gives zero. The morphism defining direct image need not be a closed immersion.

Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology

Lean source · statement

lemma openEtaleRestriction_pushforward_isZero_of_disjoint
    {X Z U : Scheme.{u}} (i : Z ⟶ X) (j : U ⟶ X) [IsOpenImmersion j]
    (hd : Disjoint (Set.range j) (Set.range i))
    (R : Type u) [CommRing R] (F : Sheaf Z.smallEtaleTopology (ModuleCat.{u} R)) :
    IsZero ((openEtaleRestriction j R).obj ((etalePushforward i R).obj F))

def

etalePushforwardClosedStalkIso

L69 ↗

EtaleCohomology.etalePushforwardClosedStalkIso

Documentation

At a geometric point of the closed subscheme, direct image has the original stalk.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
variable {X Z : Scheme.{u}} (i : Z ⟶ X) [IsClosedImmersion i]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : Spec (.of Ω) ⟶ Z)
  (R : Type u) [CommRing R]

Lean source · statement

def etalePushforwardClosedStalkIso :
    etalePushforward i R ⋙ (Scheme.pointSmallEtale (s ≫ i)).sheafFiber ≅
      (Scheme.pointSmallEtale s).sheafFiber

lemma

etalePushforward_stalk_isZero_of_not_mem_range

L80 ↗

EtaleCohomology.etalePushforward_stalk_isZero_of_not_mem_range

Documentation

Direct image along a closed immersion has zero stalk outside its image.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
variable {X Z : Scheme.{u}} (i : Z ⟶ X) [IsClosedImmersion i]
  {Ω : Type u} [Field Ω] [IsSepClosed Ω] (s : Spec (.of Ω) ⟶ Z)
  (R : Type u) [CommRing R]

Lean source · statement

lemma etalePushforward_stalk_isZero_of_not_mem_range
    (t : Spec (.of Ω) ⟶ X) (z : Spec (.of Ω)) (hz : t z ∉ Set.range i)
    (F : Sheaf Z.smallEtaleTopology (ModuleCat.{u} R)) :
    IsZero ((Scheme.pointSmallEtale t).sheafFiber.obj ((etalePushforward i R).obj F))

Module documentation

Stalks of direct image along a closed immersion

Declarations

openEtaleRestriction_pushforward_isZero_of_disjoint

etalePushforwardClosedStalkIso

etalePushforward_stalk_isZero_of_not_mem_range