NYLL
Module

DerivedLocalCohomologyFiniteTorsionFreeDescent.lean

Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologyFiniteTorsionFreeDescent
1 declaration indexed from sourceView source ↗

Module documentation

Detecting top local cohomology with a finite torsion-free module

A nonzero functional on a finite torsion-free module has a nonzero ideal as its image. The kernel has dimension at most that of the ring, whereas the quotient by the image has strictly smaller dimension. The two actual short exact sequences therefore transfer top-degree vanishing to the ring.

Imports19
Imported by2

Declarations

theorem

derivedLocalCohomology_isZero_ring_of_finite_torsionFree

L49 ↗
EtaleFundamentalGroups.derivedLocalCohomology_isZero_ring_of_finite_torsionFree
Documentation

Top-degree vanishing for a finite nonzero torsion-free module over a Noetherian local domain implies the same vanishing for the ring, for any support ideal.

Source context 6 commands

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

namespace EtaleFundamentalGroups
open CategoryTheory Limits
open scoped nonZeroDivisors
universe u
variable {R : Type u} [CommRing R] [IsDomain R]
variable [IsLocalRing R] [IsNoetherianRing R]
Lean source · statement
theorem derivedLocalCohomology_isZero_ring_of_finite_torsionFree
    (I : Ideal R) (K : ModuleCat.{u} R)
    [Module.Finite R K] [Module.IsTorsionFree R K] [Nontrivial K]
    (d : ℕ) (hdim : ringKrullDim R = (d : WithBot ℕ∞))
    (hK : IsZero (derivedLocalCohomology I K d)) :
    IsZero (derivedLocalCohomology I (ModuleCat.of R R) d)

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