NYLL
Module

IdealPowerTorsionComplexZero.lean

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

Module documentation

Degree zero of the torsion complex of an injective resolution

The inclusion of a module into its injective resolution identifies its power-torsion submodule with the degree-zero torsion cycles. Exactness supplies the preimage of a cycle; injectivity of the inclusion transports its annihilating power back to the original module. This identifies degree-zero homology with the existing local-cohomology colimit.

Imports9
Imported by2

Declarations

def

idealPowerTorsionResolutionCyclesZeroEquiv

L37 ↗
EtaleFundamentalGroups.Purity.idealPowerTorsionResolutionCyclesZeroEquiv
Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u
open CategoryTheory Limits
variable {R : Type u} [CommRing R]
Lean source · statement
def idealPowerTorsionResolutionCyclesZeroEquiv
    (I : Ideal R) {M : ModuleCat.{u} R} (J : InjectiveResolution M) :
    Ideal.primaryComponent M I ≃ₗ[R]
      LinearMap.ker ((derivedLocalCohomologyInjectiveComplex I J).d 0 1).hom
def

derivedLocalCohomologyInjectiveComplexHomologyIsoZero

L102 ↗
EtaleFundamentalGroups.Purity.derivedLocalCohomologyInjectiveComplexHomologyIsoZero
Documentation

The degree-zero homology of the torsion injective-resolution complex is the previously constructed degree-zero local-cohomology module.

Source context 5 commands

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

noncomputable section
namespace EtaleFundamentalGroups.Purity
universe u
open CategoryTheory Limits
variable {R : Type u} [CommRing R]
Lean source · statement
def derivedLocalCohomologyInjectiveComplexHomologyIsoZero
    (I : Ideal R) {M : ModuleCat.{u} R} (J : InjectiveResolution M) :
    (derivedLocalCohomologyInjectiveComplex I J).homology 0 ≅
      derivedLocalCohomologyModule I M 0

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