NYLL
Module

GluedRepresentability.lean

Nyll.EtaleCohomology.Constructible.GluedRepresentability
7 declarations indexed from sourceView source ↗

Module documentation

Representability by gluing on the small étale site

Local finite étale representers on a locally directed open cover have canonical transition maps preserving their universal sections. The small-site hypercover therefore glues those sections. Cartesian local comparisons identify the resulting Yoneda map locally with the actual representing equivalences. The sheaf condition then makes it an isomorphism on the whole base.

The cover may have any small index type. No affine, quasi-compact, quasi-separated, connected, or noetherian assumption is made on the base.

Imports21
Imported by2

Declarations

def

etaleGluedRepresenterInclusion

L56 ↗
EtaleCohomology.etaleGluedRepresenterInclusion
Documentation

The canonical inclusion of a local representer into the glued finite étale scheme.

Source context 5 commands

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

noncomputable section
universe u v w
open AlgebraicGeometry CategoryTheory Limits Opposite SchemeTheory.WeilRestriction
namespace EtaleCohomology
variable {X : Scheme.{u}} (G : Sheaf X.smallEtaleTopology (Type u))
  (𝒰 : Scheme.OpenCover.{w} X) [Category.{v} 𝒰.I₀] [𝒰.LocallyDirected]
  (W : ∀ i : 𝒰.I₀, FiniteEtale (𝒰.X i))
  (h : ∀ i : 𝒰.I₀, ((etalePostcompose (𝒰.f i)).op ⋙ G.obj).RepresentableBy
    ((finiteEtaleToEtale (𝒰.X i)).obj (W i)))
  [Quiver.IsThin 𝒰.I₀] [Small.{u} 𝒰.I₀]
Lean source · statement
def etaleGluedRepresenterInclusion (i : 𝒰.I₀) :
    (etalePostcompose (𝒰.f i)).obj ((finiteEtaleToEtale (𝒰.X i)).obj (W i)) ⟶
      (finiteEtaleToEtale X).obj (etaleGluedLocalRepresenter G 𝒰 W h)
def

etaleLocalUniversalSection

L64 ↗
EtaleCohomology.etaleLocalUniversalSection
Documentation

The universal element of the actual slice representation on a cover member.

Source context 5 commands

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

noncomputable section
universe u v w
open AlgebraicGeometry CategoryTheory Limits Opposite SchemeTheory.WeilRestriction
namespace EtaleCohomology
variable {X : Scheme.{u}} (G : Sheaf X.smallEtaleTopology (Type u))
  (𝒰 : Scheme.OpenCover.{w} X) [Category.{v} 𝒰.I₀] [𝒰.LocallyDirected]
  (W : ∀ i : 𝒰.I₀, FiniteEtale (𝒰.X i))
  (h : ∀ i : 𝒰.I₀, ((etalePostcompose (𝒰.f i)).op ⋙ G.obj).RepresentableBy
    ((finiteEtaleToEtale (𝒰.X i)).obj (W i)))
  [Quiver.IsThin 𝒰.I₀] [Small.{u} 𝒰.I₀]
Lean source · statement
def etaleLocalUniversalSection (i : 𝒰.I₀) :
    G.obj.obj (op ((etalePostcompose (𝒰.f i)).obj
      ((finiteEtaleToEtale (𝒰.X i)).obj (W i))))
def

etaleGluedRepresenterHypercover

L71 ↗
EtaleCohomology.etaleGluedRepresenterHypercover
Documentation

The local representers cover the glued object in the small étale site.

Source context 5 commands

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

noncomputable section
universe u v w
open AlgebraicGeometry CategoryTheory Limits Opposite SchemeTheory.WeilRestriction
namespace EtaleCohomology
variable {X : Scheme.{u}} (G : Sheaf X.smallEtaleTopology (Type u))
  (𝒰 : Scheme.OpenCover.{w} X) [Category.{v} 𝒰.I₀] [𝒰.LocallyDirected]
  (W : ∀ i : 𝒰.I₀, FiniteEtale (𝒰.X i))
  (h : ∀ i : 𝒰.I₀, ((etalePostcompose (𝒰.f i)).op ⋙ G.obj).RepresentableBy
    ((finiteEtaleToEtale (𝒰.X i)).obj (W i)))
  [Quiver.IsThin 𝒰.I₀] [Small.{u} 𝒰.I₀]
Lean source · statement
def etaleGluedRepresenterHypercover :
    X.smallEtaleTopology.OneHypercover.{max v w}
      ((finiteEtaleToEtale X).obj (etaleGluedLocalRepresenter G 𝒰 W h))
def

etaleGluedRepresenterCompatibleSections

L81 ↗
EtaleCohomology.etaleGluedRepresenterCompatibleSections
Documentation

Canonical transitions preserve the universal elements, making them compatible.

Source context 5 commands

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

