NYLL
Module

DerivedLocalCohomologyTorsionFreeQuotient.lean

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

Module documentation

Local cohomology after removing the primary component

The quotient by the maximal-ideal-primary component has zero degree-zero local cohomology: evaluation is injective, and every value is a power-torsion vector in a quotient containing no such nonzero vector. In positive degrees the inclusion of the primary component and its quotient give a concrete linear equivalence through the coefficient long exact sequence.

Imports7
Imported by3

Declarations

theorem

derivedLocalCohomology_maximalIdeal_isZero_zero_quotient_primaryComponent

L35 ↗
EtaleFundamentalGroups.derivedLocalCohomology_maximalIdeal_isZero_zero_quotient_primaryComponent
Documentation

Removing the maximal-ideal-primary component of a finite coefficient module makes its degree-zero maximal-support local cohomology vanish.

Source context 4 commands

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

namespace EtaleFundamentalGroups
universe u
open CategoryTheory Limits IsLocalRing
variable {R : Type u} [CommRing R] [IsNoetherianRing R]
Lean source · statement
theorem derivedLocalCohomology_maximalIdeal_isZero_zero_quotient_primaryComponent
    [IsLocalRing R] (M : ModuleCat.{u} R) [Module.Finite R M] :
    IsZero (derivedLocalCohomology (maximalIdeal R)
      (ModuleCat.of R (M ⧸ Ideal.primaryComponent M (maximalIdeal R))) 0)
def

derivedLocalCohomologyModuleEquiv_succ_quotient_primaryComponent

L55 ↗
EtaleFundamentalGroups.derivedLocalCohomologyModuleEquiv_succ_quotient_primaryComponent
Documentation

Quotienting by the ideal-primary component preserves all positive degrees of local cohomology, via the concrete coefficient quotient map.

Source context 4 commands

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

namespace EtaleFundamentalGroups
universe u
open CategoryTheory Limits IsLocalRing
variable {R : Type u} [CommRing R] [IsNoetherianRing R]
Lean source · statement
def derivedLocalCohomologyModuleEquiv_succ_quotient_primaryComponent
    (I : Ideal R) (M : ModuleCat.{u} R) (n : ℕ) :
    derivedLocalCohomologyModule I M (n + 1) ≃ₗ[R]
      derivedLocalCohomologyModule I
        (ModuleCat.of R (M ⧸ Ideal.primaryComponent M I)) (n + 1)

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