Module

EmptySections.lean

Nyll.EtaleCohomology.Sites.EmptySections

1 declaration indexed from sourceView source ↗

Module documentation

Sections on the empty étale scheme

The empty sieve covers an empty étale object. Its sheaf sections are terminal, and hence zero in any coefficient category with zero morphisms.

Imports5

Mathlib.AlgebraicGeometry.Sites.Small
Mathlib.AlgebraicGeometry.Sites.Etale
Mathlib.CategoryTheory.Sites.Sheaf
Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects

Imported by2

lemma

etaleSections_isZero_of_isEmpty

L27 ↗

EtaleCohomology.etaleSections_isZero_of_isEmpty

Documentation

Sections of an étale sheaf over an empty object form a zero object.

Source context 3 commands

Surrounding namespaces, section variables, and local commands at this declaration.

universe u v w
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology

Lean source · statement

lemma etaleSections_isZero_of_isEmpty
    {X : Scheme.{u}} (V : X.Etale) [IsEmpty V.left]
    {A : Type v} [Category.{w} A] [HasZeroMorphisms A]
    (F : Sheaf X.smallEtaleTopology A) : IsZero (F.obj.obj (op V))

Module documentation

Sections on the empty étale scheme

Declarations

etaleSections_isZero_of_isEmpty