NYLL
Module

DerivedLocalCohomologyScalarKernelArtinian.lean

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

Module documentation

Artinianness from a regular coefficient quotient

For a scalar regular on the coefficient module, the connecting map from the preceding cohomology of its quotient has image equal to the scalar kernel on the next local-cohomology module. Artinianness of that quotient cohomology therefore makes the scalar kernel Artinian. The actual ideal-power torsion of local cohomology then proves Artinianness over a complete Noetherian local ring.

Imports11
Imported by2

Declarations

theorem

isArtinian_derivedLocalCohomologyModule_succ_of_regular_smulQuotient

L42 ↗
EtaleFundamentalGroups.Purity.isArtinian_derivedLocalCohomologyModule_succ_of_regular_smulQuotient
Documentation

If a scalar in the maximal ideal is regular on the coefficients, Artinianness in degree n of the coefficient quotient implies Artinianness in degree n + 1 of the original coefficients.

Source context 5 commands

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

namespace EtaleFundamentalGroups.Purity
universe u
open IsLocalRing
variable {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R]
variable [IsAdicComplete (maximalIdeal R) R]
Lean source · statement
theorem isArtinian_derivedLocalCohomologyModule_succ_of_regular_smulQuotient
    (M : ModuleCat.{u} R) (x : R) (hx : x ∈ maximalIdeal R)
    (hxreg : IsSMulRegular M x) (n : ℕ)
    [IsArtinian R (derivedLocalCohomologyModule (maximalIdeal R)
      (ModuleCat.smulShortComplex M x).X₃ n)] :
    IsArtinian R (derivedLocalCohomologyModule (maximalIdeal R) 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.