NYLL
Module

DerivedLocalCohomologyModule.lean

Nyll.EtaleFundamentalGroups.Purity.DerivedLocalCohomologyModule
8 declarations indexed from sourceView source ↗

Module documentation

The module of derived local-cohomology classes

The scalar endomorphisms of the additive-group colimit satisfy the module laws. We package this action in an object of ModuleCat R, retaining the original additive group. The module structure is installed only while constructing that object; no additional global instance is put on the underlying additive-group colimit.

The colimit maps out of the derived-Ext groups are linear. Every class in the resulting module is annihilated by a power of the support ideal.

Imports3
Imported by21

Declarations

theorem

derivedLocalCohomologyScalarMap_add

L35 ↗
EtaleFundamentalGroups.derivedLocalCohomologyScalarMap_add
Documentation

Scalar endomorphisms of derived local cohomology respect addition.

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

derivedLocalCohomologyScalarMap_zero

L67 ↗
EtaleFundamentalGroups.derivedLocalCohomologyScalarMap_zero
Documentation

The zero scalar induces the zero 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_zero
    (I : Ideal R) (M : ModuleCat.{u} R) (i : ℕ) :
    derivedLocalCohomologyScalarMap I M i 0 = 0
def

derivedLocalCohomologyModuleStructure

L88 ↗
EtaleFundamentalGroups.derivedLocalCohomologyModuleStructure
Documentation

The scalar endomorphisms furnish the module laws on the existing additive group. This definition is deliberately not an instance.

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 derivedLocalCohomologyModuleStructure
    (I : Ideal R) (M : ModuleCat.{u} R) (i : ℕ) :
    Module R (derivedLocalCohomology I M i) where
  smul a z := derivedLocalCohomologyScalarMap I M i a z
  one_smul z :=
    ConcreteCategory.congr_hom (derivedLocalCohomologyScalarMap_one I M i) z
  mul_smul a b z :=
    ConcreteCategory.congr_hom (derivedLocalCohomologyScalarMap_mul I M i a b) z
  smul_zero a := map_zero (ConcreteCategory.hom
    (derivedLocalCohomologyScalarMap I M i a))
  smul_add a z w := map_add (ConcreteCategory.hom
    (derivedLocalCohomologyScalarMap I M i a)) z w
  add_smul a b z :=
    ConcreteCategory.congr_hom (derivedLocalCohomologyScalarMap_add I M i a b) z
  zero_smul z :=
    ConcreteCategory.congr_hom (derivedLocalCohomologyScalarMap_zero I M i) z
def

derivedLocalCohomologyModule

L107 ↗
EtaleFundamentalGroups.derivedLocalCohomologyModule
Documentation

Derived local cohomology as an R-module, with the additive group of its original derived-Ext colimit.

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 derivedLocalCohomologyModule
    (I : Ideal R) (M : ModuleCat.{u} R) (i : ℕ) : ModuleCat.{u} R
theorem

derivedLocalCohomologyModule_forget

L115 ↗
EtaleFundamentalGroups.derivedLocalCohomologyModule_forget
Documentation

Forgetting the module action recovers the original additive-group colimit, including its existing additive-group structure.

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 derivedLocalCohomologyModule_forget
    (I : Ideal R) (M : ModuleCat.{u} R) (i : ℕ) :
    (forget₂ (ModuleCat.{u} R) AddCommGrpCat.{u}).obj
        (derivedLocalCohomologyModule I M i) =
      derivedLocalCohomology I M i
theorem

derivedLocalCohomologyModule_smul

L124 ↗
EtaleFundamentalGroups.derivedLocalCohomologyModule_smul
Documentation

Scalar multiplication in the bundled module is the previously constructed colimit 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 derivedLocalCohomologyModule_smul
    (I : Ideal R) (M : ModuleCat.{u} R) (i : ℕ) (a : R)
    (z : derivedLocalCohomologyModule I M i) :
    a • z = derivedLocalCohomologyScalarMap I M i a z
def

derivedLocalCohomologyModuleι

L131 ↗
EtaleFundamentalGroups.derivedLocalCohomologyModuleι
Documentation

The colimit injection from the n-th derived-Ext group is linear.

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 derivedLocalCohomologyModuleι
    (I : Ideal R) (M : ModuleCat.{u} R) (i n : ℕ) :
    CategoryTheory.Abelian.Ext.{u}
      (ModuleCat.of R (R ⧸ I ^ n)) M i →ₗ[R]
        derivedLocalCohomologyModule I M i where
  toFun := ConcreteCategory.hom
    (colimit.ι (derivedLocalCohomologyPowersDiagram I M i) (op (op n)))
  map_add' α β :=
    map_add (ConcreteCategory.hom
      (colimit.ι (derivedLocalCohomologyPowersDiagram I M i)
        (op (op n)))) α β
  map_smul' a α := by
    change
      colimit.ι (derivedLocalCohomologyPowersDiagram I M i)
          (op (op n)) (a • α) =
        derivedLocalCohomologyScalarMap I M i a
          (colimit.ι (derivedLocalCohomologyPowersDiagram I M i)
            (op (op n)) α)
    exact (derivedLocalCohomologyScalarMap_ι_apply I M i a n α).symm
theorem

derivedLocalCohomologyModule_exists_idealPower_smul_eq_zero

L153 ↗
EtaleFundamentalGroups.derivedLocalCohomologyModule_exists_idealPower_smul_eq_zero
Documentation

Every class in the local-cohomology module is annihilated by every member of some power of the support ideal.

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

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