NYLL
Module

DerivedLocalCohomologyPrincipalAnnihilated.lean

Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologyPrincipalAnnihilated
13 declarations indexed from sourceView source ↗

Module documentation

Principal support on an annihilated coefficient module

The coefficient long exact sequence immediately supplies mono/epi criteria when one of its neighboring terms vanishes. The main result of this file is a source-level vanishing theorem: if x annihilates a module M, then degree one local cohomology of M supported at (x) vanishes.

The proof works directly in the ideal-powers Ext diagram. Every degree-one class against R / (x)^n is the boundary of a map (x)^n → M, because R is projective. On restriction to (x)^(n+1), that map is zero: every element of the latter ideal is x times an element of (x)^n, and xM = 0. Naturality of extension classes therefore says that the transition from the n-th to the (n+1)-st power kills every class.

Imports5
Imported by7

Declarations

theorem

derivedLocalCohomologyCoefficientsSecondMap_mono_of_first_isZero

L43 ↗
EtaleFundamentalGroups.derivedLocalCohomologyCoefficientsSecondMap_mono_of_first_isZero
Documentation

If the first coefficient term vanishes in degree n, the second coefficient map is a monomorphism.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
section CoefficientExactnessCorollaries
variable {R : Type u} [CommRing R]
Lean source · statement
theorem derivedLocalCohomologyCoefficientsSecondMap_mono_of_first_isZero
    (I : Ideal R) {S : ShortComplex (ModuleCat.{u} R)} (hS : S.ShortExact)
    (n : ℕ) (hzero : IsZero (derivedLocalCohomology I S.X₁ n)) :
    Mono (derivedLocalCohomologyCoefficientsSecondMap I hS n)
theorem

derivedLocalCohomologyCoefficientsFirstMap_epi_of_third_isZero

L52 ↗
EtaleFundamentalGroups.derivedLocalCohomologyCoefficientsFirstMap_epi_of_third_isZero
Documentation

If the third coefficient term vanishes in degree n, the first coefficient map is an epimorphism.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
section CoefficientExactnessCorollaries
variable {R : Type u} [CommRing R]
Lean source · statement
theorem derivedLocalCohomologyCoefficientsFirstMap_epi_of_third_isZero
    (I : Ideal R) {S : ShortComplex (ModuleCat.{u} R)} (hS : S.ShortExact)
    (n : ℕ) (hzero : IsZero (derivedLocalCohomology I S.X₃ n)) :
    Epi (derivedLocalCohomologyCoefficientsFirstMap I hS n)
theorem

derivedLocalCohomologyCoefficientsSecondMap_epi_of_next_first_isZero

L61 ↗
EtaleFundamentalGroups.derivedLocalCohomologyCoefficientsSecondMap_epi_of_next_first_isZero
Documentation

If the next first coefficient term vanishes, the second coefficient map is an epimorphism.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
section CoefficientExactnessCorollaries
variable {R : Type u} [CommRing R]
Lean source · statement
theorem derivedLocalCohomologyCoefficientsSecondMap_epi_of_next_first_isZero
    (I : Ideal R) {S : ShortComplex (ModuleCat.{u} R)} (hS : S.ShortExact)
    (n : ℕ) (hzero : IsZero (derivedLocalCohomology I S.X₁ (n + 1))) :
    Epi (derivedLocalCohomologyCoefficientsSecondMap I hS n)
theorem

derivedLocalCohomologyCoefficientsConnectingMap_mono_of_middle_isZero

L70 ↗
EtaleFundamentalGroups.derivedLocalCohomologyCoefficientsConnectingMap_mono_of_middle_isZero
Documentation

If the middle coefficient term vanishes in degree n, the connecting map out of degree n is a monomorphism.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
section CoefficientExactnessCorollaries
variable {R : Type u} [CommRing R]
Lean source · statement
theorem derivedLocalCohomologyCoefficientsConnectingMap_mono_of_middle_isZero
    (I : Ideal R) {S : ShortComplex (ModuleCat.{u} R)} (hS : S.ShortExact)
    (n : ℕ) (hzero : IsZero (derivedLocalCohomology I S.X₂ n)) :
    Mono (derivedLocalCohomologyCoefficientsConnectingMap I hS n)
theorem

derivedLocalCohomologyCoefficientsConnectingMap_epi_of_next_middle_isZero

L79 ↗
EtaleFundamentalGroups.derivedLocalCohomologyCoefficientsConnectingMap_epi_of_next_middle_isZero
Documentation

If the next middle coefficient term vanishes, the connecting map into the next degree is an epimorphism.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
section CoefficientExactnessCorollaries
variable {R : Type u} [CommRing R]
Lean source · statement
theorem derivedLocalCohomologyCoefficientsConnectingMap_epi_of_next_middle_isZero
    (I : Ideal R) {S : ShortComplex (ModuleCat.{u} R)} (hS : S.ShortExact)
    (n : ℕ) (hzero : IsZero (derivedLocalCohomology I S.X₂ (n + 1))) :
    Epi (derivedLocalCohomologyCoefficientsConnectingMap I hS n)
theorem

derivedLocalCohomologyCoefficientsFirstMap_mono_of_previous_third_isZero

L88 ↗
EtaleFundamentalGroups.derivedLocalCohomologyCoefficientsFirstMap_mono_of_previous_third_isZero
Documentation

