Module

Localization.lean

Nyll.EtaleCohomology.Sites.Localization

3 declarations indexed from sourceView source ↗

Module documentation

Open-closed localization for étale coefficient sheaves

For a closed immersion and its complementary open immersion, the actual adjunction counit and unit give the short exact sequence 0 ⟶ j_!j^*G ⟶ G ⟶ i_*i^*G ⟶ 0. The composite is zero and exactness is checked on all geometric stalks. No base field, noetherian, finite-type, or constructibility hypothesis is used.

Imports20

Nyll.EtaleCohomology.Sites.ClosedAdjunction
Nyll.EtaleCohomology.Sites.ClosedImmersionStalks
Nyll.EtaleCohomology.Sites.ExtensionByZero
Nyll.EtaleCohomology.Sites.ExtensionByZeroStalks
Nyll.EtaleCohomology.Sites.OpenAdjunction
Nyll.EtaleCohomology.Sites.SheafFunctors
Nyll.EtaleCohomology.Sites.Stalks
Nyll.SchemeTheory.Morphisms.ClosedImmersionLift
Mathlib.Algebra.Category.ModuleCat.AB
Mathlib.Algebra.Category.ModuleCat.FilteredColimits
Mathlib.Algebra.Homology.ShortComplex.Basic
Mathlib.Algebra.Homology.ShortComplex.Exact
Mathlib.Algebra.Homology.ShortComplex.ShortExact
Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
Mathlib.AlgebraicGeometry.OpenImmersion
Mathlib.AlgebraicGeometry.Properties
Mathlib.AlgebraicGeometry.Sites.AffineEtale
Mathlib.AlgebraicGeometry.Sites.EtalePoint
Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
Mathlib.CategoryTheory.Sites.Point.Conservative

Imported by2

lemma

openClosed_counit_comp_unit

L52 ↗

EtaleCohomology.openClosed_counit_comp_unit

Documentation

The adjunction maps in localization compose to zero.

Source context 6 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits
namespace EtaleCohomology
variable {X Z U : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]
  (i : Z ⟶ X) [IsClosedImmersion i]
  (hcompl : Set.range j = (Set.range i)ᶜ) (R : Type u) [CommRing R]
include hcompl in

Lean source · statement

lemma openClosed_counit_comp_unit
    (G : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)) :
    (etaleExtensionByZeroAdjunction j R).counit.app G ≫
      (etalePullbackPushforwardAdjunction i R).unit.app G = 0

def

openClosedLocalizationComplex

L75 ↗

EtaleCohomology.openClosedLocalizationComplex

Documentation

The canonical three-term complex for an open and its closed complement.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits
namespace EtaleCohomology
variable {X Z U : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]
  (i : Z ⟶ X) [IsClosedImmersion i]
  (hcompl : Set.range j = (Set.range i)ᶜ) (R : Type u) [CommRing R]

Lean source · statement

def openClosedLocalizationComplex
    (G : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)) :
    ShortComplex (Sheaf X.smallEtaleTopology (ModuleCat.{u} R))

lemma

openClosedLocalization_shortExact

L83 ↗

EtaleCohomology.openClosedLocalization_shortExact

Documentation

Open-closed localization is a short exact sequence of étale coefficient sheaves.

Source context 5 commands

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

noncomputable section
universe u
open AlgebraicGeometry CategoryTheory Limits
namespace EtaleCohomology
variable {X Z U : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]
  (i : Z ⟶ X) [IsClosedImmersion i]
  (hcompl : Set.range j = (Set.range i)ᶜ) (R : Type u) [CommRing R]

Lean source · statement

lemma openClosedLocalization_shortExact
    (G : Sheaf X.smallEtaleTopology (ModuleCat.{u} R)) :
    (openClosedLocalizationComplex j i hcompl R G).ShortExact

Module documentation

Open-closed localization for étale coefficient sheaves

Declarations

openClosed_counit_comp_unit

openClosedLocalizationComplex

openClosedLocalization_shortExact