NYLL
Module

PowerTorsionEssentialKernel.lean

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

Module documentation

Essential scalar kernels in power-torsion modules

If every element of a module is killed by a power of a scalar, the kernel of multiplication by that scalar is essential. On a submodule disjoint from the kernel, induction on the annihilating exponent forces every element to be zero. Local cohomology supplies the required power torsion for each scalar in its support ideal.

Imports4
Imported by1

Declarations

theorem

isEssentialSubmodule_ker_smul_of_power_torsion

L30 ↗
EtaleFundamentalGroups.Purity.isEssentialSubmodule_ker_smul_of_power_torsion
Documentation

The scalar kernel is essential when each element is killed by some power of that scalar.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Purity
universe u v
variable {R : Type u} [CommRing R]
Lean source · statement
theorem isEssentialSubmodule_ker_smul_of_power_torsion
    {M : Type v} [AddCommGroup M] [Module R M]
    (x : R) (hM : ∀ m : M, ∃ n : ℕ, x ^ n • m = 0) :
    IsEssentialSubmodule
      (LinearMap.ker (x • (LinearMap.id : M →ₗ[R] M)))
theorem

isEssentialSubmodule_ker_smul_derivedLocalCohomologyModule

L58 ↗
EtaleFundamentalGroups.Purity.isEssentialSubmodule_ker_smul_derivedLocalCohomologyModule
Documentation

A scalar in the support ideal has essential kernel on the actual derived local-cohomology module.

Source context 3 commands

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

namespace EtaleFundamentalGroups.Purity
universe u v
variable {R : Type u} [CommRing R]
Lean source · statement
theorem isEssentialSubmodule_ker_smul_derivedLocalCohomologyModule
    (I : Ideal R) (M : ModuleCat.{u} R) (i : ℕ) (x : R) (hx : x ∈ I) :
    IsEssentialSubmodule
      (LinearMap.ker
        (x • (LinearMap.id : derivedLocalCohomologyModule I M i →ₗ[R]
          derivedLocalCohomologyModule I M i)))

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