NYLL
Module

DerivedLocalCohomologyTorsionQuotient.lean

Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologyTorsionQuotient
5 declarations indexed from sourceView source ↗

Module documentation

Removing ideal-power torsion from coefficient modules

Degree-zero local cohomology has image equal to the primary component of the coefficient module. In a short exact coefficient sequence whose first term is ideal-power torsion, the positive-degree second maps are linear equivalences, since both neighboring cohomology groups vanish.

Imports11
Imported by5

Declarations

theorem

range_derivedLocalCohomologyZeroToModule

L40 ↗
EtaleFundamentalGroups.range_derivedLocalCohomologyZeroToModule
Documentation

The degree-zero evaluation image is the primary component for the support ideal.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits
namespace EtaleFundamentalGroups
universe u
variable {R : Type u} [CommRing R]
Lean source · statement
theorem range_derivedLocalCohomologyZeroToModule
    (I : Ideal R) (M : ModuleCat.{u} R) :
    LinearMap.range (derivedLocalCohomologyZeroToModule I M) =
      Ideal.primaryComponent M I
def

derivedLocalCohomologyZeroEquivPrimaryComponent

L51 ↗
EtaleFundamentalGroups.derivedLocalCohomologyZeroEquivPrimaryComponent
Documentation

Evaluation identifies degree-zero local cohomology with the concrete ideal-primary component of its coefficient module.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits
namespace EtaleFundamentalGroups
universe u
variable {R : Type u} [CommRing R]
Lean source · statement
def derivedLocalCohomologyZeroEquivPrimaryComponent
    (I : Ideal R) (M : ModuleCat.{u} R) :
    derivedLocalCohomologyModule I M 0 ≃ₗ[R] Ideal.primaryComponent M I
theorem

derivedLocalCohomologyZeroEquivPrimaryComponent_apply_val

L71 ↗
EtaleFundamentalGroups.derivedLocalCohomologyZeroEquivPrimaryComponent_apply_val
Documentation

The degree-zero equivalence retains the original evaluation map.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits
namespace EtaleFundamentalGroups
universe u
variable {R : Type u} [CommRing R]
Lean source · statement
theorem derivedLocalCohomologyZeroEquivPrimaryComponent_apply_val
    (I : Ideal R) (M : ModuleCat.{u} R)
    (z : derivedLocalCohomologyModule I M 0) :
    (derivedLocalCohomologyZeroEquivPrimaryComponent I M z : M) =
      derivedLocalCohomologyZeroToModule I M z
theorem

derivedLocalCohomologyModuleCoefficientsSecondMap_bijective_succ_of_power_torsion

L80 ↗
EtaleFundamentalGroups.derivedLocalCohomologyModuleCoefficientsSecondMap_bijective_succ_of_power_torsion
Documentation

Removing an ideal-power torsion first coefficient term induces a bijection in every positive cohomological degree.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits
namespace EtaleFundamentalGroups
universe u
variable {R : Type u} [CommRing R]
Lean source · statement
theorem derivedLocalCohomologyModuleCoefficientsSecondMap_bijective_succ_of_power_torsion
    [IsNoetherianRing R]
    (I : Ideal R) {S : ShortComplex (ModuleCat.{u} R)} (hS : S.ShortExact)
    (hT : ∀ z : S.X₁, ∃ k : ℕ, ∀ a ∈ I ^ k, a • z = 0) (n : ℕ) :
    Function.Bijective (derivedLocalCohomologyModuleCoefficientsSecondMap I hS (n + 1))
def

derivedLocalCohomologyModuleCoefficientsSecondEquiv_succ_of_power_torsion

L96 ↗
EtaleFundamentalGroups.derivedLocalCohomologyModuleCoefficientsSecondEquiv_succ_of_power_torsion
Documentation

The linear equivalence on positive-degree local cohomology obtained after removing ideal-power torsion coefficients.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits
namespace EtaleFundamentalGroups
universe u
variable {R : Type u} [CommRing R]
Lean source · statement
def derivedLocalCohomologyModuleCoefficientsSecondEquiv_succ_of_power_torsion
    [IsNoetherianRing R]
    (I : Ideal R) {S : ShortComplex (ModuleCat.{u} R)} (hS : S.ShortExact)
    (hT : ∀ z : S.X₁, ∃ k : ℕ, ∀ a ∈ I ^ k, a • z = 0) (n : ℕ) :
    derivedLocalCohomologyModule I S.X₂ (n + 1) ≃ₗ[R]
      derivedLocalCohomologyModule I S.X₃ (n + 1)

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