NYLL
Module

DerivedLocalCohomologyDimensionShift.lean

Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologyDimensionShift
2 declarations indexed from sourceView source ↗

Module documentation

Dimension shifting for derived local cohomology

The coefficient connecting map is surjective when the middle module is injective, and bijective when its source cohomology degree is positive. These are consequences of the actual coefficient long exact sequence and vanishing of positive Ext groups for injective modules.

Imports4
Imported by2

Declarations

theorem

derivedLocalCohomologyConnecting_surjective_of_injective

L30 ↗
EtaleFundamentalGroups.Purity.derivedLocalCohomologyConnecting_surjective_of_injective
Documentation

Injective middle coefficients make every connecting map surjective.

Source context 4 commands

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

namespace EtaleFundamentalGroups.Purity
universe u
open CategoryTheory
variable {R : Type u} [CommRing R]
Lean source · statement
theorem derivedLocalCohomologyConnecting_surjective_of_injective
    (I : Ideal R) {S : ShortComplex (ModuleCat.{u} R)} (hS : S.ShortExact)
    [Module.Injective R S.X₂] (n : ℕ) :
    Function.Surjective (derivedLocalCohomologyModuleCoefficientsConnectingMap I hS n)
theorem

derivedLocalCohomologyConnecting_bijective_succ_of_injective

L42 ↗
EtaleFundamentalGroups.Purity.derivedLocalCohomologyConnecting_bijective_succ_of_injective
Documentation

In positive source degree the same connecting map is also injective.

Source context 4 commands

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

namespace EtaleFundamentalGroups.Purity
universe u
open CategoryTheory
variable {R : Type u} [CommRing R]
Lean source · statement
theorem derivedLocalCohomologyConnecting_bijective_succ_of_injective
    (I : Ideal R) {S : ShortComplex (ModuleCat.{u} R)} (hS : S.ShortExact)
    [Module.Injective R S.X₂] (n : ℕ) :
    Function.Bijective
      (derivedLocalCohomologyModuleCoefficientsConnectingMap I hS (n + 1))

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