noncomputable section
universe u v w
open AlgebraicGeometry CategoryTheory Limits Opposite SchemeTheory.WeilRestriction
namespace EtaleCohomology
variable {X : Scheme.{u}} (G : Sheaf X.smallEtaleTopology (Type u))
  (𝒰 : Scheme.OpenCover.{w} X) [Category.{v} 𝒰.I₀] [𝒰.LocallyDirected]
  (W : ∀ i : 𝒰.I₀, FiniteEtale (𝒰.X i))
  (h : ∀ i : 𝒰.I₀, ((etalePostcompose (𝒰.f i)).op ⋙ G.obj).RepresentableBy
    ((finiteEtaleToEtale (𝒰.X i)).obj (W i)))
  [Quiver.IsThin 𝒰.I₀] [Small.{u} 𝒰.I₀]
Lean source · statement
def etaleGluedRepresenterCompatibleSections :
    ((etaleGluedRepresenterHypercover G 𝒰 W h).multicospanIndex G.obj).sections
def

etaleGluedRepresenterUniversalSection

L100 ↗
EtaleCohomology.etaleGluedRepresenterUniversalSection
Documentation

The actual sheaf condition glues the local universal elements to a global section.

Source context 5 commands

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

noncomputable section
universe u v w
open AlgebraicGeometry CategoryTheory Limits Opposite SchemeTheory.WeilRestriction
namespace EtaleCohomology
variable {X : Scheme.{u}} (G : Sheaf X.smallEtaleTopology (Type u))
  (𝒰 : Scheme.OpenCover.{w} X) [Category.{v} 𝒰.I₀] [𝒰.LocallyDirected]
  (W : ∀ i : 𝒰.I₀, FiniteEtale (𝒰.X i))
  (h : ∀ i : 𝒰.I₀, ((etalePostcompose (𝒰.f i)).op ⋙ G.obj).RepresentableBy
    ((finiteEtaleToEtale (𝒰.X i)).obj (W i)))
  [Quiver.IsThin 𝒰.I₀] [Small.{u} 𝒰.I₀]
Lean source · statement
def etaleGluedRepresenterUniversalSection :
    G.obj.obj (op ((finiteEtaleToEtale X).obj (etaleGluedLocalRepresenter G 𝒰 W h)))
lemma

etaleGluedRepresenterUniversalSection_restrict

L107 ↗
EtaleCohomology.etaleGluedRepresenterUniversalSection_restrict
Documentation

Restriction of the glued section recovers each local universal element.

Source context 5 commands

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

noncomputable section
universe u v w
open AlgebraicGeometry CategoryTheory Limits Opposite SchemeTheory.WeilRestriction
namespace EtaleCohomology
variable {X : Scheme.{u}} (G : Sheaf X.smallEtaleTopology (Type u))
  (𝒰 : Scheme.OpenCover.{w} X) [Category.{v} 𝒰.I₀] [𝒰.LocallyDirected]
  (W : ∀ i : 𝒰.I₀, FiniteEtale (𝒰.X i))
  (h : ∀ i : 𝒰.I₀, ((etalePostcompose (𝒰.f i)).op ⋙ G.obj).RepresentableBy
    ((finiteEtaleToEtale (𝒰.X i)).obj (W i)))
  [Quiver.IsThin 𝒰.I₀] [Small.{u} 𝒰.I₀]
Lean source · statement
lemma etaleGluedRepresenterUniversalSection_restrict (i : 𝒰.I₀) :
    G.obj.map (etaleGluedRepresenterInclusion G 𝒰 W h i).op
        (etaleGluedRepresenterUniversalSection G 𝒰 W h) =
      etaleLocalUniversalSection G 𝒰 W h i
def

etaleGluedLocalRepresentable

L116 ↗
EtaleCohomology.etaleGluedLocalRepresentable
Documentation

A sheaf with finite étale local representers is represented by their glued scheme.

Source context 5 commands

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

noncomputable section
universe u v w
open AlgebraicGeometry CategoryTheory Limits Opposite SchemeTheory.WeilRestriction
namespace EtaleCohomology
variable {X : Scheme.{u}} (G : Sheaf X.smallEtaleTopology (Type u))
  (𝒰 : Scheme.OpenCover.{w} X) [Category.{v} 𝒰.I₀] [𝒰.LocallyDirected]
  (W : ∀ i : 𝒰.I₀, FiniteEtale (𝒰.X i))
  (h : ∀ i : 𝒰.I₀, ((etalePostcompose (𝒰.f i)).op ⋙ G.obj).RepresentableBy
    ((finiteEtaleToEtale (𝒰.X i)).obj (W i)))
  [Quiver.IsThin 𝒰.I₀] [Small.{u} 𝒰.I₀]
Lean source · statement
def etaleGluedLocalRepresentable :
    G.obj.RepresentableBy ((finiteEtaleToEtale X).obj (etaleGluedLocalRepresenter G 𝒰 W h))

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