NYLL
Module

DerivedLocalCohomologyPowerTorsionAcyclic.lean

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

Module documentation

Acyclicity of ideal-power torsion coefficients

Positive-degree local cohomology vanishes on injective coefficients, because every derived Ext group in its defining diagram vanishes. An ideal-power torsion module over a Noetherian ring has an injective presentation whose middle and quotient terms remain ideal-power torsion.

In degree one, the degree-zero coefficient map is surjective, so the connecting map is both zero and an epimorphism. In higher degrees, induction on the quotient term and injectivity of the middle term give the vanishing through the same connecting epimorphism.

Imports8
Imported by7

Declarations

theorem

derivedLocalCohomology_isZero_succ_of_injective

L40 ↗
EtaleFundamentalGroups.derivedLocalCohomology_isZero_succ_of_injective
Documentation

Positive-degree derived local cohomology of an injective coefficient module vanishes termwise in its defining Ext diagram.

Source context 4 commands

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

namespace EtaleFundamentalGroups
universe u
open CategoryTheory Limits
variable {R : Type u} [CommRing R]
Lean source · statement
theorem derivedLocalCohomology_isZero_succ_of_injective
    (I : Ideal R) (M : ModuleCat.{u} R) [Module.Injective R M] (n : ℕ) :
    IsZero (derivedLocalCohomology I M (n + 1))
theorem

derivedLocalCohomology_isZero_succ_of_power_torsion

L52 ↗
EtaleFundamentalGroups.derivedLocalCohomology_isZero_succ_of_power_torsion
Documentation

Ideal-power torsion coefficient modules over a Noetherian ring have zero derived local cohomology in every positive degree.

Source context 4 commands

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

namespace EtaleFundamentalGroups
universe u
open CategoryTheory Limits
variable {R : Type u} [CommRing R]
Lean source · statement
theorem derivedLocalCohomology_isZero_succ_of_power_torsion
    [IsNoetherianRing R] (I : Ideal R) (M : ModuleCat.{u} R)
    (hM : ∀ z : M, ∃ k : ℕ, ∀ a ∈ I ^ k, a • z = 0) (n : ℕ) :
    IsZero (derivedLocalCohomology I M (n + 1))

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