NYLL
Module

DerivedLocalCohomologyDegreeZeroCoefficients.lean

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

Module documentation

Degree-zero coefficient maps on power-torsion modules

Evaluation of degree-zero local cohomology commutes with the second coefficient map. When the middle coefficient module is ideal-power torsion, its evaluation map is surjective. Exactness of the coefficient sequence and injectivity of evaluation on the last module then imply surjectivity of the degree-zero local-cohomology coefficient map.

Imports8
Imported by4

Declarations

theorem

derivedLocalCohomologyZeroToModule_comp_secondMap

L37 ↗
EtaleFundamentalGroups.derivedLocalCohomologyZeroToModule_comp_secondMap
Documentation

Degree-zero evaluation commutes with the second coefficient map.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
variable {R : Type u} [CommRing R]
Lean source · statement
theorem derivedLocalCohomologyZeroToModule_comp_secondMap
    (I : Ideal R) {S : ShortComplex (ModuleCat.{u} R)} (hS : S.ShortExact) :
    (derivedLocalCohomologyZeroToModule I S.X₃).comp
        (derivedLocalCohomologyModuleCoefficientsSecondMap I hS 0) =
      S.g.hom.comp (derivedLocalCohomologyZeroToModule I S.X₂)
theorem

derivedLocalCohomologyModuleCoefficientsSecondMap_surjective_zero_of_power_torsion

L70 ↗
EtaleFundamentalGroups.derivedLocalCohomologyModuleCoefficientsSecondMap_surjective_zero_of_power_torsion
Documentation

A surjective coefficient map with ideal-power torsion source induces a surjection in degree-zero local cohomology.

Source context 5 commands

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

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

derivedLocalCohomologyCoefficientsSecondMap_epi_zero_of_power_torsion

L89 ↗
EtaleFundamentalGroups.derivedLocalCohomologyCoefficientsSecondMap_epi_zero_of_power_torsion
Documentation

The same degree-zero surjection expressed in the additive-group category used by the coefficient long exact sequence.

Source context 5 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
variable {R : Type u} [CommRing R]
Lean source · statement
theorem derivedLocalCohomologyCoefficientsSecondMap_epi_zero_of_power_torsion
    (I : Ideal R) {S : ShortComplex (ModuleCat.{u} R)} (hS : S.ShortExact)
    (hT : ∀ z : S.X₂, ∃ n : ℕ, ∀ a ∈ I ^ n, a • z = 0) :
    Epi (derivedLocalCohomologyCoefficientsSecondMap I hS 0)

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