ModuleSubcanonical.lean
Nyll.EtaleCohomology.Sites.Subcanonical
2 declarations indexed from sourceView source ↗ Module documentation
Subcanonicity of the étale sites
The big étale topology is coarser than the subcanonical fppf topology. The inclusion of the small étale site into the slice of the big site is fully faithful, preserves finite limits, and preserves covering sieves. Consequently its representable presheaves are sheaves as well.
Imports9
- Mathlib.AlgebraicGeometry.Sites.Etale
- Mathlib.AlgebraicGeometry.Sites.Fpqc
- Mathlib.AlgebraicGeometry.Sites.Pretopology
- Mathlib.CategoryTheory.Sites.Subcanonical
- Mathlib.CategoryTheory.Sites.SubcanonicalOver
- Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
- Mathlib.CategoryTheory.Sites.CoverPreserving
- Mathlib.CategoryTheory.Functor.Flat
- Mathlib.CategoryTheory.Limits.MorphismProperty
Imported by9
Declarations
EtaleCohomology.etaleTopology_subcanonical
DocumentationRepresentable presheaves on the big étale site are sheaves, by fppf descent.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicGeometry CategoryTheory
universe u
namespace EtaleCohomology
EtaleCohomology.smallEtaleTopology_subcanonical
DocumentationRepresentable presheaves on the small étale site are sheaves.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open AlgebraicGeometry CategoryTheory
universe u
namespace EtaleCohomology