Module

ZariskiGlobalSections.lean

Nyll.EtaleCohomology.Sites.ZariskiGlobalSections

3 declarations indexed from sourceView source ↗

Module documentation

Global sections of the actual Zariski restriction

The top open subscheme is identified with the identity object of the small étale site. The induced identification of sections commutes with restriction to every open subscheme.

Imports4

Nyll.EtaleCohomology.Sites.ZariskiRestriction
Mathlib.AlgebraicGeometry.Restrict
Mathlib.CategoryTheory.MorphismProperty.Comma
Mathlib.CategoryTheory.Opposites

Imported by3

def

zariskiToEtaleTopIso

L32 ↗

EtaleCohomology.zariskiToEtaleTopIso

Documentation

The top open, included into the small étale site, is its identity object.

Source context 5 commands

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

noncomputable section
universe u v w
open AlgebraicGeometry CategoryTheory Opposite
namespace EtaleCohomology
variable (X : Scheme.{u})

Lean source · statement

def zariskiToEtaleTopIso :
    (zariskiToEtale X).obj ⊤ ≅ Scheme.Etale.mk (𝟙 X)

def

etaleZariskiGlobalSectionsIso

L41 ↗

EtaleCohomology.etaleZariskiGlobalSectionsIso

Documentation

The actual identification of global sections on the two sites.

Source context 6 commands

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

noncomputable section
universe u v w
open AlgebraicGeometry CategoryTheory Opposite
namespace EtaleCohomology
variable (X : Scheme.{u})
variable (A : Type v) [Category.{w} A]

Lean source · statement

def etaleZariskiGlobalSectionsIso (F : Sheaf X.smallEtaleTopology A) :
    ((etaleZariskiRestriction X A).obj F).obj.obj (op (⊤ : X.Opens)) ≅
      F.obj.obj (op (Scheme.Etale.mk (𝟙 X)))

theorem

etaleZariskiGlobalSectionsIso_inv_restrict

L48 ↗

EtaleCohomology.etaleZariskiGlobalSectionsIso_inv_restrict

Documentation

Converting a global étale section and restricting to an open is exactly restriction along that open's structural morphism.

Source context 6 commands

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

noncomputable section
universe u v w
open AlgebraicGeometry CategoryTheory Opposite
namespace EtaleCohomology
variable (X : Scheme.{u})
variable (A : Type v) [Category.{w} A]

Lean source · full declaration

theorem etaleZariskiGlobalSectionsIso_inv_restrict
    (F : Sheaf X.smallEtaleTopology A) (U : X.Opens) :
    (etaleZariskiGlobalSectionsIso X A F).inv ≫
        ((etaleZariskiRestriction X A).obj F).obj.map
          (homOfLE (show U ≤ ⊤ from le_top)).op =
      F.obj.map
        (MorphismProperty.Over.homMk
          (P := show MorphismProperty Scheme.{u} from @Etale) (Q := ⊤)
          (A := (zariskiToEtale X).obj U) (B := Scheme.Etale.mk (𝟙 X))
          U.ι (Category.comp_id U.ι)).op := by
  let g : (zariskiToEtale X).obj U ⟶ (zariskiToEtale X).obj ⊤ :=
    (zariskiToEtale X).map (homOfLE (show U ≤ ⊤ from le_top))
  let j : (zariskiToEtale X).obj U ⟶ Scheme.Etale.mk (𝟙 X) :=
    MorphismProperty.Over.homMk
      (P := show MorphismProperty Scheme.{u} from @Etale) (Q := ⊤)
      U.ι (Category.comp_id U.ι)
  have hgj : g ≫ (zariskiToEtaleTopIso X).hom = j := by
    apply MorphismProperty.Over.Hom.ext
    change g.left ≫ (⊤ : X.Opens).ι = U.ι
    exact g.w
  change F.obj.map (zariskiToEtaleTopIso X).hom.op ≫ F.obj.map g.op = F.obj.map j.op
  rw [← F.obj.map_comp, ← op_comp, hgj]

Module documentation

Global sections of the actual Zariski restriction

Declarations

zariskiToEtaleTopIso

etaleZariskiGlobalSectionsIso

etaleZariskiGlobalSectionsIso_inv_restrict