NYLL
Module

RepresenterIso.lean

Nyll.EtaleCohomology.Constructible.RepresenterIso
1 declaration indexed from sourceView source ↗

Module documentation

Transporting finite étale representers across a scheme isomorphism

A finite étale representative of the restriction along an isomorphism gives a representative of the original sheaf. We use its base change along the inverse isomorphism, the map/pullback adjunction, and the natural comparison between composing the two isomorphisms and the identity functor.

Imports8
Imported by2

Declarations

def

finiteEtaleRepresentableBy_of_isoRestriction

L36 ↗
EtaleCohomology.finiteEtaleRepresentableBy_of_isoRestriction
Documentation

Pulling the finite étale representer back along the inverse isomorphism represents the original sheaf. The comparison is constructed from the actual postcomposition/base-change adjunction and its natural identity comparison.

Source context 4 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits
namespace EtaleCohomology
Lean source · statement
def finiteEtaleRepresentableBy_of_isoRestriction {X Y : Scheme.{u}} (e : Y ≅ X)
    (G : Sheaf X.smallEtaleTopology (Type u)) (W : FiniteEtale Y)
    (h : ((etalePostcompose e.hom).op ⋙ G.obj).RepresentableBy
      ((finiteEtaleToEtale Y).obj W)) :
    G.obj.RepresentableBy ((finiteEtaleToEtale X).obj ((FiniteEtale.pullback e.inv).obj W))

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.