NYLL
Module

DerivedLocalCohomologyScalar.lean

Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologyScalar
9 declarations indexed from sourceView source ↗

Module documentation

Scalar endomorphisms and torsion in derived local cohomology

Scalars act on each derived-Ext group in the ideal-powers diagram and commute with its transition maps. Their induced colimit endomorphisms describe the scalar action without installing another module structure on the underlying additive-group colimit.

An element of an ideal annihilates Ext out of the quotient by that ideal. Consequently every local-cohomology class is annihilated by all members of some power of its support ideal.

Imports3
Imported by6

Declarations

theorem

derivedExt_quotient_smul_eq_zero

L35 ↗
EtaleFundamentalGroups.derivedExt_quotient_smul_eq_zero
Documentation

Every member of J annihilates derived Ext out of R / J.

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 derivedExt_quotient_smul_eq_zero
    (J : Ideal R) (M : ModuleCat.{u} R) (i : ℕ)
    (a : R) (ha : a ∈ J)
    (α : CategoryTheory.Abelian.Ext.{u}
      (ModuleCat.of R (R ⧸ J)) M i) :
    a • α = 0
def

derivedLocalCohomologyPowersScalarMap

L66 ↗
EtaleFundamentalGroups.derivedLocalCohomologyPowersScalarMap
Documentation

Scalar multiplication is a natural endomorphism of the powers diagram.

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 · full declaration
def derivedLocalCohomologyPowersScalarMap
    (I : Ideal R) (M : ModuleCat.{u} R) (i : ℕ) (a : R) :
    derivedLocalCohomologyPowersDiagram I M i ⟶
      derivedLocalCohomologyPowersDiagram I M i where
  app n := AddCommGrpCat.ofHom
    { toFun := fun α : CategoryTheory.Abelian.Ext.{u}
        (ModuleCat.of R (R ⧸ I ^ unop (unop n))) M i ↦ a • α
      map_zero' := smul_zero a
      map_add' := smul_add a }
  naturality {j k} f := by
    ext α
    let α' : CategoryTheory.Abelian.Ext.{u}
        (ModuleCat.of R (R ⧸ I ^ unop (unop j))) M i := α
    let q : ModuleCat.of R (R ⧸ I ^ unop (unop k)) ⟶
        ModuleCat.of R (R ⧸ I ^ unop (unop j)) :=
      (localCohomology.ringModIdeals
        (localCohomology.idealPowersDiagram I)).map f.unop
    change
      a • ((CategoryTheory.Abelian.Ext.mk₀ q).comp α' (zero_add i)) =
        (CategoryTheory.Abelian.Ext.mk₀ q).comp (a • α') (zero_add i)
    exact
      (CategoryTheory.Abelian.Ext.comp_smul
        (CategoryTheory.Abelian.Ext.mk₀ q) α' (zero_add i) a).symm
def

derivedLocalCohomologyScalarMap

L91 ↗
EtaleFundamentalGroups.derivedLocalCohomologyScalarMap
Documentation

The scalar endomorphism induced on derived 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
def derivedLocalCohomologyScalarMap
    (I : Ideal R) (M : ModuleCat.{u} R) (i : ℕ) (a : R) :
    derivedLocalCohomology I M i ⟶ derivedLocalCohomology I M i
theorem

derivedLocalCohomologyScalarMap_ι_apply

L98 ↗
EtaleFundamentalGroups.derivedLocalCohomologyScalarMap_ι_apply
Documentation

The scalar endomorphism acts on a colimit representative by its usual scalar action in derived Ext.

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 derivedLocalCohomologyScalarMap_ι_apply
    (I : Ideal R) (M : ModuleCat.{u} R) (i : ℕ) (a : R) (n : ℕ)
    (α : CategoryTheory.Abelian.Ext.{u}
      (ModuleCat.of R (R ⧸ I ^ n)) M i) :
    derivedLocalCohomologyScalarMap I M i a
        (colimit.ι (derivedLocalCohomologyPowersDiagram I M i)
          (op (op n)) α) =
      colimit.ι (derivedLocalCohomologyPowersDiagram I M i)
        (op (op n)) (a • α)
theorem

derivedLocalCohomology_exists_idealPower_scalarMap_eq_zero

L118 ↗
EtaleFundamentalGroups.derivedLocalCohomology_exists_idealPower_scalarMap_eq_zero
Documentation

Each local-cohomology class is annihilated by a power of the support ideal. The exponent can depend on the class.

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 derivedLocalCohomology_exists_idealPower_scalarMap_eq_zero
    (I : Ideal R) (M : ModuleCat.{u} R) (i : ℕ)
    (z : derivedLocalCohomology I M i) :
    ∃ n : ℕ, ∀ a : R, a ∈ I ^ n →
      derivedLocalCohomologyScalarMap I M i a z = 0
theorem

derivedLocalCohomology_exists_pow_scalarMap_eq_zero

L142 ↗
EtaleFundamentalGroups.derivedLocalCohomology_exists_pow_scalarMap_eq_zero
Documentation

In particular, a member of the support ideal acts locally nilpotently.

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 derivedLocalCohomology_exists_pow_scalarMap_eq_zero
    (I : Ideal R) (M : ModuleCat.{u} R) (i : ℕ)
    (a : R) (ha : a ∈ I) (z : derivedLocalCohomology I M i) :
    ∃ n : ℕ, derivedLocalCohomologyScalarMap I M i (a ^ n) z = 0
theorem

derivedLocalCohomologyScalarMap_one

L151 ↗
EtaleFundamentalGroups.derivedLocalCohomologyScalarMap_one
Documentation

The unit scalar induces the identity endomorphism.

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 derivedLocalCohomologyScalarMap_one
    (I : Ideal R) (M : ModuleCat.{u} R) (i : ℕ) :
    derivedLocalCohomologyScalarMap I M i 1 =
      𝟙 (derivedLocalCohomology I M i)
theorem

derivedLocalCohomologyScalarMap_mul

L172 ↗
EtaleFundamentalGroups.derivedLocalCohomologyScalarMap_mul
Documentation

Scalar multiplication on the colimit respects multiplication in R.

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 derivedLocalCohomologyScalarMap_mul
    (I : Ideal R) (M : ModuleCat.{u} R) (i : ℕ) (a b : R) :
    derivedLocalCohomologyScalarMap I M i (a * b) =
      derivedLocalCohomologyScalarMap I M i b ≫
        derivedLocalCohomologyScalarMap I M i a
theorem

derivedLocalCohomology_isZero_of_scalarMap_injective

L201 ↗
EtaleFundamentalGroups.derivedLocalCohomology_isZero_of_scalarMap_injective
Documentation

An injective scalar from the support ideal forces local cohomology to vanish: its powers are injective, whereas every class is killed by a power.

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 derivedLocalCohomology_isZero_of_scalarMap_injective
    (I : Ideal R) (M : ModuleCat.{u} R) (i : ℕ)
    (a : R) (ha : a ∈ I)
    (hinj : Function.Injective
      (ConcreteCategory.hom (derivedLocalCohomologyScalarMap I M i a))) :
    IsZero (derivedLocalCohomology I M i)

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