ModuleHenselianLocal.lean
Nyll.EtaleCohomology.Sites.HenselianLocal
2 declarations indexed from sourceView source ↗ Module documentation
Global lifting on a strictly local small étale site
Every covering sieve on the identity object of a strictly local spectrum is maximal: a neighborhood over its closed point has a section. Consequently an epimorphism of actual module sheaves is surjective on global sections. This is the exactness ingredient for the local cohomology calculation in proper base change; no proper base-change theorem is assumed here.
Imports15
- Nyll.SchemeTheory.Etale.HenselianLocalSection
- Nyll.EtaleCohomology.Sites.ConstantPresentation
- Mathlib.Algebra.Category.ModuleCat.AB
- Mathlib.Algebra.Category.ModuleCat.Adjunctions
- Mathlib.Algebra.Category.ModuleCat.Basic
- Mathlib.Algebra.Category.ModuleCat.FilteredColimits
- Mathlib.AlgebraicGeometry.Sites.AffineEtale
- Mathlib.AlgebraicGeometry.Sites.Etale
- Mathlib.CategoryTheory.MorphismProperty.Comma
- Mathlib.CategoryTheory.Adjunction.Limits
- Mathlib.CategoryTheory.ConcreteCategory.Basic
- Mathlib.CategoryTheory.Sites.EpiMono
- Mathlib.CategoryTheory.Sites.LocallySurjective
- Mathlib.CategoryTheory.Sites.Sieves.Basic
- Mathlib.CategoryTheory.Sites.Whiskering
Imported by2
Declarations
EtaleCohomology.sieve_eq_top_of_henselianLocalRing
DocumentationA covering sieve on the identity object of a strictly local small étale site contains its identity, and hence is the maximal sieve.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Opposite
namespace EtaleCohomology
variable (R : Type u) [CommRing R] [HenselianLocalRing R]
[IsSepClosed (IsLocalRing.ResidueField R)]
EtaleCohomology.sheaf_epi_globalSections_surjective_of_henselianLocalRing
DocumentationEpimorphisms of coefficient sheaves over a strictly local spectrum are surjective on the actual module of global sections. The coefficient ring is arbitrary and is unrelated to the strictly local base ring.
Source context 5 commands
Surrounding namespaces, section variables, and local commands at this declaration.
noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Opposite
namespace EtaleCohomology
variable (R : Type u) [CommRing R] [HenselianLocalRing R]
[IsSepClosed (IsLocalRing.ResidueField R)]