Module

Localization.lean

Nyll.EtaleCohomology.Classical.Localization

6 declarations indexed from sourceView source ↗

Module documentation

The classical open-closed cohomology sequence

For a closed immersion and its open complement, the localization short exact sequence gives a coefficient-linear long exact sequence

Hⁿ(X, j_!j*F) → Hⁿ(X, F) → Hⁿ(Z, i*F) → Hⁿ⁺¹(X, j_!j*F).

The closed term is the actual classical cohomology of Z, using the proved closed direct-image comparison. All three consecutive pairs are exact. No ground field, noetherian, constructibility, or torsion assumption is used.

Imports9

Imported by1

Nyll.EtaleCohomology.Classical.All

def

etaleOpenExtensionCohomologyMap

L43 ↗

EtaleCohomology.etaleOpenExtensionCohomologyMap

Documentation

The map induced by the counit for extension by zero.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits
universe u
namespace EtaleCohomology
variable {X Z U : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]
  (i : Z ⟶ X) [IsClosedImmersion i] (R : Type u) [CommRing R]
  (F : Sheaf X.smallEtaleTopology (ModuleCat.{u} R))

Lean source · statement

def etaleOpenExtensionCohomologyMap (n : ℕ) :
    etaleCohomology X R
        ((etaleExtensionByZero j R).obj ((etalePullback j R).obj F)) n →ₗ[R]
      etaleCohomology X R F n

def

etaleClosedRestrictionCohomologyMap

L51 ↗

EtaleCohomology.etaleClosedRestrictionCohomologyMap

Documentation

Restriction to the closed subscheme, expressed in its own classical cohomology.

Source context 5 commands

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

noncomputable section
open AlgebraicGeometry CategoryTheory Limits
universe u
namespace EtaleCohomology
variable {X Z U : Scheme.{u}} (j : U ⟶ X) [IsOpenImmersion j]
  (i : Z ⟶ X) [IsClosedImmersion i] (R : Type u) [CommRing R]
  (F : Sheaf X.smallEtaleTopology (ModuleCat.{u} R))

Lean source · statement

def etaleClosedRestrictionCohomologyMap (n : ℕ) :
    etaleCohomology X R F n →ₗ[R]
      etaleCohomology Z R ((etalePullback i R).obj F) n

def

etaleLocalizationConnecting

L62 ↗

EtaleCohomology.etaleLocalizationConnecting

Documentation

The boundary map of open-closed localization, with the closed cohomology term transported along the canonical direct-image comparison.

Source context 6 commands

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

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

Lean source · statement

def etaleLocalizationConnecting (n : ℕ) :
    etaleCohomology Z R ((etalePullback i R).obj F) n →ₗ[R]
      etaleCohomology X R
        ((etaleExtensionByZero j R).obj ((etalePullback j R).obj F)) (n + 1)

lemma

etaleLocalization_exact

L73 ↗

EtaleCohomology.etaleLocalization_exact

Documentation

Exactness at Hⁿ(X,F) in the localization sequence.

Source context 7 commands

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

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

Lean source · statement

lemma etaleLocalization_exact (n : ℕ) :
    Function.Exact (etaleOpenExtensionCohomologyMap j R F n)
      (etaleClosedRestrictionCohomologyMap i R F n)

lemma

etaleLocalization_exact_connecting

L85 ↗

EtaleCohomology.etaleLocalization_exact_connecting

Documentation

Exactness at Hⁿ(Z,i*F) in the localization sequence.

Source context 6 commands

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

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

Lean source · statement

lemma etaleLocalization_exact_connecting (n : ℕ) :
    Function.Exact (etaleClosedRestrictionCohomologyMap i R F n)
      (etaleLocalizationConnecting j i R F hcompl n)

lemma

etaleLocalization_connecting_exact

L97 ↗

EtaleCohomology.etaleLocalization_connecting_exact

Documentation

Exactness at Hⁿ⁺¹(X,j_!j*F) in the localization sequence.

Source context 6 commands

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

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

Lean source · statement

lemma etaleLocalization_connecting_exact (n : ℕ) :
    Function.Exact (etaleLocalizationConnecting j i R F hcompl n)
      (etaleOpenExtensionCohomologyMap j R F (n + 1))

Module documentation

The classical open-closed cohomology sequence

Declarations

etaleOpenExtensionCohomologyMap

etaleClosedRestrictionCohomologyMap

etaleLocalizationConnecting

etaleLocalization_exact

etaleLocalization_exact_connecting

etaleLocalization_connecting_exact