NYLL
Module

SpecLocalRepresenter.lean

Nyll.EtaleCohomology.Constructible.SpecLocalRepresenter
2 declarations indexed from sourceView source ↗

Module documentation

Literal spectrum coordinates for a finite étale local representer

We replace an affine étale cover and its finite étale representing scheme by the spectra of their global section rings. The fully faithful spectrum functor supplies ring maps with these precise spectra. Restriction of the original sheaf remains represented: the map/pullback adjunction transports the representing equivalence, and an actual cartesian square identifies the resulting pullback with the new spectrum.

The base ring is arbitrary; no field or noetherian hypothesis is used.

Imports18
Imported by2

Declarations

def

restrictionRepresentableByBaseChange

L48 ↗
EtaleCohomology.restrictionRepresentableByBaseChange
Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits Opposite
universe u
namespace EtaleCohomology
Lean source · statement
def restrictionRepresentableByBaseChange {X Y Z : Scheme.{u}}
    (f : Y ⟶ X) (e : Z ⟶ Y) (f' : Z ⟶ X)
    [Etale f] [Etale e] [Etale f'] (he : f' = e ≫ f)
    (G : Sheaf X.smallEtaleTopology (Type u)) (W : Y.Etale)
    (h : ((etalePostcompose f).op ⋙ G.obj).RepresentableBy W) :
    ((etalePostcompose f').op ⋙ G.obj).RepresentableBy ((etaleBaseChange e).obj W)
theorem

exists_spec_localRepresenter_faithfullyFlat

L65 ↗
EtaleCohomology.IsEtaleFiniteLocallyConstantSet.exists_spec_localRepresenter_faithfullyFlat
Documentation

A finite locally constant sheaf on Spec R is represented after restriction along a faithfully flat étale ring map R → B by a literal finite étale map Spec C → Spec B. Both the ring properties and the representing equivalence are transported from the constructed affine local representer.

Source context 4 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits Opposite
universe u
namespace EtaleCohomology
Lean source · statement
theorem IsEtaleFiniteLocallyConstantSet.exists_spec_localRepresenter_faithfullyFlat
    {R : CommRingCat.{u}} {G : Sheaf (Spec R).smallEtaleTopology (Type u)}
    (hG : IsEtaleFiniteLocallyConstantSet G) :
    ∃ (B C : CommRingCat.{u}) (f : R →+* B) (g : B →+* C)
      (hf : Etale (Spec.map (CommRingCat.ofHom f)))
      (hg : IsFiniteEtale (Spec.map (CommRingCat.ofHom g))),
      f.FaithfullyFlat ∧ f.Etale ∧ g.FiniteEtale ∧
        Nonempty (((etalePostcompose (hf := hf) (Spec.map (CommRingCat.ofHom f))).op ⋙
          G.obj).RepresentableBy
            (MorphismProperty.Over.mk ⊤ (Spec.map (CommRingCat.ofHom g)) hg.toEtale))

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