Module

RepresenterDescent.lean

Nyll.EtaleCohomology.Constructible.RepresenterDescent

3 declarations indexed from sourceView source ↗

Module documentation

Identifying a descended scheme with the original sheaf

A cartesian local representer descends to a representer of the original sheaf when its projection is invariant under the actual descent action. The proof glues the universal section along a surjective étale morphism, then checks the resulting Yoneda map on the cover.

Imports14

Nyll.EtaleCohomology.Constructible.RepresenterAction
Nyll.EtaleCohomology.Constructible.SigmaRepresenter
Nyll.EtaleCohomology.Sites.EtaleRestriction
Nyll.EtaleCohomology.Sites.Subcanonical
Mathlib.AlgebraicGeometry.Sites.Etale
Mathlib.AlgebraicGeometry.Morphisms.UnderlyingMap
Mathlib.AlgebraicGeometry.PullbackCarrier
Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
Mathlib.CategoryTheory.MorphismProperty.Comma
Mathlib.CategoryTheory.MorphismProperty.Limits
Mathlib.CategoryTheory.Sites.IsSheafFor
Mathlib.CategoryTheory.Sites.Sheaf
Mathlib.CategoryTheory.Sites.Subcanonical
Mathlib.CategoryTheory.Yoneda

Imported by2

lemma

isSheafFor_surjective_etaleHom

L39 ↗

EtaleCohomology.isSheafFor_surjective_etaleHom

Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology

Lean source · statement

lemma isSheafFor_surjective_etaleHom {X : Scheme.{u}}
    (G : Sheaf X.smallEtaleTopology (Type u)) {U V : X.Etale}
    (q : U ⟶ V) [Surjective q.left] :
    Presieve.IsSheafFor G.obj (Presieve.singleton q)

lemma

representerSection_compatible

L64 ↗

EtaleCohomology.representerSection_compatible

Documentation

The quotient's invariance makes the local universal section compatible on every pair of arrows over the proposed descended scheme.

Source context 11 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (f : Y ⟶ X) [Etale f]
variable (G : Sheaf X.smallEtaleTopology (Type u)) (W : Y.Etale)
variable (h : ((etalePostcompose f).op ⋙ G.obj).RepresentableBy W)
variable (Z : X.Etale) (q : (etalePostcompose f).obj W ⟶ Z)
variable (hcart : IsPullback W.hom q.left f Z.hom)
variable (hact : representerAction f G W h ≫ q.left =
  pullback.snd f (W.hom ≫ f) ≫ q.left)
include hcart hact

Lean source · statement

lemma representerSection_compatible {T : X.Etale}
    (a b : T ⟶ (etalePostcompose f).obj W) (hab : a ≫ q = b ≫ q) :
    G.obj.map a.op (representerSection f G W h) =
      G.obj.map b.op (representerSection f G W h)

def

representableBy_of_cartesian_localRepresenter

L94 ↗

EtaleCohomology.representableBy_of_cartesian_localRepresenter

Documentation

An equivariant cartesian local representer represents the original sheaf. The universal section is descended using the actual sheaf condition.

Source context 11 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits Opposite
namespace EtaleCohomology
variable {X Y : Scheme.{u}} (f : Y ⟶ X) [Etale f]
variable (G : Sheaf X.smallEtaleTopology (Type u)) (W : Y.Etale)
variable (h : ((etalePostcompose f).op ⋙ G.obj).RepresentableBy W)
variable (Z : X.Etale) (q : (etalePostcompose f).obj W ⟶ Z)
variable (hcart : IsPullback W.hom q.left f Z.hom)
variable (hact : representerAction f G W h ≫ q.left =
  pullback.snd f (W.hom ≫ f) ≫ q.left)
include hcart hact

Lean source · statement

def representableBy_of_cartesian_localRepresenter [Surjective f] :
    G.obj.RepresentableBy Z

Module documentation

Identifying a descended scheme with the original sheaf

Declarations

isSheafFor_surjective_etaleHom

representerSection_compatible

representableBy_of_cartesian_localRepresenter