NYLL
Module

CechLocalCohomology.lean

Nyll.EtaleFundamentalGroups.Purity.CechLocalCohomology
10 declarations indexed from sourceView source ↗

Module documentation

Čech cohomology and derived local cohomology

The natural degree-zero inclusion identifies Čech cohomology with ideal power torsion. This is first checked on injectives using the actual contraction, then descended along an injective presentation by exactness. The coefficient long exact sequences give the comparison in positive degrees by dimension shifting.

Imports9
Imported by2

Declarations

abbrev

cechCoefficients

L37 ↗
EtaleFundamentalGroups.Purity.cechCoefficients
Source context 5 commands

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

noncomputable section
open CategoryTheory Limits MonoidalCategory HomologicalComplex
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R] [IsNoetherianRing R]
Lean source · statement
abbrev cechCoefficients (xs : List R) (M : ModuleCat.{u} R)
theorem

cechHomologyZero_range_injective

L41 ↗
EtaleFundamentalGroups.Purity.cechHomologyZero_range_injective
Source context 5 commands

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

noncomputable section
open CategoryTheory Limits MonoidalCategory HomologicalComplex
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R] [IsNoetherianRing R]
Lean source · statement
theorem cechHomologyZero_range_injective
    (xs : List R) (M : ModuleCat.{u} R) [Module.Injective R M] :
    LinearMap.range (cechHomologyZeroToModule xs M).hom =
      Ideal.primaryComponent M (Ideal.ofList xs)
theorem

cechHomologyZeroToModule_range

L89 ↗
EtaleFundamentalGroups.Purity.cechHomologyZeroToModule_range
Documentation

The natural degree-zero Čech embedding has exactly the expected ideal-power torsion image for every coefficient module.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits MonoidalCategory HomologicalComplex
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R] [IsNoetherianRing R]
Lean source · statement
theorem cechHomologyZeroToModule_range (xs : List R) (M : ModuleCat.{u} R) :
    LinearMap.range (cechHomologyZeroToModule xs M).hom =
      Ideal.primaryComponent M (Ideal.ofList xs)
def

cechHomologyZeroEquivPrimaryComponent

L151 ↗
EtaleFundamentalGroups.Purity.cechHomologyZeroEquivPrimaryComponent
Source context 5 commands

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

noncomputable section
open CategoryTheory Limits MonoidalCategory HomologicalComplex
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R] [IsNoetherianRing R]
Lean source · statement
def cechHomologyZeroEquivPrimaryComponent (xs : List R) (M : ModuleCat.{u} R) :
    (cechCoefficients xs M).homology 0 ≃ₗ[R]
      Ideal.primaryComponent M (Ideal.ofList xs)
def

cechLocalCohomologyZeroEquiv

L170 ↗
EtaleFundamentalGroups.Purity.cechLocalCohomologyZeroEquiv
Source context 5 commands

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

noncomputable section
open CategoryTheory Limits MonoidalCategory HomologicalComplex
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R] [IsNoetherianRing R]
Lean source · statement
def cechLocalCohomologyZeroEquiv (xs : List R) (M : ModuleCat.{u} R) :
    (cechCoefficients xs M).homology 0 ≃ₗ[R]
      derivedLocalCohomologyModule (Ideal.ofList xs) M 0
theorem

cechLocalCohomologyZeroEquiv_eval

L176 ↗
EtaleFundamentalGroups.Purity.cechLocalCohomologyZeroEquiv_eval
Source context 5 commands

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

noncomputable section
open CategoryTheory Limits MonoidalCategory HomologicalComplex
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R] [IsNoetherianRing R]
Lean source · statement
theorem cechLocalCohomologyZeroEquiv_eval (xs : List R) (M : ModuleCat.{u} R)
    (z : (cechCoefficients xs M).homology 0) :
    derivedLocalCohomologyZeroToModule (Ideal.ofList xs) M
      (cechLocalCohomologyZeroEquiv xs M z) = (cechHomologyZeroToModule xs M) z
theorem

cechLocalCohomologyZeroEquiv_secondMap

L192 ↗
EtaleFundamentalGroups.Purity.cechLocalCohomologyZeroEquiv_secondMap
Source context 5 commands

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

noncomputable section
open CategoryTheory Limits MonoidalCategory HomologicalComplex
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R] [IsNoetherianRing R]
Lean source · statement
theorem cechLocalCohomologyZeroEquiv_secondMap
    (xs : List R) {S : ShortComplex (ModuleCat.{u} R)} (hS : S.ShortExact) :
    (cechLocalCohomologyZeroEquiv xs S.X₃).toLinearMap.comp
      (homologyMap ((tensorComplexCoefficientFunctor (cechLocalizationComplex xs)).map S.g) 0).hom =
      (derivedLocalCohomologyModuleCoefficientsSecondMap (Ideal.ofList xs) hS 0).comp
        (cechLocalCohomologyZeroEquiv xs S.X₂).toLinearMap
theorem

cechCoefficients_isZero_homology_succ

L221 ↗
EtaleFundamentalGroups.Purity.cechCoefficients_isZero_homology_succ
Source context 5 commands

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

noncomputable section
open CategoryTheory Limits MonoidalCategory HomologicalComplex
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R] [IsNoetherianRing R]
Lean source · statement
theorem cechCoefficients_isZero_homology_succ
    (xs : List R) (M : ModuleCat.{u} R) [Module.Injective R M] (n : ℕ) :
    IsZero ((cechCoefficients xs M).homology (n + 1))
def

cechLocalCohomologyOneEquiv

L229 ↗
EtaleFundamentalGroups.Purity.cechLocalCohomologyOneEquiv
Source context 5 commands

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

noncomputable section
open CategoryTheory Limits MonoidalCategory HomologicalComplex
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R] [IsNoetherianRing R]
Lean source · statement
def cechLocalCohomologyOneEquiv
    (xs : List R) {S : ShortComplex (ModuleCat.{u} R)} (hS : S.ShortExact)
    [Module.Injective R S.X₂] :
    (cechCoefficients xs S.X₁).homology 1 ≃ₗ[R]
      derivedLocalCohomologyModule (Ideal.ofList xs) S.X₁ 1
def

cechLocalCohomologyLinearEquiv

L267 ↗
EtaleFundamentalGroups.Purity.cechLocalCohomologyLinearEquiv
Documentation

The actual bounded Čech complex computes derived local cohomology, with a linear comparison in every degree and for every coefficient module.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits MonoidalCategory HomologicalComplex
namespace EtaleFundamentalGroups.Purity
universe u
variable {R : Type u} [CommRing R] [IsNoetherianRing R]
Lean source · statement
def cechLocalCohomologyLinearEquiv (xs : List R) (M : ModuleCat.{u} R) (n : ℕ) :
    ((((tensorLeft M).mapHomologicalComplex (ComplexShape.up ℕ)).obj
      (cechLocalizationComplex xs)).homology n) ≃ₗ[R]
        derivedLocalCohomologyModule (Ideal.ofList xs) M n

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