NYLL
Module

InjectiveChainLocalCohomology.lean

Nyll.EtaleFundamentalGroups.Purity.InjectiveChainLocalCohomology
14 declarations indexed from sourceView source ↗

Module documentation

Local cohomology along an injective chain

The cycle--boundary and boundary--homology short exact sequences are constructed directly from the differentials. Their coefficient sequences allow scalar annihilators to be propagated up the chain.

Imports12
Imported by2

Declarations

def

linearChainCycles

L39 ↗
EtaleFundamentalGroups.Purity.linearChainCycles
Documentation

Concrete cycles in a chain complex of modules.

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 linearChainCycles (K : ChainComplex (ModuleCat.{u} R) ℕ) (n : ℕ) :
    Submodule R (K.X n)
def

linearChainToCycles

L43 ↗
EtaleFundamentalGroups.Purity.linearChainToCycles
Documentation

The incoming differential with its values restricted to cycles.

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 linearChainToCycles (K : ChainComplex (ModuleCat.{u} R) ℕ) (n : ℕ) :
    K.X (n + 1) →ₗ[R] linearChainCycles K n
def

linearChainBoundaries

L48 ↗
EtaleFundamentalGroups.Purity.linearChainBoundaries
Documentation

Concrete boundaries as a submodule of cycles.

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 linearChainBoundaries (K : ChainComplex (ModuleCat.{u} R) ℕ) (n : ℕ) :
    Submodule R (linearChainCycles K n)
def

linearChainBoundaryHomologySequence

L52 ↗
EtaleFundamentalGroups.Purity.linearChainBoundaryHomologySequence
Documentation

The short exact sequence from boundaries to cycles to homology.

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 linearChainBoundaryHomologySequence
    (K : ChainComplex (ModuleCat.{u} R) ℕ) (n : ℕ) :
    ShortComplex (ModuleCat.{u} R)
theorem

linearChainBoundaryHomologySequence_shortExact

L59 ↗
EtaleFundamentalGroups.Purity.linearChainBoundaryHomologySequence_shortExact
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
theorem linearChainBoundaryHomologySequence_shortExact
    (K : ChainComplex (ModuleCat.{u} R) ℕ) (n : ℕ) :
    (linearChainBoundaryHomologySequence K n).ShortExact
theorem

next_chain_nat

L67 ↗
EtaleFundamentalGroups.Purity.next_chain_nat
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
theorem next_chain_nat (n : ℕ) :
    (ComplexShape.down ℕ).next n = n - 1
def

linearChainHomologyIso

L74 ↗
EtaleFundamentalGroups.Purity.linearChainHomologyIso
Documentation

The cycle quotient is the actual homology of the chain complex.

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 linearChainHomologyIso
    (K : ChainComplex (ModuleCat.{u} R) ℕ) (n : ℕ) :
    K.homology n ≅ (linearChainBoundaryHomologySequence K n).X₃
def

linearChainTopHomologyIso

L83 ↗
EtaleFundamentalGroups.Purity.linearChainTopHomologyIso
Documentation

If the incoming chain term is zero, the cycle quotient has no boundaries, so the homology identifies with the actual cycle submodule.

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 linearChainTopHomologyIso
    (K : ChainComplex (ModuleCat.{u} R) ℕ) (n : ℕ)
    (hz : IsZero (K.X (n + 1))) :
    K.homology n ≅ ModuleCat.of R (linearChainCycles K n)
theorem

linearChainCycleBoundary_comp_eq_zero

L96 ↗
EtaleFundamentalGroups.Purity.linearChainCycleBoundary_comp_eq_zero
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
theorem linearChainCycleBoundary_comp_eq_zero
    (K : ChainComplex (ModuleCat.{u} R) ℕ) (n : ℕ) :
    (linearChainToCycles K n).rangeRestrict.comp (linearChainCycles K (n + 1)).subtype = 0
def

linearChainCycleBoundarySequence

L107 ↗
EtaleFundamentalGroups.Purity.linearChainCycleBoundarySequence
Documentation

The short exact sequence from cycles to a chain term to the preceding boundaries.

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 linearChainCycleBoundarySequence
    (K : ChainComplex (ModuleCat.{u} R) ℕ) (n : ℕ) :
    ShortComplex (ModuleCat.{u} R)
theorem

linearChainCycleBoundarySequence_shortExact

L114 ↗
EtaleFundamentalGroups.Purity.linearChainCycleBoundarySequence_shortExact
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
theorem linearChainCycleBoundarySequence_shortExact
    (K : ChainComplex (ModuleCat.{u} R) ℕ) (n : ℕ) :
    (linearChainCycleBoundarySequence K n).ShortExact
theorem

linearChainCycleBoundary_zero_surjective

L130 ↗
EtaleFundamentalGroups.Purity.linearChainCycleBoundary_zero_surjective
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
theorem linearChainCycleBoundary_zero_surjective
    (I : Ideal R) (K : ChainComplex (ModuleCat.{u} R) ℕ)
    (hΓ : Function.Surjective ((idealPowerTorsionFunctor I).map (K.d 1 0))) :
    Function.Surjective (derivedLocalCohomologyModuleCoefficientsSecondMap I
      (linearChainCycleBoundarySequence_shortExact K 0) 0)
theorem

linearChainCycles_localCohomology_one_eq_zero

L161 ↗
EtaleFundamentalGroups.Purity.linearChainCycles_localCohomology_one_eq_zero
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
theorem linearChainCycles_localCohomology_one_eq_zero
    (I : Ideal R) (K : ChainComplex (ModuleCat.{u} R) ℕ)
    [Module.Injective R (K.X 1)]
    (hΓ : Function.Surjective ((idealPowerTorsionFunctor I).map (K.d 1 0)))
    (z : derivedLocalCohomologyModule I (ModuleCat.of R (linearChainCycles K 1)) 1) :
    z = 0
theorem

linearChainCycles_localCohomology_pow_smul_eq_zero

L187 ↗
EtaleFundamentalGroups.Purity.linearChainCycles_localCohomology_pow_smul_eq_zero
Documentation

The lower homology annihilator propagates along an injective chain. Surjectivity of the initial differential on ideal-power torsion supplies the degree-one base case; each subsequent homology term contributes one factor of the scalar.

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
theorem linearChainCycles_localCohomology_pow_smul_eq_zero
    (I : Ideal R) (K : ChainComplex (ModuleCat.{u} R) ℕ)
    [∀ j : ℕ, Module.Injective R (K.X j)]
    (hΓ : Function.Surjective ((idealPowerTorsionFunctor I).map (K.d 1 0)))
    (a : R) (n : ℕ)
    (ha : ∀ i : ℕ, i < n → ∀ h : K.homology (i + 1), a • h = 0)
    (z : derivedLocalCohomologyModule I
      (ModuleCat.of R (linearChainCycles K (n + 1))) (n + 1)) :
    a ^ n • z = 0

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