NYLL
Module

DerivedLocalCohomologyCoefficientAnnihilator.lean

Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologyCoefficientAnnihilator
3 declarations indexed from sourceView source ↗

Module documentation

Coefficient annihilators in local cohomology

A scalar annihilating the coefficients annihilates every local-cohomology class, as is seen on its Ext representative. Along a coefficient short exact sequence, an annihilator of the quotient and an annihilator of the middle local-cohomology group multiply to annihilate the first group. This is the induction step for truncating an injective complex whose intermediate homology modules have scalar annihilators.

Imports5
Imported by2

Declarations

theorem

derivedLocalCohomologyModule_smul_eq_zero_of_coefficients

L36 ↗
EtaleFundamentalGroups.derivedLocalCohomologyModule_smul_eq_zero_of_coefficients
Documentation

A scalar annihilating a coefficient module annihilates its local cohomology with any support, in every degree.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe u
open CategoryTheory Limits Opposite
variable {R : Type u} [CommRing R]
Lean source · statement
theorem derivedLocalCohomologyModule_smul_eq_zero_of_coefficients
    (I : Ideal R) (M : ModuleCat.{u} R) (n : ℕ) (a : R)
    (ha : ∀ m : M, a • m = 0)
    (z : derivedLocalCohomologyModule I M n) : a • z = 0
theorem

derivedLocalCohomologyModule_mul_smul_eq_zero_of_shortExact

L60 ↗
EtaleFundamentalGroups.derivedLocalCohomologyModule_mul_smul_eq_zero_of_shortExact
Documentation

In a coefficient short exact sequence, an annihilator of the last module and an annihilator of the middle cohomology multiply to annihilate the first cohomology.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe u
open CategoryTheory Limits Opposite
variable {R : Type u} [CommRing R]
Lean source · statement
theorem derivedLocalCohomologyModule_mul_smul_eq_zero_of_shortExact
    (I : Ideal R) {S : ShortComplex (ModuleCat.{u} R)} (hS : S.ShortExact)
    (n : ℕ) (a b : R) (ha : ∀ m : S.X₃, a • m = 0)
    (hb : ∀ w : derivedLocalCohomologyModule I S.X₂ (n + 1), b • w = 0)
    (z : derivedLocalCohomologyModule I S.X₁ (n + 1)) :
    (a * b) • z = 0
theorem

derivedLocalCohomologyModule_smul_eq_zero_of_injective_middle

L85 ↗
EtaleFundamentalGroups.derivedLocalCohomologyModule_smul_eq_zero_of_injective_middle
Documentation

For a short exact sequence with injective middle term, an annihilator in degree n of the last coefficient annihilates degree n + 1 of the first coefficient. This is scalar-compatible dimension shifting.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups
universe u
open CategoryTheory Limits Opposite
variable {R : Type u} [CommRing R]
Lean source · statement
theorem derivedLocalCohomologyModule_smul_eq_zero_of_injective_middle
    (I : Ideal R) {S : ShortComplex (ModuleCat.{u} R)} (hS : S.ShortExact)
    [Module.Injective R S.X₂] (n : ℕ) (a : R)
    (ha : ∀ w : derivedLocalCohomologyModule I S.X₃ n, a • w = 0)
    (z : derivedLocalCohomologyModule I S.X₁ (n + 1)) : a • z = 0

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