ModuleStalks.lean
Nyll.EtaleCohomology.Sites.Stalks
5 declarations indexed from sourceView source ↗ Module documentation
Geometric stalks and exactness on the small étale site
At a point of a scheme, use the separable closure of its residue field to obtain a geometric point and its filtered-colimit stalk functor. The existing conservativity of this family of geometric points detects the vanishing of homology, hence exactness of sequences of coefficient sheaves.
Imports10
- Mathlib.Algebra.Category.ModuleCat.AB
- Mathlib.Algebra.Category.ModuleCat.Adjunctions
- Mathlib.Algebra.Category.ModuleCat.FilteredColimits
- Mathlib.AlgebraicGeometry.Sites.AffineEtale
- Mathlib.AlgebraicGeometry.Sites.EtalePoint
- Mathlib.CategoryTheory.Sites.Point.Basic
- Mathlib.CategoryTheory.Sites.Point.Conservative
- Mathlib.CategoryTheory.Sites.Point.Skyscraper
- Mathlib.Algebra.Homology.ShortComplex.Exact
- Mathlib.Algebra.Homology.ShortComplex.ShortExact
Imported by5
Declarations
EtaleCohomology.residueStalk
DocumentationThe geometric stalk at the separable closure of the residue field of a point.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleCohomology
variable (X : Scheme.{u}) (R : Type u) [CommRing R]
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleCohomology
variable (X : Scheme.{u}) (R : Type u) [CommRing R]
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleCohomology
variable (X : Scheme.{u}) (R : Type u) [CommRing R]
EtaleCohomology.exact_iff_residueStalk
DocumentationExactness of coefficient sheaves is detected on these geometric stalks.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleCohomology
variable (X : Scheme.{u}) (R : Type u) [CommRing R]
EtaleCohomology.shortExact_iff_residueStalk
DocumentationShort exactness is likewise equivalent to short exactness at every geometric stalk.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleCohomology
variable (X : Scheme.{u}) (R : Type u) [CommRing R]