Module

LocalCohomologyExtVanishing.lean

Nyll.EtaleFundamentalGroups.Purity.LocalCohomologyExtVanishing

1 declaration indexed from sourceView source ↗

Module documentation

Local-cohomology vanishing from Ext vanishing

Local cohomology is defined as a colimit of Ext modules. This file records the categorical passage from pointwise vanishing of the Ext diagram to vanishing of the resulting local-cohomology module.

Imports2

Mathlib.Algebra.Homology.LocalCohomology
Mathlib.CategoryTheory.Limits.FunctorCategory.Basic

Imported by3

theorem

localCohomology_isZero_of_subsingleton_ext_powers

L28 ↗

EtaleFundamentalGroups.localCohomology_isZero_of_subsingleton_ext_powers

Documentation

A local-cohomology module vanishes if every Ext module in its defining ideal-powers diagram vanishes.

Source context 4 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u

Lean source · statement

theorem localCohomology_isZero_of_subsingleton_ext_powers
    {R : Type u} [CommRing R] (I : Ideal R) (M : ModuleCat.{u} R) (i : ℕ)
    (hExt : ∀ n : ℕ, Subsingleton
      (((_root_.Ext R (ModuleCat.{u} R) i).obj
        (op (ModuleCat.of R (R ⧸ I ^ n)))).obj M)) :
    IsZero ((localCohomology I i).obj M)

Module documentation

Local-cohomology vanishing from Ext vanishing

Declarations

localCohomology_isZero_of_subsingleton_ext_powers