ModuleEtale.lean
Nyll.EtaleCohomology.Classical.Etale
4 declarations indexed from sourceView source ↗ Module documentation
Classical étale cohomology with module coefficients
All site and Ext hypotheses are supplied by the existing affine étale comparison and Grothendieck abelian category instances. The underlying groups are Sheaf.H on the small étale site.
Declarations
EtaleCohomology.etaleCohomology
DocumentationClassical étale cohomology, bundled with its coefficient module.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleCohomology
variable (X : Scheme.{u}) (R : Type u) [CommRing R]
EtaleCohomology.etaleCohomologyZeroEquiv
DocumentationDegree-zero étale cohomology is the module of sections over the terminal étale object.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleCohomology
variable (X : Scheme.{u}) (R : Type u) [CommRing R]
EtaleCohomology.finiteCoefficientSheaf
DocumentationThe finite-level coefficient object on the actual small étale site.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleCohomology
variable (X : Scheme.{u}) (R : Type u) [CommRing R]
EtaleCohomology.finiteCoefficientCohomologyZeroEquiv
DocumentationFinite-level classical cohomology and global sections agree in degree zero.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleCohomology
variable (X : Scheme.{u}) (R : Type u) [CommRing R]