If the previous third coefficient term vanishes, the first coefficient map in the next degree is a monomorphism.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
section CoefficientExactnessCorollaries
variable {R : Type u} [CommRing R]
Lean source · statement
theorem derivedLocalCohomologyCoefficientsFirstMap_mono_of_previous_third_isZero
    (I : Ideal R) {S : ShortComplex (ModuleCat.{u} R)} (hS : S.ShortExact)
    (n : ℕ) (hzero : IsZero (derivedLocalCohomology I S.X₃ n)) :
    Mono (derivedLocalCohomologyCoefficientsFirstMap I hS (n + 1))
def

principalIdealPowerQuotientShortComplex

L103 ↗
EtaleFundamentalGroups.principalIdealPowerQuotientShortComplex
Documentation

The tautological short exact complex (x)^n → R → R / (x)^n.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
section PrincipalAnnihilated
variable {R : Type u} [CommRing R]
Lean source · statement
def principalIdealPowerQuotientShortComplex (x : R) (n : ℕ) :
    ShortComplex (ModuleCat.{u} R)
theorem

principalIdealPowerQuotientShortComplex_shortExact

L112 ↗
EtaleFundamentalGroups.principalIdealPowerQuotientShortComplex_shortExact
Documentation

The tautological principal-power quotient complex is short exact.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
section PrincipalAnnihilated
variable {R : Type u} [CommRing R]
Lean source · statement
theorem principalIdealPowerQuotientShortComplex_shortExact
    (x : R) (n : ℕ) :
    (principalIdealPowerQuotientShortComplex x n).ShortExact
def

principalIdealPowerQuotientShortComplexSuccTransition

L122 ↗
EtaleFundamentalGroups.principalIdealPowerQuotientShortComplexSuccTransition
Documentation

The natural morphism from the (n+1)-st principal-power quotient complex to the n-th one.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
section PrincipalAnnihilated
variable {R : Type u} [CommRing R]
Lean source · full declaration
def principalIdealPowerQuotientShortComplexSuccTransition
    (x : R) (n : ℕ) :
    principalIdealPowerQuotientShortComplex x (n + 1) ⟶
      principalIdealPowerQuotientShortComplex x n where
  τ₁ := ModuleCat.ofHom (Submodule.inclusion
    (Ideal.pow_le_pow_right (Nat.le_succ n)))
  τ₂ := 𝟙 _
  τ₃ := ModuleCat.ofHom
    (principalPowerQuotientTransition x (Nat.le_succ n))
  comm₁₂ := by
    ext
    rfl
  comm₂₃ := by
    ext
    rfl
theorem

principalIdealPower_succ_inclusion_comp_linear_eq_zero

L140 ↗
EtaleFundamentalGroups.principalIdealPower_succ_inclusion_comp_linear_eq_zero
Documentation

On underlying linear maps, a map (x)^n → M restricts to zero on (x)^(n+1) when x annihilates M.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
section PrincipalAnnihilated
variable {R : Type u} [CommRing R]
Lean source · statement
theorem principalIdealPower_succ_inclusion_comp_linear_eq_zero
    (x : R) (M : ModuleCat.{u} R) (hx : x • 𝟙 M = 0)
    (n : ℕ)
    (b : ((Ideal.span {x}) ^ n : Ideal R) →ₗ[R] M) :
    b.comp (Submodule.inclusion
      (Ideal.pow_le_pow_right (Nat.le_succ n))) = 0
theorem

principalIdealPower_succ_inclusion_comp_eq_zero

L174 ↗
EtaleFundamentalGroups.principalIdealPower_succ_inclusion_comp_eq_zero
Documentation

A map (x)^n → M restricts to zero on (x)^(n+1) when x annihilates M.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
section PrincipalAnnihilated
variable {R : Type u} [CommRing R]
Lean source · statement
theorem principalIdealPower_succ_inclusion_comp_eq_zero
    (x : R) (M : ModuleCat.{u} R) (hx : x • 𝟙 M = 0)
    (n : ℕ)
    (b : (principalIdealPowerQuotientShortComplex x n).X₁ ⟶ M) :
    (principalIdealPowerQuotientShortComplexSuccTransition x n).τ₁ ≫ b = 0
theorem

derivedLocalCohomology_span_singleton_succ_transition_one_eq_zero

L184 ↗
EtaleFundamentalGroups.derivedLocalCohomology_span_singleton_succ_transition_one_eq_zero
Documentation

Every degree-one transition from (x)^n to (x)^(n+1) is zero when x annihilates the coefficient module.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
section PrincipalAnnihilated
variable {R : Type u} [CommRing R]
Lean source · statement
theorem derivedLocalCohomology_span_singleton_succ_transition_one_eq_zero
    (x : R) (M : ModuleCat.{u} R) (hx : x • 𝟙 M = 0)
    (n : ℕ) :
    (derivedLocalCohomologyPowersDiagram (Ideal.span {x}) M 1).map
      (homOfLE (Nat.le_succ n)).op.op = 0
theorem

derivedLocalCohomology_span_singleton_isZero_one_of_smul_id_eq_zero

L219 ↗
EtaleFundamentalGroups.derivedLocalCohomology_span_singleton_isZero_one_of_smul_id_eq_zero
Documentation

If x annihilates M, then degree-one derived local cohomology of M supported at the principal ideal (x) vanishes.

Source context 6 commands

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

noncomputable section
open CategoryTheory Limits Opposite
namespace EtaleFundamentalGroups
universe u
section PrincipalAnnihilated
variable {R : Type u} [CommRing R]
Lean source · statement
theorem derivedLocalCohomology_span_singleton_isZero_one_of_smul_id_eq_zero
    (x : R) (M : ModuleCat.{u} R) (hx : x • 𝟙 M = 0) :
    IsZero (derivedLocalCohomology (Ideal.span {x}) M 1)

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