Module

ExtensionByZero.lean

Nyll.EtaleCohomology.Sites.ExtensionByZero

17 declarations indexed from sourceView source ↗

Module documentation

Extension by zero for an open immersion

Composition with an open immersion gives a fully faithful, continuous inclusion of small étale sites. Its adjunction with base change identifies restriction of sheaves with the inverse image constructed in Sites.SheafFunctors.

Extension by zero is constructed by passing to the affine étale site, taking left Kan extension, and sheafifying. The resulting adjunction is with the existing inverse-image functor. The affine-site comparison supplies the required small colimits. The stalk formula and exactness are subsequent steps.

Reference: https://stacks.math.columbia.edu/tag/03S2

Imports20

Nyll.EtaleCohomology.Sites.BaseChange
Nyll.EtaleCohomology.Sites.EtaleRestriction
Nyll.EtaleCohomology.Sites.SheafFunctors
Mathlib.Algebra.Category.ModuleCat.Colimits
Mathlib.AlgebraicGeometry.Morphisms.Etale
Mathlib.AlgebraicGeometry.Sites.AffineEtale
Mathlib.AlgebraicGeometry.Sites.Etale
Mathlib.CategoryTheory.Adjunction.Basic
Mathlib.CategoryTheory.Comma.Over.Basic
Mathlib.CategoryTheory.Comma.StructuredArrow.Small
Mathlib.CategoryTheory.Functor.FullyFaithful
Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
Mathlib.CategoryTheory.Limits.EssentiallySmall
Mathlib.CategoryTheory.MorphismProperty.Comma
Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
Mathlib.CategoryTheory.Sites.CoverPreserving
Mathlib.CategoryTheory.Sites.DenseSubsite.InducedTopology
Mathlib.CategoryTheory.Sites.Over
Mathlib.CategoryTheory.Sites.Continuous
Mathlib.CategoryTheory.Sites.Pullback

Imported by7

abbrev

openEtaleInclusion

L55 ↗

EtaleCohomology.openEtaleInclusion

Documentation

Composition with an open immersion on the small étale sites.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleCohomology
variable {U X : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]

Lean source · statement

abbrev openEtaleInclusion : U.Etale ⥤ X.Etale

def

openEtaleInclusionBaseChangeAdjunction

L58 ↗

EtaleCohomology.openEtaleInclusionBaseChangeAdjunction

Documentation

Composition with the immersion is left adjoint to base change.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleCohomology
variable {U X : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]

Lean source · statement

def openEtaleInclusionBaseChangeAdjunction : openEtaleInclusion j ⊣ etaleBaseChange j

def

openEtaleInclusionFullyFaithful

L62 ↗

EtaleCohomology.openEtaleInclusionFullyFaithful

Documentation

A morphism over the ambient scheme is already over the open subscheme.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleCohomology
variable {U X : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]

Lean source · full declaration

def openEtaleInclusionFullyFaithful : (openEtaleInclusion j).FullyFaithful where
  preimage {V W} f := (Scheme.Etale.forget U).preimage
    (CategoryTheory.Over.homMk ((Scheme.Etale.forget X).map f).left (by
      apply (cancel_mono j).mp
      exact (Category.assoc _ _ _).trans
        (CategoryTheory.Over.w ((Scheme.Etale.forget X).map f))))
  map_preimage {V W} f := by
    apply (Scheme.Etale.forget X).map_injective
    ext
    exact congrArg
      (fun g : (Scheme.Etale.forget U).obj V ⟶ (Scheme.Etale.forget U).obj W => g.left)
      ((Scheme.Etale.forget U).map_preimage _)
  preimage_map f := (Scheme.Etale.forget U).preimage_map f

instance

(anonymous instance)

L76 ↗

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleCohomology
variable {U X : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]

Lean source · statement

instance : (openEtaleInclusion j).Full

instance

(anonymous instance)

L77 ↗

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleCohomology
variable {U X : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]

Lean source · statement

instance : (openEtaleInclusion j).Faithful

lemma

openEtaleInclusion_coverPreserving

L80 ↗

EtaleCohomology.openEtaleInclusion_coverPreserving

Documentation

An étale covering over the open subscheme is an étale covering over the ambient scheme.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleCohomology
variable {U X : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]

Lean source · statement

lemma openEtaleInclusion_coverPreserving :
    CoverPreserving U.smallEtaleTopology X.smallEtaleTopology (openEtaleInclusion j)

