Module

ClosedImmersionExact.lean

Nyll.EtaleCohomology.Sites.ClosedImmersionExact

2 declarations indexed from sourceView source ↗

Module documentation

Exactness of direct image along a closed immersion

At a geometric point inside the image, direct image has the original stalk. Outside the image, it has zero stalk. Geometric stalks therefore show that direct image preserves short exact sequences and finite colimits. There are no noetherian, finite-type, or base-field hypotheses.

Imports21

Nyll.EtaleCohomology.Sites.ClosedImmersionStalks
Nyll.EtaleCohomology.Sites.SheafFunctors
Nyll.EtaleCohomology.Sites.Stalks
Nyll.SchemeTheory.Morphisms.ClosedImmersionLift
Mathlib.Algebra.Category.ModuleCat.AB
Mathlib.Algebra.Category.ModuleCat.Colimits
Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Mathlib.Algebra.Category.ModuleCat.Limits
Mathlib.Algebra.Homology.ShortComplex.Basic
Mathlib.Algebra.Homology.ShortComplex.Exact
Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
Mathlib.Algebra.Homology.ShortComplex.ShortExact
Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Mathlib.AlgebraicGeometry.Properties
Mathlib.AlgebraicGeometry.Sites.AffineEtale
Mathlib.AlgebraicGeometry.Sites.EtalePoint
Mathlib.CategoryTheory.Limits.Preserves.Basic
Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
Mathlib.CategoryTheory.Preadditive.Biproducts
Mathlib.CategoryTheory.Sites.Point.Skyscraper
Mathlib.FieldTheory.IsSepClosed

Imported by2

lemma

etalePushforwardClosed_shortExact

L50 ↗

EtaleCohomology.etalePushforwardClosed_shortExact

Documentation

Direct image along a closed immersion preserves short exact sequences.

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 Z : Scheme.{u}} (i : Z ⟶ X) [IsClosedImmersion i]
  (R : Type u) [CommRing R]

Lean source · statement

lemma etalePushforwardClosed_shortExact
    (S : ShortComplex (Sheaf Z.smallEtaleTopology (ModuleCat.{u} R)))
    (hS : S.ShortExact) : (S.map (etalePushforward i R)).ShortExact

instance

etalePushforwardClosed_preservesFiniteColimits

L78 ↗

EtaleCohomology.etalePushforwardClosed_preservesFiniteColimits