def

openEtaleRestriction

L87 ↗

EtaleCohomology.openEtaleRestriction

Documentation

Restriction of coefficient sheaves by precomposition with the inclusion of sites.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleCohomology
variable {U X : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]
variable (R : Type u) [CommRing R]

Lean source · statement

def openEtaleRestriction :
    Sheaf X.smallEtaleTopology (ModuleCat.{u} R) ⥤
      Sheaf U.smallEtaleTopology (ModuleCat.{u} R)

def

openEtaleRestrictionPushforwardAdjunction

L94 ↗

EtaleCohomology.openEtaleRestrictionPushforwardAdjunction

Documentation

Restriction is left adjoint to the already constructed direct image.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleCohomology
variable {U X : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]
variable (R : Type u) [CommRing R]

Lean source · statement

def openEtaleRestrictionPushforwardAdjunction :
    openEtaleRestriction j R ⊣ etalePushforward j R

def

etalePullbackOpenRestrictionIso

L100 ↗

EtaleCohomology.etalePullbackOpenRestrictionIso

Documentation

Inverse image along an open immersion is ordinary restriction of sheaves.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleCohomology
variable {U X : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]
variable (R : Type u) [CommRing R]

Lean source · statement

def etalePullbackOpenRestrictionIso : etalePullback j R ≅ openEtaleRestriction j R

def

affineOpenEtaleInclusion

L105 ↗

EtaleCohomology.affineOpenEtaleInclusion

Documentation

The inclusion restricted to affine étale schemes over the open subscheme.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleCohomology
variable {U X : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]
variable (R : Type u) [CommRing R]

Lean source · statement

def affineOpenEtaleInclusion : U.AffineEtale ⥤ X.Etale

instance

(anonymous instance)

L108 ↗

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleCohomology
variable {U X : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]
variable (R : Type u) [CommRing R]

Lean source · statement

instance : (affineOpenEtaleInclusion j).IsContinuous (Scheme.AffineEtale.topology U)
    X.smallEtaleTopology

instance

(anonymous instance)

L113 ↗

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleCohomology
variable {U X : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]
variable (R : Type u) [CommRing R]

Lean source · statement

instance (F : U.AffineEtaleᵒᵖ ⥤ ModuleCat.{u} R) :
    (affineOpenEtaleInclusion j).op.HasPointwiseLeftKanExtension F

def

etaleExtensionByZero

L122 ↗

EtaleCohomology.etaleExtensionByZero

Documentation

Extension by zero, constructed by left Kan extension and sheafification.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleCohomology
variable {U X : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]
variable (R : Type u) [CommRing R]

Lean source · statement

def etaleExtensionByZero :
    Sheaf U.smallEtaleTopology (ModuleCat.{u} R) ⥤
      Sheaf X.smallEtaleTopology (ModuleCat.{u} R)

def

affineOpenRestrictionIso

L130 ↗

EtaleCohomology.affineOpenRestrictionIso

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleCohomology
variable {U X : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]
variable (R : Type u) [CommRing R]

Lean source · statement

def affineOpenRestrictionIso :
    (affineOpenEtaleInclusion j).sheafPushforwardContinuous (ModuleCat.{u} R)
        (Scheme.AffineEtale.topology U) X.smallEtaleTopology ⋙
      (Scheme.AffineEtale.sheafEquiv U (ModuleCat.{u} R)).functor ≅
      openEtaleRestriction j R

def

etaleExtensionByZeroAdjunction

L146 ↗

EtaleCohomology.etaleExtensionByZeroAdjunction

Documentation

Extension by zero is left adjoint to inverse image along the open immersion.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleCohomology
variable {U X : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]
variable (R : Type u) [CommRing R]

Lean source · statement

def etaleExtensionByZeroAdjunction : etaleExtensionByZero j R ⊣ etalePullback j R

instance

(anonymous instance)

L154 ↗

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleCohomology
variable {U X : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]
variable (R : Type u) [CommRing R]

Lean source · statement

instance : (etaleExtensionByZero j R).IsLeftAdjoint

instance

(anonymous instance)

L157 ↗

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory CategoryTheory.Limits Opposite
namespace EtaleCohomology
variable {U X : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]
variable (R : Type u) [CommRing R]

Lean source · statement

instance : (etalePullback j R).IsRightAdjoint

Module documentation

Extension by zero for an open immersion

Declarations